oncologyLatticeCert
plain-language theorem explainer
oncologyLatticeCert assembles the 125-element cancer target space into a single certificate record by direct substitution of its four component properties. Modelers of combination therapies would cite the record to assert that the three axes HallmarkCluster, TreatmentModality and OncogeneFamily are each surjective and that the product cardinality strictly exceeds their sum. The definition is a one-line record constructor that plugs in the pre-proved theorems cancerTargetCount, hallmark_surj, modality_surj, oncogene_surj and product_exceeds_sum.
Claim. Let $C$ denote the finite type of cancer targets. Then $|C|=125$, the projection $C$ to HallmarkCluster is surjective, the projection to TreatmentModality is surjective, the projection to OncogeneFamily is surjective, and $125 > 5+5+5$.
background
The module defines a 5 by 5 by 5 product space whose elements are triples (HallmarkCluster, TreatmentModality, OncogeneFamily). Each axis is an independent intervention lever: the hallmark describes what the cancer does, the modality how it is attacked, and the oncogene which driver mutation is present. The upstream theorem cancerTargetCount establishes the cardinality equality by reducing the product of the three axis cardinalities via Fintype.card_prod and the three count lemmas. The three surjectivity theorems each supply an explicit witness triple that hits any given element on its axis.
proof idea
The definition is a direct record construction. It instantiates target_count with cancerTargetCount, hallmark_surj with hallmark_surj, modality_surj with modality_surj, oncogene_surj with oncogene_surj, and multiplicative with product_exceeds_sum.
why it matters
The definition certifies the structural claim of the oncology lattice module that combination therapies indexed on all three axes should exhibit multiplicative rather than additive response. It aligns the lattice with the multiplicative property of J-automorphisms from CostAlgebra, thereby embedding the cross-domain oncology example inside the Recognition Science framework. No downstream theorems yet consume the certificate, leaving open its use in empirical validation against TCGA response data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.