hallmarkCount
plain-language theorem explainer
hallmarkCount proves that the finite type HallmarkCluster has cardinality exactly five. Researchers building oncology lattices cite the result to fix one axis when computing the size of the 5×5×5 product space. The proof applies the decide tactic to the Fintype instance derived from the inductive definition.
Claim. Let HallmarkCluster be the inductive type whose constructors are proliferation, evasion, invasion, metabolic, and genomic. Then the cardinality of this finite type equals 5.
background
The Oncology Lattice module models cancer therapy search as the product space HallmarkCluster × TreatmentModality × OncogeneFamily. Module documentation states that the three axes represent independent levers and predicts that combination therapies produce multiplicative rather than additive responses, testable on TCGA data.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic enumerates the five constructors of the inductive HallmarkCluster and confirms the derived Fintype cardinality equals 5.
why it matters
cancerTargetCount applies hallmarkCount inside a simp to obtain Fintype.card CancerTarget = 125. product_exceeds_sum then rewrites with the three cardinalities to show the product exceeds their sum. The declaration realizes the 5×5×5 structural claim of the module. It extends the Recognition lattice construction to oncology without reference to forcing chains or phi constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.