withinMicroWindow
plain-language theorem explainer
Predicate that a dimensionless observable triple lies inside an ε-neighborhood of the Recognition Science reference bundle (α⁻¹, m_e/m_μ, m_p/m_e). Citation target for the bounds-uniqueness surrogate around the RS prediction map. Defined by reducing to componentwise closeness against the fixed RS values.
Claim. For $\varepsilon\in\mathbb{R}$ and an observable triple $o=(\alpha^{-1},\,m_e/m_\mu,\,m_p/m_e)$, write $\mathrm{withinMicroWindow}(\varepsilon,o)$ when each coordinate of $o$ is within absolute distance $\varepsilon$ of the corresponding RS reference value.
background
In the exclusivity verification layer, predictions are packaged as a dimensionless triple: inverse fine-structure constant, electron-to-muon mass ratio, and proton-to-electron mass ratio. The RS programme supplies a fixed reference triple rsObservables built from the cost-first ledger (J-cost and φ).
A micro-window is the product neighborhood of half-width ε around that reference. Componentwise closeness means each coordinate differs from the RS value by at most ε in absolute value. The module uses this as a clean surrogate for exact uniqueness of prediction maps at the pair (J-cost, φ), avoiding an O(1)-complexity uniqueness claim that is still open in the scaffold.
Related width notions appear elsewhere (interval width as hi−lo), but here the window is a fixed ε-ball in the three observable coordinates, not an interval certificate.
proof idea
Pure definitional abbreviation: unfold to componentwise closeness of the given observable triple to the RS reference triple at tolerance ε. No tactics, no lemmas.
why it matters
Anchors the reformulated Open Problem 2 in this module: exact uniqueness of admissible predictors is not encoded; instead one proves a bounds-uniqueness surrogate. If two predictors both land inside the same micro-window of width microWidth (default 10⁻⁶) around the RS bundle at (J-cost, φ), then their outputs are componentwise 2·microWidth-close (prediction_map_unique).
Also used by the trivial self-membership fact that the RS bundle sits in every nonnegative micro-window about itself (rs_within_micro_window). Together these give a verifiable exclusivity statement: RS predictions are the unique point that every admissible map must approach inside a fixed micro-tolerance, tying verification language to the forced constants (φ, J) without claiming full complexity-theoretic uniqueness yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.