CombinationID
plain-language theorem explainer
The inductive enumeration of nine implemented Option A combinations indexes the falsifier registry. Researchers auditing cross-domain theorems in Recognition Science cite it to assign empirical actions and deliverables to each case. The declaration introduces nine named constructors and derives decidable equality, string representation, and finite cardinality.
Claim. The inductive type enumerating the implemented Option A combinations consists of nine cases: cognitive tensor, planet strata, oncology tensor, quantum molecular depth, attention tensor, Erikson reverse, universal response, Miller span, and regulatory ceiling.
background
The Option A Falsifier Registry maintains a finite pairing of cross-domain theorems with empirical test classes. This attachment prevents the cross-domain work from drifting into unfalsifiable numerology. The module carries zero sorry or axiom statements.
proof idea
Inductive definition that introduces nine constructors for the combinations and derives DecidableEq, Repr, and Fintype instances.
why it matters
This enumeration anchors the empirical layer of the Option A registry. It supplies the domain for analysisAction and deliverableFor, which map each case to concrete actions such as fitFactorModel for oncology tensor and deliverables such as oncologyFactorModelNotebook. The structure supports theorems including hasAnalysisAction_all and EmpiricalActionPlanCert that certify completeness of the first-pass schedule. It directly implements the module goal of keeping falsifiers attached to the Lean theorem bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.