IndisputableMonolith.Foundation.MaximalForcing.RSAlphaUniverse

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2import IndisputableMonolith.Numerics.Interval.AlphaBounds
   3
   4/-!
   5# Maximal Forcing: the alpha layer (Phase 2 extension, fine-structure constant)
   6
   7Fourth concrete instantiation, reaching a physics-adjacent quantity rather than a
   8structural primitive. NB this layer forces a WINDOW (band containment) of the RS
   9**construction value**, not the measured constant: the seed 44π = 4π·11 is an
  10identification, not a derived coupling, so the exact infrared α⁻¹(0) = 137.035999
  11remains a boundary condition, OPEN (see `Verification.EMAlphaCert`). What is forced
  12here is precisely "the construction lands in the CODATA-bracketing window," which
  13is a real, non-vacuous claim about the parameter-free formula, not a derivation of α.
  14
  15* The realization carrier is a candidate inverse fine-structure value `a : ℝ`.
  16* The loose class `Lalpha0` is every candidate real.
  17* The gate class `LalphaRS` pins `a` to the RS construction value
  18  `alphaInv = 44π · exp(-w8·ln φ / 44π)` (no fitted parameters; seed 44π OPEN).
  19* The claim under closure is "a lies in the CODATA-bracketing window
  20  (137.030, 137.039)."
  21
  22Over `LalphaRS`, the window claim is forced, wrapping the proved interval bounds
  23`Numerics.alphaInv_gt` and `Numerics.alphaInv_lt`. Over `Lalpha0` it is
  24independent: the RS construction value is in the window, but `0` is not. The RS
  25assembly does real work; the window is forced by the parameter-free construction,
  26even though the construction itself is not a derivation of the measured α.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace MaximalForcing
  32
  33open IndisputableMonolith.Constants (alphaInv)
  34open IndisputableMonolith.Numerics (alphaInv_gt alphaInv_lt)
  35
  36/-- Loosest alpha class `Lalpha0`: every candidate value. -/
  37def Lalpha0 : AdmissibilityClass ℝ where
  38  admissible := Set.univ
  39  label := "every candidate inverse-coupling value"
  40
  41/-- Gate-tightened alpha class `LalphaRS`: the candidate equals the RS-assembled
  42inverse fine-structure value. -/
  43def LalphaRS : AdmissibilityClass ℝ where
  44  admissible := { a | a = alphaInv }
  45  label := "RS-assembled inverse coupling: a = 44π·exp(-w8·ln φ/44π)"
  46
  47/-- `LalphaRS` is a tightening of `Lalpha0`. -/
  48def tighten_Lalpha0_LalphaRS : Tightening Lalpha0 LalphaRS where
  49  subset := by
  50    intro a _
  51    trivial
  52  strict_witness := True
  53
  54/-- The forced claim of the alpha layer: the value lies in the CODATA-bracketing
  55window `(137.030, 137.039)`. -/
  56def isAlphaWindowClaim : RealityClaim ℝ where
  57  label := "137.030 < a < 137.039"
  58  holds := fun a => (137.030 : ℝ) < a ∧ a < (137.039 : ℝ)
  59
  60/-- The alpha-layer claim universe. -/
  61def alphaUniverse : ClaimUniverse where
  62  Realization := ℝ
  63  admissibility := LalphaRS
  64  claims := { isAlphaWindowClaim }
  65
  66/-- **Alpha window as a forced invariant.** Over the RS-assembly gate, the value
  67lies in `(137.030, 137.039)`. Wraps the proved bounds; the only external content
  68is interval arithmetic, no fitted parameter. -/
  69theorem forced_alphaWindow : Forced LalphaRS.admissible isAlphaWindowClaim := by
  70  intro a ha
  71  have ha' : a = alphaInv := ha
  72  subst ha'
  73  exact ⟨alphaInv_gt, alphaInv_lt⟩
  74
  75/-- The claim `isAlphaWindowClaim` is in the closure of the alpha universe. -/
  76theorem isAlphaWindowClaim_in_closure :
  77    InClosure Primitive.lawOfLogic alphaUniverse isAlphaWindowClaim := by
  78  show isAlphaWindowClaim ∈ alphaUniverse.claims
  79  exact Set.mem_singleton _
  80
  81/-- Forced-register entry for the fine-structure window. -/
  82def alphaForcedInvariant : ForcedInvariant Primitive.lawOfLogic alphaUniverse where
  83  claim := isAlphaWindowClaim
  84  in_closure := isAlphaWindowClaim_in_closure
  85  forced := forced_alphaWindow
  86
  87/-- The alpha-layer universe is fully classified. -/
  88theorem alphaUniverse_classifier :
  89    ∀ C : RealityClaim alphaUniverse.Realization,
  90      InClosure Primitive.lawOfLogic alphaUniverse C → ClaimClassification alphaUniverse C := by
  91  intro C hC
  92  have hCeq : C = isAlphaWindowClaim := Set.mem_singleton_iff.mp hC
  93  subst hCeq
  94  exact ClaimClassification.forced forced_alphaWindow
  95
  96/-- A real `MaximalClosureCert` for the alpha-layer universe. -/
  97def alphaUniverseCert : MaximalClosureCert Primitive.lawOfLogic alphaUniverse where
  98  classifies := alphaUniverse_classifier
  99
 100/-! ## The RS-assembly gate does real work -/
 101
 102/-- Over the loose class `Lalpha0`, the window claim is independent: the RS value
 103satisfies it, and `0` does not. -/
 104theorem alphaWindow_independent_over_Lalpha0 :
 105    Independent Lalpha0.admissible isAlphaWindowClaim := by
 106  refine ⟨alphaInv, 0, ?_, ?_, ?_, ?_⟩
 107  · trivial
 108  · trivial
 109  · exact ⟨alphaInv_gt, alphaInv_lt⟩
 110  · intro h
 111    have h1 : (137.030 : ℝ) < 0 := h.1
 112    norm_num at h1
 113
 114/-- **The RS-assembly tightening is legitimate, not cheap.** The window claim is
 115independent over `Lalpha0` but forced over `LalphaRS`. -/
 116theorem tightening_Lalpha0_LalphaRS_effective :
 117    Independent Lalpha0.admissible isAlphaWindowClaim ∧
 118    Forced LalphaRS.admissible isAlphaWindowClaim :=
 119  ⟨alphaWindow_independent_over_Lalpha0, forced_alphaWindow⟩
 120
 121end MaximalForcing
 122end Foundation
 123end IndisputableMonolith
 124