bridge_B5_prediction_map_exists
plain-language theorem explainer
A Predictor exists that sends the J-cost functional and φ to the RS dimensionless observable bundle and lands inside the prescribed bounds. Anyone citing Bridge B5 or Open Problem 1 (existence of the RS prediction map) uses this. The proof is a three-component term witness: the concrete map, reflexivity of equality, and the already-proved bounds lemma.
Claim. There exists a prediction procedure $P$ (a computable map from a cost functional and a scale to a bundle of dimensionless observables) such that $P(J,\varphi)$ equals the RS observable bundle and $P(J,\varphi)$ lies within the prescribed bounds, where $J(x)=(x+x^{-1})/2-1$ and $\varphi$ is the self-similar fixed point.
background
The module builds the exclusivity side of verification: a formal prediction map from the RS primitives to dimensionless observables, then checks that the image sits inside experimental windows.
The cost input is the recognition cost $J(x)=(x+x^{-1})/2-1$, the unique functional forced by the Recognition Composition Law (forcing chain T5). The scale input is $\varphi$, the self-similar fixed point forced at T6. A Predictor is a structure packing a map (cost, scale) → DimensionlessObservables together with a blanket bounds obligation on every input pair.
The concrete RS algorithm is the sibling rsPredictionMap; the sibling rsObservables is the target bundle, and rs_within_bounds already records that this bundle satisfies withinBounds.
proof idea
Pure term-mode existence. The witness is the triple ⟨rsPredictionMap, rfl, rs_within_bounds⟩: the concrete RS prediction map supplies the Predictor, reflexivity discharges equality of its output on (Jcost, phi) with rsObservables, and the sibling lemma rs_within_bounds discharges the bounds conjunct. No tactics and no further unfolding.
why it matters
Closes Open Problem 1 (Existence) on the exclusivity bridge: a computable map from (Jcost, φ) into the dimensionless observable space that stays inside bounds. That is Bridge B5 in the PredictionMap module. It packages the T5 J-cost and T6 φ inputs into a single certified predictor, so later uniqueness or micro-window arguments (siblings such as componentwiseClose, withinMicroWindow, rs_within_micro_window) can treat the RS prediction as an inhabited, bounds-checked object rather than a schematic. No downstream consumers are wired yet; the declaration is the existence anchor for the exclusivity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.