IndisputableMonolith.Verification.Exclusivity.PredictionMap
Defines the RS observable bundle: a finite list of dimensionless predictions (mass ratios, coupling windows, geometric invariants) extracted from the Recognition programme. Supplies the Predictor interface, the concrete RS prediction map, and micro-window closeness predicates used by exclusivity arguments. Mostly definitions and elementary bound lemmas; no deep analytic work lives here.
claimThe module packages a dimensionless observable vector $O_{\mathrm{RS}}$ (mass ladder ratios, $\alpha^{-1}$ band, geometric constants) together with a predictor map $P$ and predicates $\mathrm{withinBounds}$, $\mathrm{withinMicroWindow}$ asserting that a candidate theory's predictions lie inside prescribed absolute or micro-width tolerances of the RS reference values.
background
Recognition Science fixes dimensionless observables once the forcing chain has selected $J(x)=\cosh(\log x)-1$, the golden ratio $\varphi$ as self-similar fixed point, the eight-tick period, and $D=3$. Masses sit on the $\varphi$-ladder; $\alpha^{-1}$ is constrained to a narrow numerical band; $c$, $\hbar$, $G$ are fixed in RS-native units.
This module sits in the Verification/Exclusivity layer. It does not re-derive those constants. It only packages the resulting dimensionless numbers into a single observable bundle and defines what it means for another predictor to match that bundle inside stated tolerances. Upstream imports supply $\tau_0$ (the RS tick) and the $J$-cost infrastructure; the numerical values themselves come from Constants.
Sibling definitions introduce DimensionlessObservables, the concrete rsObservables vector, a generic Predictor type, the RS instance rsPredictionMap, and two closeness relations: componentwise absolute bounds and a tighter micro-window of width microWidth.
proof idea
Definition module with thin wrapper lemmas. The observable record and predictor interface are pure data. rs_within_bounds and rs_within_micro_window are direct evaluations of the RS numbers against the stated tolerances. bridge_B5_prediction_map_exists asserts that the RS predictor inhabits the abstract Predictor type. close_to_same_reference is an elementary transitivity/identity fact for the closeness relations. No substantial proof burden is carried here.
why it matters in Recognition Science
Exclusivity arguments need a single, named target: the list of numbers any rival framework must hit. This module is that target. Downstream exclusivity bridges (B5 and related uniqueness claims) quantify over predictors and demand they land inside the RS micro-window; without a canonical observable bundle those statements have nothing to compare against. The module therefore closes the interface between the constructive RS constants and the meta-theoretic claim that no inequivalent predictor reproduces the same dimensionless physics. It does not itself prove exclusivity; it only fixes the prediction map that exclusivity talks about.
scope and limits
- Does not derive mass-ladder rungs, alpha band, or geometric constants; only packages them.
- Does not prove exclusivity or uniqueness of RS among predictors.
- Does not address dimensionful units or experimental error models beyond fixed micro-widths.
- Does not supply numerical certificates; bounds are definitional or trivial evaluations.
- Does not constrain predictors outside the listed dimensionless components.
depends on (2)
declarations in this module (14)
-
structure
DimensionlessObservables -
def
rsObservables -
def
withinBounds -
theorem
rs_within_bounds -
structure
Predictor -
def
rsPredictionMap -
theorem
bridge_B5_prediction_map_exists -
def
componentwiseClose -
def
withinMicroWindow -
def
microWidth -
theorem
close_to_same_reference -
theorem
rs_within_micro_window -
theorem
prediction_map_unique -
theorem
prediction_map_matches_bounds