IndisputableMonolith.Constants.AlphaGenesis.ResidualTarget

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.Alpha
   4import IndisputableMonolith.Constants.ExternalAnchors
   5import IndisputableMonolith.Constants.AlphaGenesis.LoopCertificate
   6import IndisputableMonolith.Foundation.MeasureForcing
   7import IndisputableMonolith.Numerics.Interval.AlphaBounds
   8
   9/-!
  10# Alpha Genesis M4: The Residual Target (quarantine module)
  11
  12**QUARANTINE.** This is the ONLY Alpha Genesis module that references the
  13measured value. M1–M3 (the derivation) are blind to CODATA by construction;
  14this module states the comparison and the open target, and nothing in M1–M3
  15depends on it.
  16
  17## What this module proves
  18
  191. `residual_bounds`: the certified band confines the residual
  20   `alphaInv − α⁻¹_CODATA` to `(−0.006, 0.0031)`.
  212. `correctedAlphaInv`: with the response forced (M1), any second-order
  22   correction must enter as ADDITIONAL SPECTRAL LOAD (multiplicatively, in
  23   the exponent), never as an additive display patch. The legacy additive
  24   tail `δ_κ = −103/(102π⁵)` belongs to the excluded form-(A) display
  25   (`DressingResponse.no_additive_response`) and is retired from the
  26   structural pipeline (it was already removed from the certified value).
  273. `closingLoad` exists and is UNIQUE: there is exactly one second-order
  28   load `δ₂` for which the dressed value equals the measured value
  29   (`corrected_eq_codata_iff`). The open problem is therefore sharply
  30   localized: derive this one number from voxel seam geometry, blind.
  31
  32## The open target (OPEN, expected closure)
  33
  34Derive `δ₂` from the seam topology of the D=3 voxel lattice with a
  35procedure that never references CODATA, and publish the result either way.
  36
  37* If the blind derivation lands on `closingLoad` (within stated tolerance),
  38  the α derivation closes at experimental precision.
  39* If it lands elsewhere, the channel-budget bridge (the one named input of
  40  M3) is wrong and the assembly is falsified at that layer.
  41
  42**Anti-epicycle rule (binding):** no candidate `δ₂` may be admitted to the
  43certified surface on the basis of numerical proximity to `closingLoad`.
  44Admission requires a forced derivation from lattice geometry. The candidate
  45catalogue of `Verification/AlphaCorrectionAnalysis.lean` is a search record,
  46not a derivation, and must not be cited as one.
  47
  48STATUS: THEOREM for 1–3; OPEN (expected closure) for the seam derivation.
  49-/
  50
  51namespace IndisputableMonolith
  52namespace Constants
  53namespace AlphaGenesis
  54
  55noncomputable section
  56
  57open Constants.ExternalAnchors
  58
  59/-- The signed residual of the (first-order) genesis value against CODATA. -/
  60def residual : ℝ := Constants.alphaInv - alpha_inv_CODATA
  61
  62/-- The certified band confines the residual to `(−0.006, 0.0031)`. -/
  63theorem residual_bounds : (-0.006 : ℝ) < residual ∧ residual < (0.0031 : ℝ) := by
  64  unfold residual
  65  have hgt := Numerics.alphaInv_gt
  66  have hlt := Numerics.alphaInv_lt
  67  have hC : alpha_inv_CODATA = (137.035999177 : ℝ) := rfl
  68  constructor
  69  · rw [hC]; linarith
  70  · rw [hC]; linarith
  71
  72/-- **The load-form correction.** With the response forced (M1), any
  73second-order term enters as additional spectral load in the exponent. -/
  74def correctedAlphaInv (δ₂ : ℝ) : ℝ :=
  75  channelBudget * Foundation.MeasureForcing.contWeight (spectralLoad + δ₂)
  76
  77/-- Zero correction recovers the first-order genesis value. -/
  78theorem corrected_at_zero : correctedAlphaInv 0 = alphaInvGenesis := by
  79  unfold correctedAlphaInv alphaInvGenesis
  80  rw [add_zero]
  81
  82/-- **The unique closing load**: the one value of `δ₂` aligning the dressed
  83value with CODATA, written in closed form. This is the sharply localized
  84open target: derive THIS number from seam geometry, blind. -/
  85def closingLoad : ℝ :=
  86  Real.log (alpha_inv_CODATA / channelBudget) / Real.log Foundation.MeasureForcing.rho
  87    - spectralLoad
  88
  89/-- `log ρ ≠ 0` (ρ = 1/φ ∈ (0,1)). -/
  90theorem log_rho_ne_zero : Real.log Foundation.MeasureForcing.rho ≠ 0 := by
  91  have hneg : Real.log Foundation.MeasureForcing.rho < 0 :=
  92    Real.log_neg Foundation.MeasureForcing.rho_pos Foundation.MeasureForcing.rho_lt_one
  93  exact ne_of_lt hneg
  94
  95/-- The closing load closes: `correctedAlphaInv closingLoad = α⁻¹_CODATA`. -/
  96theorem corrected_at_closingLoad :
  97    correctedAlphaInv closingLoad = alpha_inv_CODATA := by
  98  unfold correctedAlphaInv closingLoad
  99  have hb : (0 : ℝ) < channelBudget := channelBudget_pos
 100  have hb' : channelBudget ≠ 0 := ne_of_gt hb
 101  have hC : (0 : ℝ) < alpha_inv_CODATA := alpha_inv_CODATA_pos
 102  have hratio : (0 : ℝ) < alpha_inv_CODATA / channelBudget := div_pos hC hb
 103  have hexp : spectralLoad +
 104      (Real.log (alpha_inv_CODATA / channelBudget) / Real.log Foundation.MeasureForcing.rho
 105        - spectralLoad)
 106      = Real.log (alpha_inv_CODATA / channelBudget) / Real.log Foundation.MeasureForcing.rho := by
 107    ring
 108  rw [hexp]
 109  show channelBudget *
 110      Foundation.MeasureForcing.rho ^
 111        (Real.log (alpha_inv_CODATA / channelBudget) / Real.log Foundation.MeasureForcing.rho)
 112    = alpha_inv_CODATA
 113  rw [Real.rpow_def_of_pos Foundation.MeasureForcing.rho_pos]
 114  have hlog : Real.log Foundation.MeasureForcing.rho ≠ 0 := log_rho_ne_zero
 115  have harg : Real.log Foundation.MeasureForcing.rho *
 116      (Real.log (alpha_inv_CODATA / channelBudget) / Real.log Foundation.MeasureForcing.rho)
 117      = Real.log (alpha_inv_CODATA / channelBudget) := by
 118    field_simp
 119  rw [harg, Real.exp_log hratio]
 120  field_simp
 121
 122/-- **Uniqueness of the closing load.** The dressed value is strictly
 123decreasing in the load (ρ < 1), so exactly one `δ₂` closes the residual. -/
 124theorem corrected_eq_codata_iff (δ₂ : ℝ) :
 125    correctedAlphaInv δ₂ = alpha_inv_CODATA ↔ δ₂ = closingLoad := by
 126  constructor
 127  · intro h
 128    have hb : (0 : ℝ) < channelBudget := channelBudget_pos
 129    have hkey : Foundation.MeasureForcing.rho ^ (spectralLoad + δ₂) =
 130        Foundation.MeasureForcing.rho ^ (spectralLoad + closingLoad) := by
 131      have h2 : correctedAlphaInv δ₂ = correctedAlphaInv closingLoad := by
 132        rw [h, corrected_at_closingLoad]
 133      unfold correctedAlphaInv at h2
 134      exact mul_left_cancel₀ (ne_of_gt hb) h2
 135    -- ρ^x is strictly antitone for ρ ∈ (0,1), so the exponents agree
 136    have hexp_eq : spectralLoad + δ₂ = spectralLoad + closingLoad := by
 137      by_contra hne
 138      rcases lt_or_gt_of_ne hne with hlt | hgt
 139      · have hmono := Real.rpow_lt_rpow_of_exponent_gt
 140          Foundation.MeasureForcing.rho_pos Foundation.MeasureForcing.rho_lt_one hlt
 141        linarith [hkey.le, hkey.ge, hmono]
 142      · have hmono := Real.rpow_lt_rpow_of_exponent_gt
 143          Foundation.MeasureForcing.rho_pos Foundation.MeasureForcing.rho_lt_one hgt
 144        linarith [hkey.le, hkey.ge, hmono]
 145    linarith [hexp_eq]
 146  · intro h
 147    rw [h]
 148    exact corrected_at_closingLoad
 149
 150/-- There is exactly one closing load. -/
 151theorem existsUnique_closingLoad :
 152    ∃! δ₂ : ℝ, correctedAlphaInv δ₂ = alpha_inv_CODATA := by
 153  refine ⟨closingLoad, corrected_at_closingLoad, ?_⟩
 154  intro δ h
 155  exact (corrected_eq_codata_iff δ).mp h
 156
 157/-- **THE SEAM FALSIFIER.** A blind seam derivation producing load `δ₂`
 158closes the α program iff `δ₂ = closingLoad`; any other value falsifies the
 159channel-budget bridge. (Definition-level statement of the kill condition.) -/
 160def SeamDerivationCloses (δ₂ : ℝ) : Prop :=
 161  correctedAlphaInv δ₂ = alpha_inv_CODATA
 162
 163theorem seam_closes_iff (δ₂ : ℝ) : SeamDerivationCloses δ₂ ↔ δ₂ = closingLoad :=
 164  corrected_eq_codata_iff δ₂
 165
 166end
 167
 168end AlphaGenesis
 169end Constants
 170end IndisputableMonolith
 171