HallmarkCluster
plain-language theorem explainer
HallmarkCluster enumerates five cancer hallmarks as an inductive type equipped with decidable equality and finite cardinality. Cross-domain oncology modelers cite it when assembling the 125-element target space for testing multiplicative therapy responses. The definition proceeds by direct enumeration of the five constructors with automatic derivation of Fintype and related type classes.
Claim. Let $H$ be the finite set whose elements are the five cancer hallmarks proliferation, evasion, invasion, metabolic reprogramming, and genomic instability, equipped with decidable equality and Fintype structure.
background
The module frames oncology as a three-axis product space whose axes are independent intervention levers: biological process, treatment modality, and driver mutation. Their Cartesian product is asserted to contain 125 elements, with the prediction that combination therapies indexed on all three axes exhibit multiplicative rather than additive clinical response. HallmarkCluster supplies the first axis, the set of canonical cancer hallmarks.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype by the deriving clause.
why it matters
This definition supplies the first coordinate for the CancerTarget product type and the OncologyLatticeCert structure that certifies the 125-element lattice together with projection surjectivity. It is used by hallmarkCount, product_exceeds_sum, and the modality and oncogene surjectivity theorems. The construction supports the module's structural claim that the product cardinality exceeds the sum of the individual cardinalities, confirming the multiplicative character of the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.