PredictedObservable
plain-language theorem explainer
The inductive type enumerates nine observable signatures that Recognition Science predicts for its C1-C9 cross-domain theorems. Protocol designers and falsification checks cite it when specifying what each structural claim must produce in data. The definition is a direct finite enumeration whose Fintype instance is derived automatically.
Claim. Let $P$ be the finite type whose elements are the nine predicted observables: tensor rank 125, strata ratio as a power of phi, multiplicative therapy response, five-bit address bound, forty stable five transient, reverse Erikson order, unit response coefficient, q-space span sequence, and regulatory ceiling 70.
background
The Option A Falsifier Registry pairs each of the nine cross-domain theorems with an empirical test class, dataset class, predicted observable, and failure mode. This attachment keeps the Lean structural results from drifting into unfalsifiable claims. The module defines several parallel enumerative types (CombinationID, TestClass, DatasetClass, EmpiricalStatus, FailureMode) that together form the registry.
proof idea
Inductive definition that introduces the nine constructors explicitly. The DecidableEq, Repr, and Fintype instances are obtained by the deriving clause with no further proof steps required.
why it matters
Supplies the observable field required by ProtocolFalsifiable and ProtocolSpec, and is counted in FalsifierRegistryCert. It therefore closes the empirical loop for the nine combinations referenced in the downstream empirical protocol. The construction directly implements the registry's purpose of keeping falsifiers attached to the theorem bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.