modalityCount
The theorem asserts that the finite set of treatment modalities contains exactly five elements. Researchers modeling multi-axis cancer therapies cite this count when establishing the 125-element product space of intervention axes. The proof is a direct decision procedure on the enumerated inductive definition of the modality type.
claimLet $T$ be the set of treatment modalities consisting of surgery, radiation, chemotherapy, immunotherapy, and targeted therapy. Then $|T| = 5$.
background
In the oncology lattice model, cancer therapy is structured along three independent axes: HallmarkCluster, TreatmentModality, and OncogeneFamily. Their product yields a 125-element space of possible intervention combinations. The TreatmentModality axis enumerates five distinct approaches: surgery, radiation, chemotherapy, immunotherapy, and targeted therapy. This setup predicts that combination therapies should exhibit multiplicative rather than additive effects, testable on clinical data.
proof idea
The proof applies the decide tactic to compute the cardinality of the finite type directly from its inductive definition with five constructors.
why it matters in Recognition Science
This count is used to derive the total of 125 cancer targets via the product of the three axes. It supports the claim that the product exceeds the sum of the individual cardinalities (125 > 15), highlighting the multiplicative structure. The result fills in the structural claim for the 5 × 5 × 5 lattice in cross-domain oncology modeling.
scope and limits
- Does not claim these five modalities cover all possible therapies.
- Does not model synergies or conflicts between modalities.
- Does not connect to the core Recognition Science forcing chain or constants.
- Does not address empirical validation on TCGA data.
Lean usage
simp only [modalityCount]formal statement (Lean)
37theorem modalityCount : Fintype.card TreatmentModality = 5 := by decide