rsPredictionMap
plain-language theorem explainer
The Recognition Science prediction map is the concrete Predictor instance: for any cost functional and scale it returns the fixed RS dimensionless observables, certified inside experimental bounds. Exclusivity and bridge arguments cite it as the witness that a computable (J, φ) → observables map exists. Construction is a two-field structure instance: constant predict plus the existing within-bounds certificate.
Claim. The RS prediction map is a predictor whose prediction function sends every cost functional $J:\mathbb{R}\to\mathbb{R}$ and every scale $\varphi\in\mathbb{R}$ to the fixed RS dimensionless observable bundle, and whose certificate asserts that those observables lie within experimental bounds for all $J$ and $\varphi$.
background
In the exclusivity verification layer, a Predictor is a pair: a map from a cost functional $J$ and a scale $\varphi$ into dimensionless observables, together with a proof that every such output stays inside experimental bounds. Dimensionless observables collect the RS-native dimensionless targets (fine-structure band, mass-ladder ratios, and related constants) used for exclusivity checks.
The cost side is the standard recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique in the T5 step of the forcing chain. The scale is the golden ratio $\varphi$ fixed by self-similarity (T6). Upstream, rsObservables packages the concrete RS values and rs_within_bounds already proves they sit inside the experimental windows.
This module turns that fixed bundle into an explicit algorithm of Predictor type so existence and matching lemmas can quantify over predictors rather than hard-code one map.
proof idea
Definitional structure instance, not a tactic proof. The predict field is the constant function ignoring both $J$ and $\varphi$ and returning the precomputed RS observable record. The within_bounds field is likewise constant in $J$ and $\varphi$, pointing at the already-established certificate that those observables lie inside bounds. No algebraic reduction is performed here; the work is deferred to rsObservables and rs_within_bounds.
why it matters
This is the concrete witness for Open Problem 1 (Existence) in the exclusivity bridge: there exists a computable map from $(J_{\mathrm{cost}},\varphi)$ into dimensionless observables within bounds. Downstream, bridge_B5_prediction_map_exists packages it as an existential Predictor with definitional equality of the prediction at $(J_{\mathrm{cost}},\varphi)$ and the bounds certificate; prediction_map_matches_bounds is the direct value-identification corollary.
In the broader framework it sits after T5–T6 (unique $J$ and forced $\varphi$) and after the RS-native constant package ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$, $\alpha^{-1}$ in the narrow band). It does not derive new physics; it freezes the RS prediction algorithm into the type needed for exclusivity and micro-window comparison lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.