empiricalStatus_count
The theorem establishes that the empirical status type for theorems in the Option A falsifier registry has exactly three elements. Researchers auditing attachment of empirical tests to cross-domain claims in Recognition Science would cite this cardinality to confirm the registry structure. The proof is a direct decide tactic on the derived Fintype instance of the inductive type.
claim$|E| = 3$ where $E$ is the finite type whose elements classify a theorem as theorem-only, theorem-plus-hypothesis, or scaffold-plus-hypothesis.
background
The Option A Falsifier Registry maintains a finite pairing of C1-C9 cross-domain theorems with empirical test classes. This keeps falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. EmpiricalStatus is the inductive type with constructors theoremOnly, theoremPlusHypothesis, and scaffoldPlusHypothesis, each recording the status of a Lean theorem relative to its empirical claim. The upstream Dataset structure organizes empirical inputs into separate lists for leptons, quarks, bosons, and baryons, but the present cardinality result depends only on the Fintype derivation for EmpiricalStatus.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This succeeds because the inductive definition of EmpiricalStatus derives both DecidableEq and Fintype, so the cardinality computation reduces to a decidable equality that the tactic discharges automatically.
why it matters in Recognition Science
The result supplies the three_statuses field inside the falsifierRegistryCert definition, which aggregates nine combinations, nine test classes, three statuses, nine dataset classes, and nine observables to certify the registry. It directly implements the module's guarantee of zero sorry and zero axiom, ensuring every cross-domain theorem remains tied to a concrete empirical test class. The construction prevents the Recognition Science claims from becoming unfalsifiable numerology.
scope and limits
- Does not assign a specific status to any individual theorem.
- Does not validate or execute any empirical test.
- Does not introduce or permit additional status categories.
- Does not prove existence of matching empirical data for the theorems.
Lean usage
example : falsifierRegistryCert.three_statuses = 3 := by rw [falsifierRegistryCert]; exact empiricalStatus_countformal statement (Lean)
57theorem empiricalStatus_count : Fintype.card EmpiricalStatus = 3 := by
proof body
Decided by rfl or decide.
58 decide
59
60/-- Dataset class expected to carry the empirical test. -/