prediction_map_matches_bounds
plain-language theorem explainer
The Recognition Science prediction map, evaluated at the forced cost J and the self-similar scale φ, lands inside the stated experimental windows for the dimensionless observables. Anyone checking that the exclusivity/prediction bridge is empirically anchored cites this. The proof is a one-line appeal to the calibration theorem that RS observables already sit in CODATA bounds.
Claim. The dimensionless observables produced by the RS prediction map at the recognition cost $J(x)=(x+x^{-1})/2-1$ and the fixed point $\varphi$ satisfy the componentwise experimental bound predicate (each coordinate lies between its lower and upper empirical limits).
background
In the exclusivity verification layer, a prediction map turns the RS cost functional and the self-similar scale into a tuple of dimensionless observables (inverse fine-structure constant, mass ratios, and related quantities). The predicate withinBounds asserts that every coordinate of such a tuple lies inside a fixed empirical window (CODATA-style lower/upper cuts).
The cost used here is the unique recognition cost $J(x)=\frac12(x+x^{-1})-1$ forced by the Recognition Composition Law (T5). The scale $\varphi$ is the self-similar fixed point from the forcing chain (T6). Upstream, the calibration theorem states that the cost-first RS observable tuple already lies inside those same empirical windows: it is an external anchor linking derived RS values to CODATA 2022 bounds.
Locally, the RS prediction map is the canonical Predictor instance that feeds $J$ and $\varphi$ into that same observable construction, so matching bounds is the value-identification step for the map.
proof idea
One-line term proof: the goal is exactly the statement of the upstream calibration theorem that RS observables lie within bounds. Applying that theorem discharges the goal, because the prediction map at $J$ and $\varphi$ is definitionally the RS observable tuple already checked against the empirical windows (componentwise norm_num comparison to the stored lower/upper cuts).
why it matters
This closes the value-identification seam for the exclusivity prediction map: the map is not merely well-typed, it outputs numbers inside experimental bounds. It sits on the external-anchor calibration that ties cost-first RS observables to CODATA windows, and it uses the forced pair $(J,\varphi)$ from the forcing chain (T5 J-uniqueness, T6 $\varphi$ fixed point) and the RCL-derived cost. Downstream exclusivity or bridge results that need "the RS predictor is empirically admissible" can quote this rather than re-open the bound arithmetic. No further used-by edges are recorded yet; the declaration is the terminal check in this module that the predictor matches the calibrated bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.