CancerTarget
plain-language theorem explainer
CancerTarget is the Cartesian product HallmarkCluster × TreatmentModality × OncogeneFamily, supplying the 125-element type for the oncology lattice. Systems biologists and oncologists modeling combination therapies cite it when testing the claim that multi-axis interventions produce multiplicative rather than additive effects. The declaration is realized as a direct type abbreviation to the product of three five-element inductive types.
Claim. Let $H$ be the set of five hallmark clusters, $T$ the set of five treatment modalities, and $O$ the set of five oncogene families. The cancer target space is the product space $H × T × O$.
background
The module defines three finite inductive types. HallmarkCluster enumerates proliferation, evasion, invasion, metabolic, and genomic. TreatmentModality enumerates surgery, radiation, chemotherapy, immunotherapy, and targetedTherapy. OncogeneFamily enumerates ras, myc, egfr, pi3k, and bcl2. Each carries DecidableEq, Repr, BEq, and Fintype instances, so all three sets are computable and have cardinality five.
proof idea
The definition is a direct abbreviation that expands to the Cartesian product of the three upstream inductive types HallmarkCluster, TreatmentModality, and OncogeneFamily.
why it matters
CancerTarget supplies the underlying type for cancerTargetCount (which proves cardinality 125), the three surjectivity theorems, the OncologyLatticeCert structure, and product_exceeds_sum. The module documentation states that the three axes are independent intervention levers, so the product exceeds the sum (125 > 15). This cross-domain lattice construction applies the Recognition Science emphasis on product structures to predict non-additive therapeutic outcomes, with zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.