Pith. sign in
module module moderate

IndisputableMonolith.Verification.Exclusivity.Observables

show as:
view Lean formalization →

Canonical package of dimensionless observables any complete physics framework should predict: inverse fine-structure constant, lepton and nucleon mass ratios, and a dimensionless gravitational coupling, all pure ratios with no SI anchors. Recognition Science fills the slots from phi-ladder and RCL-derived constants. Exclusivity and verification arguments cite the type when testing whether predictions fall inside empirical bands. Pure type and bound infrastructure; no external data in the definitions.

claimDefines a record of dimensionless observables $(\alpha^{-1}, m_\mu/m_e, m_p/m_e, G_{\mathrm{dimless}})$, RS-derived values for each, empirical bound intervals, a predicate that a prediction lies inside those bounds, and interfaces (prediction map; strong derivation) asserting a framework produces the full set as ratios only.

background

Recognition Science derives physics from the Recognition Composition Law and the forcing chain, with RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and $\alpha^{-1}$ targeted inside $(137.030,137.039)$. Mass ratios sit on the phi-ladder (yardstick times $\varphi$ to a rung offset). Experiment comparison is quarantined: ExternalAnchors is the single home for CODATA and empirical calibration so the cost-first core never mixes SI data into definitions.

This module lives under Verification.Exclusivity. It names the canonical dimensionless ratios a complete framework must hit. DimensionlessObservables is a pure type (doc: no external data). Sibling slots such as alpha_inv_derived, electron_muon_derived, proton_electron_derived, and dimensionless_G_derived are the RS-filled values; rsObservables bundles them. EmpiricalBounds / empiricalBounds and withinBounds / rs_within_bounds gate comparison to anchor bands. PredictionFunction and DerivesObservablesStrong are the interfaces exclusivity proofs use.

proof idea

This is a definition module, not a proof of physical claims. It introduces the DimensionlessObservables record, RS-populated instances (per-observable derived values and rsObservables), EmpiricalBounds with a concrete empiricalBounds witness, the withinBounds predicate and rs_within_bounds, plus PredictionFunction and DerivesObservablesStrong as type-level interfaces. Dependencies are Constants (RS-native units, $\tau_0$) and ExternalAnchors (quarantined CODATA). No tactic proof burden beyond structural wiring.

why it matters in Recognition Science

Exclusivity needs a fixed, unit-free target: which numbers must a rival framework reproduce? This module supplies that target so downstream Verification.Exclusivity arguments can say a framework derives the observables and lands inside bounds without smuggling SI units into the core. Parent use is the exclusivity stack built on DerivesObservablesStrong, withinBounds, and rs_within_bounds (siblings in-module; no external used_by edges in the graph snapshot).

Calibration status is intentional: pure type definition. Empirical bite comes only through ExternalAnchors. Framework landmarks in play are the alpha band, phi-ladder mass ratios, and dimensionless $G$ from the RS-native package $G=\varphi^5/\pi$ with $c=1$, $\hbar=\varphi^{-5}$.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)