modality_surj
plain-language theorem explainer
The projection from the cancer target product space onto the TreatmentModality coordinate is surjective. Researchers constructing multi-axis therapy models cite this to confirm every modality pairs with arbitrary hallmarks and oncogenes. The proof is a direct term construction that fixes one hallmark and one oncogene family for any input modality.
Claim. The function $f : H_1 × M × O_1 → M$ given by $f(h, m, o) = m$, where $H_1$ is the set of five hallmark clusters, $M$ the set of treatment modalities, and $O_1$ the set of five oncogene families, is surjective.
background
CancerTarget is the product type HallmarkCluster × TreatmentModality × OncogeneFamily. HallmarkCluster is the inductive type with constructors proliferation, evasion, invasion, metabolic, genomic. OncogeneFamily is the inductive type with constructors ras, myc, egfr, pi3k, bcl2. Both derive DecidableEq, Repr, BEq, Fintype. The module sets the oncology lattice as the 5 × 5 × 5 product space of 125 targets whose axes represent independent intervention levers (cancer behavior, attack method, driver mutation).
proof idea
The proof is a term-mode construction. It introduces an arbitrary modality x and supplies the explicit witness triple (HallmarkCluster.proliferation, x, OncogeneFamily.ras) whose projection recovers x by reflexivity.
why it matters
The result supplies one of the three surjectivity fields required by the OncologyLatticeCert structure, which also records the target cardinality 125 and the multiplicative inequality. It supports the module claim that combination therapies indexed on all three axes should exhibit multiplicative rather than additive responses on TCGA data. The theorem completes the lattice certification bundle alongside the symmetric hallmark and oncogene surjectivities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.