TreatmentModality
plain-language theorem explainer
TreatmentModality enumerates the five standard cancer intervention types that form one axis of the oncology lattice product space. Modelers of combination therapies cite this enumeration when building the 125-element HallmarkCluster × TreatmentModality × OncogeneFamily structure and verifying its surjectivity properties. The declaration is a plain inductive type whose deriving clauses supply the finite-type and decidability instances needed by the downstream cardinality and surjectivity theorems.
Claim. Let $T$ be the finite type whose elements are the five treatment modalities: surgery, radiation, chemotherapy, immunotherapy, and targeted therapy.
background
The Oncology Lattice module models cancer therapy as an exhaustive search over the product of three independent axes whose cardinalities multiply to 125. One axis is the set of treatment modalities; the other two are HallmarkCluster (cancer behaviors) and OncogeneFamily (driver mutations). The module states that current practice mostly varies one axis at a time, while the structural claim predicts that full-product indexing yields multiplicative rather than additive response on TCGA data. The construction imports Mathlib to obtain Fintype and DecidableEq instances automatically.
proof idea
The declaration is an inductive definition with five constructors. The deriving clause for DecidableEq, Repr, BEq, and Fintype is supplied by Mathlib and requires no further proof steps.
why it matters
TreatmentModality supplies the middle factor in the CancerTarget product type and the modalityCount theorem that fixes its cardinality at 5. It is required by the surjectivity lemmas hallmark_surj, modality_surj, and oncogene_surj, and by the OncologyLatticeCert structure that certifies the full lattice. The definition directly enables the product_exceeds_sum theorem, which records the module's central empirical prediction that 125 exceeds the sum 15. This cross-domain application instantiates the Recognition Science emphasis on product structures whose cardinality is strictly larger than the sum of the factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.