PredictedObservable
plain-language theorem explainer
PredictedObservable enumerates the nine empirical signatures attached to the C1-C9 cross-domain theorems in the Recognition Science falsifier registry. A researcher specifying an empirical protocol for any combination would cite this type inside ProtocolFalsifiable to name the observable that must be measured. The declaration is a plain inductive enumeration that derives DecidableEq, Repr and Fintype with no further obligations.
Claim. Let $PO$ be the finite inductive type whose nine constructors are the tensor of rank 1.25, the strata ratio expressed as a power of the golden ratio, the multiplicative therapy response, the five-bit address bound, the pattern of forty stable and five transient states, the reverse Erikson order, the unit response coefficient, the q-space span sequence, and the regulatory ceiling of 70.
background
The Option A Falsifier Registry pairs each of the nine cross-domain theorems (C1-C9) with a concrete empirical test class. PredictedObservable supplies the list of observables that the structural theorems plus the Recognition Science hypothesis predict for those combinations. The module states explicitly that the registry does not prove the empirical claims but keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. This type appears directly in the definition of ProtocolFalsifiable, which requires each combination to possess a dataset class, a predicted observable, and a failure mode.
proof idea
The declaration is an inductive definition that introduces exactly nine constructors, one for each registered observable. It then derives DecidableEq, Repr and Fintype automatically; no lemmas are applied and no tactics are required beyond the inductive declaration itself.
why it matters
PredictedObservable supplies the observable component required by ProtocolFalsifiable and ProtocolSpec, and it is counted in FalsifierRegistryCert to certify that exactly nine observables are registered. It thereby anchors the empirical predictions that arise from the unified forcing chain (T0-T8) and the Recognition Composition Law, ensuring the nine cross-domain theorems remain testable rather than numerological. The downstream certification theorem predictedObservable_count confirms the cardinality matches the nine combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.