prediction_map_unique
plain-language theorem explainer
Any two admissible predictors whose outputs at the RS pair (J-cost, φ) both sit inside the fixed 10^{-6} micro-window around the RS observable bundle are componentwise at most 2·10^{-6} apart. Cited as the clean bounds-uniqueness surrogate for Open Problem 2 when exact O(1)-complexity uniqueness is not yet encoded. Proof is a three-component triangle inequality via closeness to a common reference.
Claim. Let $P_1,P_2$ be predictors (maps from a cost functional and scale to dimensionless observables, each required to land inside experimental bounds). If both $P_1(J,\varphi)$ and $P_2(J,\varphi)$ lie in the micro-window of width $10^{-6}$ about the RS reference bundle, then the two output triples are componentwise within distance $2\cdot 10^{-6}$ of each other.
background
The module builds a verification layer for exclusivity of Recognition Science predictions. A Predictor is a structure packing a computable map (cost, scale) → DimensionlessObservables together with a proof that every output stays inside experimental bounds. The concrete RS algorithm is the distinguished instance of this structure.
Observables are compared in a fixed micro-window of width microWidth (numerically $10^{-6}$) about the RS bundle evaluated at the canonical cost $J(x)=(x+x^{-1})/2-1$ and the golden scale $\varphi$. Componentwise closeness of two triples is the product metric on the three dimensionless channels (fine-structure, mass-ratio, and related packing observables).
The local lemma close_to_same_reference records the elementary fact that two real numbers each within $\varepsilon$ of a common reference are within $2\varepsilon$ of each other. That fact is applied once per channel.
proof idea
Introduce the two micro-window hypotheses and unfold the definitions of the window predicate, componentwise closeness, and the numeric width. Destructure each hypothesis into its three channel inequalities. Build the conclusion as a triple of goals; discharge each by applying close_to_same_reference to the matching pair of channel bounds. No analytic estimates beyond the triangle inequality are required.
why it matters
This is the formal content of Open Problem 2 in its present scaffold: exact uniqueness of an O(1)-complexity prediction map is not yet encoded, so the development proves a bounds-uniqueness surrogate instead. Any two admissible maps that both hit the RS micro-window at $(J,\varphi)$ cannot disagree by more than twice the window width.
In the broader Recognition framework the result anchors the exclusivity claim that the RS prediction map (forced by T5 J-uniqueness and T6 $\varphi$ as self-similar fixed point) is the only map that can sit inside the experimental micro-window. Downstream exclusivity or bridge theorems can quote it to convert "both match data" into "both match each other." No parent theorem currently depends on it (used_by is empty), so it is a leaf ready for the exclusivity assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.