oncogeneCount
plain-language theorem explainer
OncogeneFamily is the inductive type with constructors ras, myc, egfr, pi3k, bcl2. Researchers modeling three-axis combination therapies cite this result to fix the third factor in the 125-element target space. The proof is a one-line wrapper that invokes decide on the derived Fintype instance.
Claim. $|OncogeneFamily| = 5$, where OncogeneFamily is the inductive type with constructors ras, myc, egfr, pi3k, bcl2.
background
The OncologyLattice module models cancer therapy targets as the Cartesian product HallmarkCluster × TreatmentModality × OncogeneFamily. Each axis has five elements, producing a 125-element space whose independence is asserted because the axes represent distinct intervention levers. The module documentation states that combination therapies indexed on all three axes should exhibit multiplicative rather than additive response, testable on TCGA data.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive definition of OncogeneFamily derives a Fintype instance whose cardinality is computed directly from the five constructors.
why it matters
This result is invoked by cancerTargetCount to establish that the total number of cancer targets is 125 and by product_exceeds_sum to show that 125 exceeds the sum of the three separate cardinalities. It supplies the third factor in the module's structural claim that cancer therapy searches a three-axis product space. The declaration thereby supports the prediction of multiplicative effects for therapies that move along all three axes simultaneously.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.