IndisputableMonolith.Verification.Exclusivity.PredictionMap
Defines the RS observable bundle: a finite list of dimensionless predictions (mass ratios, coupling windows, geometric factors) fixed by the phi-ladder and J-cost. Verification and exclusivity arguments cite it to compare any candidate theory against the same reference vector. The module is mostly structure and predicates, with existence of the RS map discharged by a named bridge lemma.
claimThe module packages a dimensionless observable vector $O_{\mathrm{RS}}$ built from RS constants ($\varphi$, $J$-cost normalizations, rung gaps) together with predicates that a predictor $P$ lies inside macroscopic bounds or a micro-window of $O_{\mathrm{RS}}$, and asserts that an RS prediction map realizing those observables exists.
background
Recognition Science fixes dimensionless numbers from a single cost functional $J$ and the golden ratio $\varphi$ (self-similar fixed point of the forcing chain). Dimensionful units drop out; what remains is a finite bundle of pure numbers: coupling inverses in a narrow band, mass ratios on the $\varphi$-ladder, and geometric thresholds such as the Berry scale $\varphi^{-1}$.
This module sits in the exclusivity/verification layer. It imports RS constants ($\tau_0 = 1$ tick and related native units) and the cost layer that supplies $J$. Sibling definitions introduce the observable record, the concrete RS filling of that record, a generic Predictor type, componentwise closeness, and micro-window width around the RS reference.
The theoretical job is bookkeeping: fix one reference vector so that later uniqueness or bridge theorems can say "any admissible predictor is componentwise near $O_{\mathrm{RS}}$" without re-deriving each constant.
proof idea
Definition-and-predicate module, not a deep proof development. It declares the observable bundle type, populates the RS instance from Constants and Cost, and defines bounds checks (withinBounds, micro-window predicates, componentwise closeness). The sole substantial claim is existence of the RS prediction map, recorded as a bridge lemma that wires the concrete RS observables into the abstract Predictor interface. Remaining lemmas are mostly unfolding and arithmetic comparison against fixed numeric windows.
why it matters in Recognition Science
Exclusivity arguments need a single, named target: the dimensionless fingerprint RS actually predicts. Without this map, "agrees with RS" is informal. The bundle feeds bridge B5-style statements that an admissible predictor exists and lies inside the RS micro-window, which in turn support claims that rival frameworks either reproduce the same vector or exit the allowed band (e.g. the $\alpha^{-1}$ window near $137.03$--$137.04$).
Downstream exclusivity and verification developments (even when not yet linked in the graph) are expected to quote rsPredictionMap and the micro-window lemmas rather than inlining constant lists. The module therefore anchors the empirical face of the forcing chain (T5--T8 and the mass ladder) inside the formal verification stack.
scope and limits
- Does not derive the numeric values of the observables from the forcing chain inside this file.
- Does not prove uniqueness of predictors; only packages the RS reference and closeness predicates.
- Does not address dimensionful units or experimental error models beyond fixed micro-windows.
- Does not itself close exclusivity; it only supplies the prediction target other modules compare against.
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