close_to_same_reference
plain-language theorem explainer
If two real numbers each sit within ε of a common reference, their mutual distance is at most 2ε. Verification and exclusivity arguments cite this when converting “both near the RS bundle” into “near each other.” The proof is a short triangle-inequality calc with absolute-value symmetry and additivity of ≤.
Claim. For all real $x,y,z,\varepsilon$, if $|x-z|\le\varepsilon$ and $|y-z|\le\varepsilon$, then $|x-y|\le 2\varepsilon$.
background
In the PredictionMap verification module, dimensionless RS observables are packaged as a finite bundle of real scalars (the RS prediction at the cost functional $J$ and the golden ratio $\varphi$). Admissible predictors are compared to that bundle inside a fixed nonnegative micro-window of width microWidth (order $10^{-6}$ in the exclusivity scaffold).
The local geometric fact needed is elementary real analysis: closeness to a shared reference controls pairwise separation. Absolute value on $\mathbb{R}$ is a metric, so the triangle inequality $|x-y|\le|x-z|+|z-y|$ applies, and $|z-y|=|y-z|$.
The module sits in the exclusivity/verification layer: it does not re-derive $J$ or $\varphi$, but checks that prediction maps landing near the RS reference cannot drift far from one another componentwise.
proof idea
Rewrite $|y-z|$ as $|z-y|$ via absolute-value commutativity. Apply the triangle inequality $|x-y|\le|x-z|+|z-y|$. Bound the sum by $\varepsilon+\varepsilon$ using monotonicity of addition on $\le$, then simplify $\varepsilon+\varepsilon=2\varepsilon$ by ring. The whole argument is a three-step calc block; no Recognition-specific lemmas are required.
why it matters
Feeds prediction_map_unique, the scaffold’s bounds-uniqueness surrogate for Open Problem 2: if two admissible predictors both land inside the same micro-window around the RS bundle at $(J,\varphi)$, then they are componentwise $2\cdot$microWidth-close. Exact $O(1)$-complexity uniqueness is not encoded yet; this lemma is the scalar engine that turns “both near the reference” into “near each other,” applied componentwise across the observable bundle.
In the broader Recognition exclusivity story, that surrogate is what can be proved cleanly while the sharper uniqueness claim remains open. The lemma itself is framework-agnostic real analysis, but it is the hinge between micro-window membership and componentwise closeness in the prediction-map uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.