IndisputableMonolith.Constants.AlphaGenesis.ResummationForcing

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.GapWeight
   4import IndisputableMonolith.Constants.Alpha
   5import IndisputableMonolith.Foundation.MeasureForcing
   6
   7/-!
   8# Alpha Genesis M1: Resummation Forcing
   9
  10**THE THEOREM.** The exponential dressing of the α seed is not a "resummation
  11convention." It is forced: any dressing response that factorizes over
  12independent gap loads and has unit linear response at zero load is exactly
  13`ε ↦ exp(−ε)`. The additive display `ε ↦ 1 − ε` is not a factorizing
  14response at all (witness: ε₁ = ε₂ = 1).
  15
  16This discharges discrete choice (i) of the no-fit proposition (resummation
  17form (E) vs (A)): form (E) is the unique admissible response; form (A) is its
  18first-order truncation, a display, not a structural alternative.
  19
  20## Why factorization is the right premise (not a new choice)
  21
  22The premise is inherited, not invented for α. It is the same factorization
  23premise that forces the T9 measure:
  24
  25* `Foundation.MeasureForcing.RecognitionWeightRule.factorizes` — independent
  26  composition multiplies weights (lattice layer).
  27* `Foundation.MeasureForcing.Factorizes` — the continuum layer premise of
  28  `continuum_weight_forced`.
  29
  30The surviving coupling fraction after paying gap cost ε IS a recognition
  31weight at cost ε. Independent gap loads on independent channels compose
  32additively in cost; an unpaid correlation between independent loads is
  33forbidden by ledger additivity (same argument as MeasureForcing §1). So the
  34response must factorize: `g(ε₁ + ε₂) = g(ε₁) · g(ε₂)`.
  35
  36The calibration `g′(0) = −1` is the unit-linear-response normalization, the
  37dressing analog of T5's `IsCalibrated` (unit log-curvature at the identity).
  38
  39## The unification corollary
  40
  41`alphaInv_eq_seed_mul_forced_weight`: the α dressing factor IS the T9 forced
  42measure `contWeight` evaluated at the spectral gap load per channel
  43(`w₈ / (44π)` in rung units). The fine-structure constant is the channel
  44budget of ∂Q₃ attenuated by the unique recognition weight — the same measure
  45that fixes ℏ = φ⁻⁵, θ = φ⁻⁴, and the rung-44 scale.
  46
  47STATUS: THEOREM (0 sorry target). No CODATA reference anywhere in this file.
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Constants
  52namespace AlphaGenesis
  53
  54noncomputable section
  55
  56/-- A **dressing response**: the fraction of coupling budget surviving a gap
  57load ε. The two fields are the inherited ledger premises:
  58
  59* `factorizes` — independent gap loads multiply survival fractions (the same
  60  premise that forces the T9 measure);
  61* `unit_response` — unit linear response at zero load (calibration, the
  62  dressing analog of T5's unit log-curvature). -/
  63structure DressingResponse where
  64  /-- Survival fraction as a function of gap load. -/
  65  g : ℝ → ℝ
  66  /-- Factorization over independent gap loads (ledger additivity shadow). -/
  67  factorizes : ∀ x y : ℝ, g (x + y) = g x * g y
  68  /-- Unit linear response at zero load (calibration). -/
  69  unit_response : HasDerivAt g (-1) 0
  70
  71namespace DressingResponse
  72
  73variable (R : DressingResponse)
  74
  75/-- Zero load means no dressing: `g(0) = 1`. (The alternative `g(0) = 0`
  76forces `g ≡ 0`, contradicting the unit response.) -/
  77theorem g_zero : R.g 0 = 1 := by
  78  have h : R.g 0 = R.g 0 * R.g 0 := by
  79    have h0 := R.factorizes 0 0
  80    simpa using h0
  81  have hz : R.g 0 * (R.g 0 - 1) = 0 := by
  82    rw [mul_sub, mul_one, ← h, sub_self]
  83  rcases mul_eq_zero.mp hz with h0 | h1
  84  · exfalso
  85    have hall : ∀ x, R.g x = 0 := by
  86      intro x
  87      have hx := R.factorizes x 0
  88      simpa [h0] using hx
  89    have hconst : R.g = fun _ => (0 : ℝ) := funext hall
  90    have hd : HasDerivAt (fun _ : ℝ => (0 : ℝ)) (-1) 0 := by
  91      have hur := R.unit_response
  92      rw [hconst] at hur
  93      exact hur
  94    have hzero : ((-1 : ℝ)) = 0 := hd.unique (hasDerivAt_const 0 0)
  95    norm_num at hzero
  96  · linarith [sub_eq_zero.mp h1]
  97
  98/-- The response is differentiable everywhere with `g′(x) = −g(x)`:
  99factorization propagates the calibrated derivative from 0 to every point. -/
 100theorem hasDerivAt_neg_self (x : ℝ) : HasDerivAt R.g (-(R.g x)) x := by
 101  have hshift : HasDerivAt (fun y : ℝ => y - x) 1 x := (hasDerivAt_id x).sub_const x
 102  have hcomp0 : HasDerivAt (R.g ∘ fun y : ℝ => y - x) (-1 * 1) x := by
 103    apply HasDerivAt.comp
 104    · show HasDerivAt R.g (-1) ((fun y : ℝ => y - x) x)
 105      simpa [sub_self] using R.unit_response
 106    · exact hshift
 107  have hcomp : HasDerivAt (fun y : ℝ => R.g (y - x)) (-1 * 1) x := by
 108    simpa [Function.comp] using hcomp0
 109  have hmul : HasDerivAt (fun y : ℝ => R.g x * R.g (y - x)) (R.g x * (-1 * 1)) x :=
 110    hcomp.const_mul (R.g x)
 111  have hfun : (fun y : ℝ => R.g x * R.g (y - x)) = R.g := by
 112    funext y
 113    rw [← R.factorizes x (y - x)]
 114    congr 1
 115    ring
 116  rw [hfun] at hmul
 117  convert hmul using 1
 118  ring
 119
 120/-- **RESUMMATION FORCING.** Any factorizing dressing response with unit
 121linear response is exactly the exponential: `g(ε) = exp(−ε)`. There is no
 122resummation freedom. -/
 123theorem response_forced : ∀ ε : ℝ, R.g ε = Real.exp (-ε) := by
 124  -- h(x) = g(x)·exp(x) has zero derivative everywhere, hence is constant 1.
 125  have hd : ∀ x : ℝ, HasDerivAt (fun y : ℝ => R.g y * Real.exp y) 0 x := by
 126    intro x
 127    have hmul := (R.hasDerivAt_neg_self x).mul (Real.hasDerivAt_exp x)
 128    convert hmul using 1
 129    ring
 130  have hdiff : Differentiable ℝ (fun y : ℝ => R.g y * Real.exp y) :=
 131    fun x => (hd x).differentiableAt
 132  have hderiv : ∀ x : ℝ, deriv (fun y : ℝ => R.g y * Real.exp y) x = 0 :=
 133    fun x => (hd x).deriv
 134  have hconst : ∀ x : ℝ, R.g x * Real.exp x = R.g 0 * Real.exp 0 := by
 135    intro x
 136    exact is_const_of_deriv_eq_zero hdiff hderiv x 0
 137  intro ε
 138  have hε : R.g ε * Real.exp ε = 1 := by
 139    have hx := hconst ε
 140    simpa [R.g_zero] using hx
 141  have hexp : Real.exp ε ≠ 0 := (Real.exp_pos ε).ne'
 142  have hgε : R.g ε = (Real.exp ε)⁻¹ := by
 143    have h2 := congrArg (· * (Real.exp ε)⁻¹) hε
 144    simpa [mul_assoc, mul_inv_cancel₀ hexp] using h2
 145  rw [hgε, ← Real.exp_neg]
 146
 147/-- **ADDITIVE FORM EXCLUDED.** No dressing response is the additive display
 148`ε ↦ 1 − ε`: it fails factorization (witness ε₁ = ε₂ = 1). Form (A) is a
 149truncation of form (E), not a structural alternative. -/
 150theorem no_additive_response : R.g ≠ fun ε => 1 - ε := by
 151  intro hcontra
 152  have h := R.factorizes 1 1
 153  rw [hcontra] at h
 154  norm_num at h
 155
 156end DressingResponse
 157
 158/-- The additive map fails the factorization law outright (independent of any
 159response structure). -/
 160theorem additive_map_not_factorizing :
 161    ¬ (∀ x y : ℝ, (1 - (x + y)) = (1 - x) * (1 - y)) := by
 162  intro h
 163  have h11 := h 1 1
 164  norm_num at h11
 165
 166/-- The dressed coupling: seed times forced response at normalized load. -/
 167def dressedCoupling (S δ : ℝ) : ℝ := S * Real.exp (-(δ / S))
 168
 169/-- Any dressing response yields exactly the form-(E) dressed coupling. -/
 170theorem dressedCoupling_forced (R : DressingResponse) (S δ : ℝ) :
 171    S * R.g (δ / S) = dressedCoupling S δ := by
 172  rw [R.response_forced (δ / S)]
 173  rfl
 174
 175/-- **THE UNIFICATION COROLLARY.** The certified `alphaInv` is the channel
 176budget multiplied by the **T9 forced measure** at the spectral gap load per
 177channel (in rung units):
 178
 179`α⁻¹ = (4π·11) · contWeight(w₈ / (4π·11))`.
 180
 181The α dressing factor is not α-specific structure. It is the unique
 182recognition weight `φ⁻ᵗ` forced by factorization + self-similar calibration
 183(`Foundation.MeasureForcing.continuum_weight_forced`), evaluated at
 184`t = w₈/(44π)` rungs. -/
 185theorem alphaInv_eq_seed_mul_forced_weight :
 186    Constants.alphaInv =
 187      Constants.alpha_seed *
 188        Foundation.MeasureForcing.contWeight
 189          (Constants.w8_from_eight_tick / Constants.alpha_seed) := by
 190  rw [Foundation.MeasureForcing.contWeight_gibbs]
 191  simp only [Constants.alphaInv]
 192  have hgap : Constants.f_gap = Constants.w8_from_eight_tick * Real.log Constants.phi := rfl
 193  rw [hgap]
 194  congr 1
 195  congr 1
 196  ring
 197
 198/-- The response that dresses α and the weight that forces the measure are
 199one function: `g(lnφ · t) = contWeight(t)` for every dressing response. -/
 200theorem response_is_forced_measure (R : DressingResponse) (t : ℝ) :
 201    R.g (Real.log Constants.phi * t) = Foundation.MeasureForcing.contWeight t := by
 202  rw [R.response_forced, Foundation.MeasureForcing.contWeight_gibbs]
 203  congr 1
 204  ring
 205
 206end
 207
 208end AlphaGenesis
 209end Constants
 210end IndisputableMonolith
 211