predictedObservable_count
plain-language theorem explainer
The theorem asserts that the inductive type PredictedObservable enumerates exactly nine observables derived from Recognition Science structural theorems plus the core hypotheses. Researchers auditing cross-domain falsifiability would cite the count to confirm registry completeness before empirical tests. The proof is a direct decidable computation on the finite inductive definition.
Claim. The cardinality of the type of observables predicted by the Lean structural theorems together with the Recognition Science hypotheses equals nine: $|PredictedObservable| = 9$.
background
The module maintains a finite registry that pairs each of the nine C1-C9 cross-domain theorems with an empirical test class, ensuring the structural claims remain attached to concrete observables rather than drifting into unfalsifiable numerology. PredictedObservable is the inductive type whose nine constructors list the specific observables (tensorRank125, strataRatioPhiPower, multiplicativeTherapyResponse, fiveBitAddressBound, fortyStableFiveTransient, reverseEriksonOrder, unitResponseCoefficient, qSpaceSpanSequence, regulatoryCeiling70) generated by the phi-ladder, J-cost, and ledger structures. Upstream results supply the supporting structures: nuclear densities in phi-tiers from NucleosynthesisTiers, J-cost calibration from LedgerFactorization, and gauge content plus three generations from SpectralEmergence.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the automatically generated Fintype instance of the inductive type PredictedObservable.
why it matters
The result supplies the nine_observables field inside falsifierRegistryCert, which certifies the complete registry of nine observables, nine test classes, and nine dataset classes. It directly implements the module's purpose of keeping falsifiers attached to the C1-C9 theorems so the framework stays testable. In the larger Recognition Science setting it closes the loop from the T0-T8 forcing chain and Recognition Composition Law by enumerating the concrete observables needed to confront constants such as alpha inverse in (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.