Predictor
plain-language theorem explainer
A Predictor packages a map from a cost functional J and a scale φ to the dimensionless observable bundle (α⁻¹, m_e/m_μ, m_p/m_e), plus a certificate that every output sits inside fixed empirical windows. Anyone citing the exclusivity bridge (existence or the micro-window uniqueness surrogate) uses this type as the carrier. It is a pure structure definition: two fields, no separate proof body.
Claim. A predictor is a pair $(\mathrm{predict},\,\mathrm{within\_bounds})$ where $\mathrm{predict}:(J,\varphi)\mapsto(\alpha^{-1},\,m_e/m_\mu,\,m_p/m_e)$ sends a cost functional $J:\mathbb{R}\to\mathbb{R}$ and a scale $\varphi\in\mathbb{R}$ to the dimensionless observable triple, and $\mathrm{within\_bounds}$ asserts that for every such $(J,\varphi)$ the triple lies inside the fixed empirical intervals on those three ratios.
background
In the exclusivity verification layer, any candidate physics framework is asked to emit a fixed bundle of dimensionless ratios: the inverse fine-structure constant $\alpha^{-1}$, the electron-to-muon mass ratio, and the proton-to-electron mass ratio. The local structure DimensionlessObservables is exactly that triple; no SI anchors appear.
Empirical admissibility is the predicate withinBounds: $\alpha^{-1}\in[137.0359,137.0361]$, $m_e/m_\mu\in[4.836\times10^{-3},4.837\times10^{-3}]$, and $m_p/m_e\in[1836.15,1836.16]$. (A sibling Observables module carries the same idea against CODATA windows; this module hard-codes the tight verification band.)
The module sits downstream of the cost-first ledger and the RS-native constants (including $\varphi$ and the J-cost). A Predictor is the abstract interface that turns those inputs into an admissible observable bundle.
proof idea
No proof body: this is a structure declaration. The first field is a function of type $(\mathbb{R}\to\mathbb{R})\to\mathbb{R}\to$ DimensionlessObservables. The second field is a universal Prop requiring that every value of that function satisfies the local withinBounds predicate. Inhabitants are built by supplying both fields (see the concrete rsPredictionMap instance).
why it matters
This type is the carrier for Open Problem 1 (existence) and the reformulated Open Problem 2 (uniqueness) in the exclusivity bridge. Downstream, bridge_B5_prediction_map_exists exhibits a Predictor whose prediction at $(J_{\mathrm{cost}},\varphi)$ equals the RS bundle and lies in bounds; rsPredictionMap is that concrete inhabitant (constant map to rsObservables). The uniqueness surrogate prediction_map_unique quantifies over two Predictors and shows that if both land in the same $10^{-6}$ micro-window around the RS bundle, their outputs are componentwise $2\cdot10^{-6}$-close.
In framework terms this is the verification face of the forcing chain: once T5 fixes J and T6 fixes $\varphi$, the prediction map is the object that must hit the $\alpha^{-1}$ band near 137.036 and the mass-ratio windows. The structure itself does not force uniqueness of the algorithm; it only names the admissible maps that later uniqueness arguments compare.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.