IndisputableMonolith.Verification.Exclusivity.Observables
Defines the canonical bundle of dimensionless observables that any complete physics framework must predict: inverse fine-structure constant, mass ratios, and a dimensionless gravitational coupling, all as pure ratios with no SI anchors. Verification and exclusivity arguments cite this bundle when comparing Recognition Science predictions to empirical bands. The module is pure type and data structure; no theorems are proved here.
claimA record of dimensionless observables $(\alpha^{-1}, m_\mu/m_e, m_p/m_e, G_{\mathrm{dimless}})$ together with RS-derived values, empirical bound intervals, a predicate that a prediction lies inside those bounds, and a strong derivation interface asserting that a framework produces the full bundle from its internal constants.
background
Recognition Science works in RS-native units ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and forces dimensionless structure from the Recognition Composition Law and the T0–T8 chain. Comparison with experiment therefore cannot lean on SI yardsticks; it must use pure ratios.
This module sits in the Verification/Exclusivity layer. It imports Constants (the RS time quantum $\tau_0=1$ tick and related native constants) and ExternalAnchors (the single quarantined home for CODATA and empirical calibration). The design keeps the cost-first core free of external data while still enabling a clean match against measured bands.
The central type packages inverse fine structure, electron–muon and proton–electron mass ratios, and a dimensionless $G$. Companion structures hold RS-derived numbers, empirical intervals, and a within-bounds predicate.
proof idea
This is a definition module, no proofs. It introduces the DimensionlessObservables record, named RS-derived fields (alpha inverse, lepton and baryon mass ratios, dimensionless $G$), an EmpiricalBounds bundle with a concrete empiricalBounds instance, the predicate withinBounds, a packaged rsObservables value, and interfaces PredictionFunction and DerivesObservablesStrong for frameworks that claim to derive the full set.
why it matters in Recognition Science
Exclusivity arguments need a fixed, SI-free target: what every complete framework must hit. This module supplies that target so downstream verification can state "RS lies inside empirical bands" and "a rival framework either derives the same bundle or fails."
It connects the forced RS constants (phi-ladder masses, alpha band near $137.03$–$137.04$, native $G$) to the quarantined external anchors without polluting the forcing chain. Sibling names such as rs_within_bounds and DerivesObservablesStrong are the natural consumers; the module itself has no further used-by edges in the graph snapshot.
Calibration status is explicit: pure types and derived placeholders, no smuggled experimental inputs in the definitions.
scope and limits
- Does not prove that RS predictions match experiment; only defines the observable bundle and bounds types.
- Does not import or assert CODATA numerics inside the core definitions; anchors stay quarantined.
- Does not derive alpha, mass ratios, or G; those live in upstream constants and mass-ladder modules.
- Does not claim exclusivity or completeness of the observable list beyond the packaged ratios.
- Does not address dimensionful SI units or absolute mass scales.
depends on (2)
declarations in this module (19)
-
structure
DimensionlessObservables -
def
alpha_inv_derived -
def
electron_muon_derived -
def
proton_electron_derived -
def
dimensionless_G_derived -
def
rsObservables -
structure
EmpiricalBounds -
def
empiricalBounds -
def
withinBounds -
theorem
rs_within_bounds -
structure
PredictionFunction -
def
DerivesObservablesStrong -
structure
DerivesObservablesWitness -
def
unitPrediction -
def
rsDerivesObservables -
theorem
rs_derives_observables_strong -
def
badPrediction -
theorem
bad_prediction_fails -
theorem
bad_framework_fails_strong