empiricalStatus
plain-language theorem explainer
This definition supplies a finite case-by-case mapping from each of the nine implemented Option A cross-domain combinations to its empirical status. A working physicist or mathematician auditing the Recognition Science formalization cites it to determine which theorems carry attached empirical hypotheses versus scaffolds. The definition is realized as exhaustive pattern matching on the inductive CombinationID type with no auxiliary lemmas.
Claim. The function that maps each implemented combination identifier to its status relative to the empirical claim: cognitive tensor, planet strata, oncology tensor, quantum molecular depth, attention tensor, universal response, Miller span, and regulatory ceiling each map to theorem-plus-hypothesis, while Erikson reverse maps to scaffold-plus-hypothesis.
background
The Option A Falsifier Registry is a finite registry pairing each C1-C9 cross-domain theorem with its empirical test class. This does not prove the empirical claims. It keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology, with Lean status zero sorry and zero axiom. CombinationID is the inductive type listing the implemented combinations (cognitive tensor through regulatory ceiling, with C10 left as commentary). EmpiricalStatus is the inductive type classifying status as theoremOnly, theoremPlusHypothesis, or scaffoldPlusHypothesis.
proof idea
The definition is a direct exhaustive pattern match on the nine constructors of CombinationID, returning the corresponding EmpiricalStatus constructor in each case. No lemmas are applied and no tactics are used; it is a pure definitional expansion.
why it matters
This definition anchors the falsifier registry so that each cross-domain theorem remains explicitly linked to its empirical test class, fulfilling the module's stated purpose of preventing drift into unfalsifiable numerology. It supplies the classification layer referenced by the broader Option A framework and the PDG.Fits dataset structure, though it currently has no downstream dependents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.