componentwiseClose
plain-language theorem explainer
Two dimensionless observable bundles are componentwise ε-close when α⁻¹, m_e/m_μ, and m_p/m_e each differ by at most ε. Exclusivity and prediction-map arguments cite this as the metric on the RS observable triple. The body is a pure three-clause absolute-value definition, not a proved theorem.
Claim. For $\varepsilon\in\mathbb{R}$ and dimensionless observable bundles $o_1,o_2$ (each a triple $(\alpha^{-1},\,m_e/m_\mu,\,m_p/m_e)$), write $\mathrm{close}_\varepsilon(o_1,o_2)$ when $|\alpha^{-1}(o_1)-\alpha^{-1}(o_2)|\le\varepsilon$, $|m_e/m_\mu(o_1)-m_e/m_\mu(o_2)|\le\varepsilon$, and $|m_p/m_e(o_1)-m_p/m_e(o_2)|\le\varepsilon$.
background
In the exclusivity verification layer, a complete framework is asked to output a fixed bundle of dimensionless ratios: the inverse fine-structure constant $\alpha^{-1}$, the electron-to-muon mass ratio $m_e/m_\mu$, and the proton-to-electron mass ratio $m_p/m_e$. The local structure packages exactly those three reals; no SI anchors appear.
The module builds a prediction map from the RS cost $J$ and the golden ratio $\phi$ into that bundle, then compares rival predictors by how near their outputs sit to the RS reference triple. Componentwise closeness is the elementary $\ell^\infty$-style relation used for that comparison: a single tolerance $\varepsilon$ bounds every coordinate gap.
Upstream, the same triple type is the canonical observable set any complete physics framework should predict. Active-edge and anchor constants ($A=1$, coherence scale $\phi^{-5}$) sit behind the RS numerical values, but this definition itself is pure comparison geometry on the triple.
proof idea
Pure definition (no proof obligations). The predicate is the conjunction of three absolute-value inequalities, one per field of the dimensionless observable structure. Downstream lemmas unfold it and discharge the inequalities by simp or triangle inequality.
why it matters
This is the comparison primitive for Open Problem 2 in the exclusivity scaffold. The micro-window around the RS bundle is defined by applying the predicate to a candidate and the RS reference triple. The RS bundle lies in every nonnegative micro-window of itself by unfolding and nonnegativity of $\varepsilon$.
The bounds-uniqueness surrogate then states: if two admissible predictors both land inside the default $10^{-6}$ micro-window around the RS values at $(J,\phi)$, their outputs are componentwise $2\cdot 10^{-6}$-close. Exact $O(1)$-complexity uniqueness is not encoded; this $\varepsilon$-closeness surrogate is what the scaffold can prove cleanly. Framework landmarks in play are the RS $\alpha^{-1}$ band and the $\phi$-ladder mass ratios that fill the three coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.