cancerTargetCount
plain-language theorem explainer
The theorem establishes that the finite cardinality of the cancer target space equals 125. Mathematical oncologists modeling combination therapies would cite this to quantify the size of the three-axis search lattice. The proof is a one-line term simplification that unfolds the product definition and substitutes the three axis cardinality lemmas.
Claim. Let $H$, $M$, and $O$ denote the finite types HallmarkCluster, TreatmentModality, and OncogeneFamily. If $C := H × M × O$, then the cardinality of $C$ is 125.
background
The OncologyLattice module models cancer targets as the Cartesian product HallmarkCluster × TreatmentModality × OncogeneFamily. The module documentation describes this as a 5 × 5 × 5 lattice because the axes represent independent intervention levers: cancer hallmarks, treatment modalities, and oncogene families. Empirical prediction follows that combination therapies should show multiplicative response on TCGA data.
proof idea
The proof applies simp to the goal using the definition of CancerTarget as the product type, the lemma Fintype.card_prod for the cardinality of a product, and the three upstream cardinality theorems hallmarkCount, modalityCount, and oncogeneCount. This reduces the equality directly to the arithmetic fact 5 × 5 × 5 = 125.
why it matters
This theorem supplies the target_count field in the oncologyLatticeCert definition and is invoked by product_exceeds_sum to establish that the product 125 exceeds the sum 15. It instantiates the structural claim in the module documentation for the 5×5×5 oncology lattice. In the Recognition framework it illustrates the multiplicative composition across domains, aligning with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.