PredictionFunction
plain-language theorem explainer
A prediction function assigns to every state of a physics framework the four canonical dimensionless observables, and requires that assignment to be constant across states. Exclusivity and verification arguments cite it as the non-trivial interface for "derives observables." It is a pure structure: a total map plus a uniformity axiom, with no proof obligations beyond well-typed fields.
Claim. A prediction function on a state space $S$ is a total map $\mathrm{predict}: S \to \mathcal{O}$ into the four dimensionless observables $(\alpha^{-1},\, m_e/m_\mu,\, m_p/m_e,\, G m_e^2/(\hbar c))$, together with the uniformity condition that $\mathrm{predict}(s_1)=\mathrm{predict}(s_2)$ for all $s_1,s_2\in S$. Predictions are therefore framework-determined, not state-dependent.
background
The Observables module builds a non-trivial interface for physics frameworks: "derives observables" must mean producing specific numerical predictions comparable to measurement, not a vacuous existence claim. It separates a cost-first core (pure types and $\varphi$-derived values) from an external-anchor section (CODATA bounds, marked @[external_anchor]).
The codomain is the structure of dimensionless observables: $\alpha^{-1}$, the electron-muon mass ratio, the proton-electron mass ratio, and the dimensionless gravitational coupling $G m_e^2/(\hbar c)$. All four are pure ratios, so SI anchor issues never enter the type. Recognition Science supplies reference values for these via the $\varphi$-ladder and the forcing chain (T5 J-cost uniqueness through the mass and coupling formulae).
Uniformity encodes that a complete framework fixes its predictions once and for all: different states of the same theory must not yield different constants of nature.
proof idea
Structure definition, not a theorem. Two fields: a total function from the parameter StateSpace into dimensionless observables, and a propositional field asserting that function is constant on the whole state space. No tactics, no lemmas, no sorry. Inhabitants are built by supplying an explicit map and a proof of equality of its values (often rfl when the map ignores the state).
why it matters
This is the carrier type for the strong, non-trivial derivation predicate used throughout exclusivity verification. Downstream, DerivesObservablesStrong asserts existence of such a function whose outputs lie inside empirical bounds; DerivesObservablesWitness packages the function with an explicit bounds proof. Concrete inhabitants include the RS unit-state prediction (feeding the $\varphi$-derived observables) and a deliberately wrong "bad" prediction used to prove that frameworks with incorrect $\alpha^{-1}$ fail the strong predicate.
That failure theorem is the key non-triviality test: not every framework satisfies the interface. Parameter-count bookkeeping in the Framework module also routes through this type when scoring algorithmic frameworks. In the broader RS picture it sits on the verification side of the forcing chain: once T5–T8 and the mass ladder fix the numbers, this structure is how those numbers are presented as framework-level predictions rather than free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.