microWidth
plain-language theorem explainer
Fixes the default micro-window half-width at $10^{-6}$ for the bounds-uniqueness surrogate on dimensionless RS observables. Anyone citing the prediction-map uniqueness argument uses this constant as the shared tolerance around the RS bundle at $(J,\varphi)$. It is a one-line real literal, not a derived quantity.
Claim. The default micro-window width is the real number $\varepsilon = 10^{-6}$, used as the half-width of the neighborhood around the Recognition Science observable bundle in which two admissible predictors are compared.
background
In the exclusivity verification layer, exact uniqueness of an $O(1)$-complexity prediction map is not yet encoded. The scaffold instead proves a bounds-uniqueness surrogate: predictors that both land inside a tiny window around the RS reference values must be componentwise close to each other.
The reference bundle is evaluated at the J-cost and the golden ratio $\varphi$. The micro-window is the $\varepsilon$-neighborhood of that bundle in the space of dimensionless observables. Sibling notions include componentwise closeness and the predicate that a predicted tuple lies within the micro-window of a given width.
This constant simply names the conventional $\varepsilon = 10^{-6}$ used throughout that argument, matching the $10^{-6}$ figure in the open-problem reformulation for prediction-map uniqueness.
proof idea
Pure definition: the real literal $1\times 10^{-6}$. No lemmas, tactics, or algebraic reduction. Downstream theorems treat it as a fixed positive scale parameter.
why it matters
Feeds prediction_map_unique, the reformulation of Open Problem 2: if two admissible predictors both lie inside the $10^{-6}$ micro-window around the RS bundle at $(J_{\mathrm{cost}},\varphi)$, then they are componentwise $2\cdot 10^{-6}$-close. Naming the width keeps the uniqueness surrogate readable and lets the factor-of-two triangle inequality stay explicit.
In the broader Recognition framework this is bookkeeping for verification exclusivity, not a forcing-chain step (T0–T8). It anchors the numerical tolerance against which competing prediction maps are judged near the RS fixed point, without claiming exact uniqueness of the map itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.