rs_within_micro_window
plain-language theorem explainer
The RS dimensionless observable bundle lies in every nonnegative micro-window centered on itself. Exclusivity and prediction-map arguments cite this reflexivity when treating the RS bundle as the reference point of a micro-window uniqueness surrogate. The proof unfolds componentwise closeness and simplifies: self-distance is zero once ε ≥ 0.
Claim. For every real $\varepsilon \ge 0$, the Recognition Science dimensionless observable bundle lies inside the micro-window of half-width $\varepsilon$ about itself: each component is componentwise at most $\varepsilon$ from the corresponding RS value.
background
The module builds a prediction map from admissible Recognition Structure data to a bundle of dimensionless observables, then compares maps by componentwise closeness. The RS cost is the standard J-cost $J(x)=(x+x^{-1})/2-1$ on positive ratios (the unique cost forced by the Recognition Composition Law in the T5 step of the forcing chain). The golden ratio $\phi$ is the self-similar fixed point (T6).
rsObservables is the concrete RS bundle at that $(J,\phi)$ reference. A micro-window of half-width $\varepsilon$ is the set of bundles whose components each differ from a reference by at most $\varepsilon$ (via componentwiseClose). The predicate withinMicroWindow ε O asserts that $O$ sits inside the micro-window of width $\varepsilon$ about the RS bundle.
The surrounding scaffold reformulates exact O(1)-complexity uniqueness as a bounds-uniqueness surrogate: maps that both land in a fixed $10^{-6}$ micro-window about RS are componentwise $2\cdot 10^{-6}$-close to each other.
proof idea
Term-style tactic proof. Unfold withinMicroWindow and the underlying componentwiseClose predicate, exposing componentwise absolute deviations between rsObservables and itself. Those deviations are identically zero. simp with the hypothesis $\varepsilon \ge 0$ discharges every inequality $0 \le \varepsilon$. No external lemmas are required beyond definitional unfolding.
why it matters
This is the reflexivity half of the micro-window comparison used in the exclusivity/prediction-map layer. The module's Open Problem 2 reformulation states that exact O(1)-complexity uniqueness is not yet encoded; what is clean is a bounds-uniqueness surrogate around the RS bundle at $(J_{\mathrm{cost}},\phi)$. Placing RS inside every nonnegative micro-window about itself makes that reference well-defined and lets later closeness lemmas (e.g. two maps inside the same window are mutually close) fire without a special case.
It sits next to rs_within_bounds, close_to_same_reference, and the bridge asserting existence of the RS prediction map. Framework landmarks in play are T5 J-uniqueness and T6 $\phi$ as the fixed point that pin the RS reference bundle. No downstream consumers are wired yet (used_by is empty); the lemma is infrastructure for the uniqueness surrogate rather than a physics prediction itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.