modalityCount
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.