OncologyLatticeCert
plain-language theorem explainer
The OncologyLatticeCert structure certifies that the cancer target space is the cartesian product of three five-element sets, yielding cardinality 125 with surjective projections onto each axis and a strict multiplicative inequality on cardinalities. Cross-domain modelers of combination cancer therapies would cite it to encode the three-axis intervention lattice. It is realized as a structure definition that directly assembles the product cardinality, three explicit surjectivity witnesses, and the inequality.
Claim. Let $H$, $M$, $O$ be sets of cardinality 5. Let $C = H × M × O$. Then $|C| = 125$, the projections $C → H$, $C → M$, $C → O$ are surjective, and $|C| > |H| + |M| + |O|$.
background
The module introduces three inductive types, each with five constructors: HallmarkCluster (proliferation, evasion, invasion, metabolic, genomic), TreatmentModality (surgery, radiation, chemotherapy, immunotherapy, targetedTherapy), and OncogeneFamily (ras, myc, egfr, pi3k, bcl2). CancerTarget is defined as their cartesian product. The module doc states the structural claim that cancer therapy searches a three-axis product space of cardinality 125 whose axes correspond to independent intervention levers (what the cancer does, how we attack it, which driver mutation it carries).
proof idea
The structure is defined by enumerating its five fields. The target_count field states the cardinality equality. The three surjectivity fields are filled by the module theorems hallmark_surj, modality_surj, and oncogene_surj, each supplying an explicit preimage. The multiplicative field records the inequality between product cardinality and the sum of the three factor cardinalities.
why it matters
The structure is instantiated by the downstream definition oncologyLatticeCert, which supplies concrete values using the module's cardinality and surjectivity results. It encodes the multiplicative character of the oncology lattice, aligning with the Recognition Science emphasis on multiplicative composition laws. The declaration supplies the cross-domain certificate that closes the scaffolding for applying J-automorphism multiplicativity to biological target spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.