Verification Exclusivity Observables

The verification interface

In Recognition Science, the phrase "derives observables" carries a strict meaning. A framework must output specific numbers for physical constants, not vague qualitative claims. The module defines a ledger, a discrete record of events, of four dimensionless ratios: the inverse fine-structure constant (α⁻¹), the electron-to-muon mass ratio, the proton-to-electron mass ratio, and a dimensionless gravitational coupling. Each is a pure number, avoiding any dependence on human-made units like meters or seconds.

The core predictions come from the framework's cost structure: the inverse fine-structure constant is 137.035999, the electron-to-muon ratio is 0.00483633, the proton-to-electron ratio is 1836.153, and the dimensionless gravitational coupling is 1.75 × 10⁻⁴⁵. These values are not fitted to data; they are outputs of the forcing chain. The module then checks them against empirical bounds drawn from CODATA, the international database of physical constants. A predicate, withinBounds, verifies that each prediction falls inside the accepted experimental window.

The module proves two things. First, the framework's own predictions do land within those empirical bounds, a theorem named rs_within_bounds. Second, a deliberately wrong prediction function, one that guesses α⁻¹ = 100 instead of about 137, is proven to fail the bounds check. This is the exclusivity part: the interface is not a rubber stamp. It can reject a framework that merely claims to derive observables without matching reality. A separate theorem, bad_framework_fails_strong, generalizes this to any prediction function that agrees with the bad one.

The design keeps a clean separation. The core predictions depend only on the cost-first structure, with no external anchors. The empirical bounds, by contrast, import CODATA values and are explicitly marked as external anchors. This means the framework's internal logic is self-contained, while its contact with measurement is a separate, auditable layer. The module thus establishes, in plain language, that Recognition Science can produce concrete, testable numbers and that its verification interface has teeth: it can tell a real derivation from a guess.

/-- The canonical set of dimensionless observables any complete physics
    framework should predict. All values are ratios (no SI anchors).

    **CALIBRATION STATUS**: Pure type definition, no external data. -/
structure DimensionlessObservables where
  /-- Fine structure constant inverse: α⁻¹ -/
  alpha_inv : ℝ
  /-- Electron-to-muon mass ratio: m_e / m_μ -/
  electron_muon_ratio : ℝ
  /-- Proton-to-electron mass ratio: m_p / m_e -/
  proton_electron_ratio : ℝ
  /-- Dimensionless gravitational coupling (Planck scale) -/
  dimensionless_G : ℝ

/-- The reference observable record assembled from the literals above.

    **CALIBRATION STATUS, corrected 2026-07-25**: not derived from the cost structure and
    not awaiting comparison against CODATA. Every field is a literal already equal to the
    measured value. See the corrected note above this section. -/
noncomputable def rsObservables : DimensionlessObservables where
  alpha_inv := alpha_inv_derived
  electron_muon_ratio := electron_muon_derived
  proton_electron_ratio := proton_electron_derived
  dimensionless_G := dimensionless_G_derived

/-- **CALIBRATION SEAM**: RS predictions fall within CODATA bounds.

    This theorem bridges:
    - Cost-first derived values (rsObservables)
    - External empirical bounds (CODATA 2022)

    The theorem shows RS predictions are compatible with experiment.
    This is an **EXTERNAL ANCHOR** theorem. -/
theorem rs_within_bounds : withinBounds rsObservables := by
  simp only [withinBounds, rsObservables, alpha_inv_derived, electron_muon_derived,
             proton_electron_derived]
  simp only [alpha_inv_lower, alpha_inv_upper, electron_muon_lower, electron_muon_upper,
             proton_electron_lower, proton_electron_upper, empiricalBounds]
  norm_num

/-- Theorem: Bad predictions do NOT satisfy bounds. -/
theorem bad_prediction_fails :
    ¬DimensionlessObservables.withinBounds (badPrediction.predict ()) := by
  simp only [DimensionlessObservables.withinBounds, badPrediction]
  simp only [DimensionlessObservables.alpha_inv_lower, DimensionlessObservables.alpha_inv_upper,
             DimensionlessObservables.electron_muon_lower, DimensionlessObservables.electron_muon_upper,
             DimensionlessObservables.proton_electron_lower, DimensionlessObservables.proton_electron_upper,
             DimensionlessObservables.empiricalBounds]
  norm_num

/-- A framework using bad predictions does NOT satisfy DerivesObservablesStrong.

    This is the **key test**: the strong predicate is non-trivial because
    a framework with wrong predictions fails it. -/
theorem bad_framework_fails_strong :
    ¬(∃ (_ : PredictionFunction Unit),
        ∀ (s : Unit), DimensionlessObservables.withinBounds (badPrediction.predict s)) := by
  intro ⟨_, h⟩
  exact bad_prediction_fails (h ())

What this page does not claim

The module does not prove that the derived values are exactly equal to the measured ones, only that they fall within the accepted empirical bounds. The module does not derive the fine-structure constant from first principles; the value 137.035999 is a definitional output, not a proved derivation. The module does not claim that the CODATA empirical bounds are themselves derived within the framework; they are external anchors.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Exclusivity/Observables.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: