EmpiricalStatus
plain-language theorem explainer
The inductive definition classifies each C1-C9 theorem in the Option A Falsifier Registry by its relation to empirical claims. It separates pure theorems from those carrying hypotheses and from scaffolds. Researchers mapping cross-domain results to test classes cite it to maintain falsifiability. The definition enumerates three constructors and derives decidability plus finiteness instances.
Claim. Inductive type with three constructors indicating whether a theorem stands alone, is paired with an empirical hypothesis, or forms a scaffold paired with a hypothesis.
background
The module builds a finite registry that pairs each of the nine C1-C9 cross-domain theorems with an empirical test class. This keeps falsifiers attached to the Lean bundles and blocks drift into unfalsifiable numerology. The status type supplies the vocabulary for distinguishing structural theorems from those that require empirical hypotheses.
proof idea
One-line inductive definition that lists the three constructors and derives DecidableEq, Repr, and Fintype instances.
why it matters
The type is referenced by the empiricalStatus mapping over CombinationID and by the FalsifierRegistryCert structure that certifies three statuses among its nine-by-nine counts. It directly implements the module goal of tethering each theorem to a falsifiable test class, consistent with the Recognition Science requirement that cross-domain claims remain empirically grounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.