IndisputableMonolith.Constants.AlphaGenesis.SpectralForcing

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.GapWeight.Formula
   4import IndisputableMonolith.Constants.GapWeight.Projection
   5import IndisputableMonolith.Constants.AlphaGenesis.PatternForcing
   6import IndisputableMonolith.Foundation.MeasureForcing
   7
   8/-!
   9# Alpha Genesis M6: Spectral Forcing (the sin² factor is the derivative spectrum)
  10
  11**THE THEOREM.** The oscillation factor `sin²(kπ/8)` inside the gap-weight
  12mode weights is not a modeling choice: it is (one quarter of) the spectrum
  13of the one-step difference operator on the eight-tick cycle, evaluated on
  14the DFT-8 eigenbasis.
  15
  16The chain, every link a theorem:
  17
  181. The DFT-8 modes diagonalize the cyclic shift
  19   (`DFT8.dft8_shift_eigenvector`).
  202. The difference energy of mode k is the squared modulus of its shift
  21   eigenvalue minus one (`GapWeight.diffEnergy8_mode`):
  22   `diffEnergy8(mode k) = |ω₈ᵏ − 1|²`.
  233. **The trig closure (this module):** `|ω₈ᵏ − 1|² = 4 sin²(kπ/8)`
  24   (`normSq_omega8_pow_sub_one`).
  254. **The factorization (this module):** for every nonzero mode,
  26   `geometricWeight k = (diffEnergy8(mode k)/4) · latticeWeight k`
  27   (`geometricWeight_eq_spectrum_mul_measure`): the mode weight is the
  28   difference-operator spectrum times the T9 forced measure. Both factors
  29   are now theorem-backed; neither is an input.
  30
  31Together with M2 (the pattern is forced) and M5 (the calibration is not an
  32input), this closes the last interior joint of the gap weight: pattern,
  33envelope, oscillation factor, and dressing form are all forced. The only
  34remaining w₈ ingredient inherited without re-derivation is the Parseval /
  3564-cell normalization (named in the paper's premise section).
  36
  37STATUS: THEOREM (0 sorry target). No CODATA reference anywhere in this file.
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Constants
  42namespace AlphaGenesis
  43
  44noncomputable section
  45
  46open IndisputableMonolith.Spectral
  47open Constants.GapWeight
  48
  49/-- **The trig closure.** The squared modulus of the shift eigenvalue minus
  50one is four times the squared half-angle sine:
  51`|ω₈ᵏ − 1|² = 4 sin²(kπ/8)`. -/
  52theorem normSq_omega8_pow_sub_one (k : ℕ) :
  53    Complex.normSq (omega8 ^ k - 1) =
  54      4 * (Real.sin ((k : ℝ) * Real.pi / 8)) ^ 2 := by
  55  -- ω₈ᵏ = exp(i·θ) with θ = −kπ/4
  56  have hpow : omega8 ^ k = Complex.exp ((-((k : ℝ) * Real.pi / 4) : ℝ) * Complex.I) := by
  57    unfold omega8
  58    rw [← Complex.exp_nat_mul]
  59    congr 1
  60    push_cast
  61    ring
  62  rw [hpow, Complex.exp_mul_I]
  63  -- normSq(cos θ + sin θ·i − 1) = (cos θ − 1)² + sin² θ
  64  have hcos : Complex.cos ((-((k : ℝ) * Real.pi / 4) : ℝ) : ℂ) =
  65      ((Real.cos (-((k : ℝ) * Real.pi / 4)) : ℝ) : ℂ) := by
  66    rw [Complex.ofReal_cos]
  67  have hsin : Complex.sin ((-((k : ℝ) * Real.pi / 4) : ℝ) : ℂ) =
  68      ((Real.sin (-((k : ℝ) * Real.pi / 4)) : ℝ) : ℂ) := by
  69    rw [Complex.ofReal_sin]
  70  rw [hcos, hsin]
  71  set θ : ℝ := -((k : ℝ) * Real.pi / 4) with hθ
  72  have hrw : (Real.cos θ : ℂ) + (Real.sin θ : ℂ) * Complex.I - 1
  73      = ((Real.cos θ - 1 : ℝ) : ℂ) + ((Real.sin θ : ℝ) : ℂ) * Complex.I := by
  74    push_cast
  75    ring
  76  rw [hrw, Complex.normSq_add_mul_I]
  77  -- (cos θ − 1)² + sin² θ = 2 − 2 cos θ
  78  have hpyth : Real.sin θ ^ 2 + Real.cos θ ^ 2 = 1 := Real.sin_sq_add_cos_sq θ
  79  have h2 : (Real.cos θ - 1) ^ 2 + (Real.sin θ) ^ 2 = 2 - 2 * Real.cos θ := by
  80    nlinarith [hpyth]
  81  rw [h2]
  82  -- cos θ = cos(kπ/4) (cos is even)
  83  have hcos_even : Real.cos θ = Real.cos ((k : ℝ) * Real.pi / 4) := by
  84    rw [hθ, Real.cos_neg]
  85  rw [hcos_even]
  86  -- half-angle via double-angle: cos(2x) = 2cos²x − 1 and sin²x = 1 − cos²x
  87  have hcos2 : Real.cos (2 * ((k : ℝ) * Real.pi / 8)) =
  88      2 * Real.cos ((k : ℝ) * Real.pi / 8) ^ 2 - 1 :=
  89    Real.cos_two_mul ((k : ℝ) * Real.pi / 8)
  90  have harg : 2 * ((k : ℝ) * Real.pi / 8) = (k : ℝ) * Real.pi / 4 := by ring
  91  rw [harg] at hcos2
  92  have hsq : Real.sin ((k : ℝ) * Real.pi / 8) ^ 2 =
  93      1 - Real.cos ((k : ℝ) * Real.pi / 8) ^ 2 :=
  94    Real.sin_sq ((k : ℝ) * Real.pi / 8)
  95  nlinarith [hcos2, hsq]
  96
  97/-- **The spectrum identity.** The difference energy of DFT mode k equals
  98`4 sin²(kπ/8)`: the oscillation factor of the gap weight is exactly one
  99quarter of the difference-operator spectrum. -/
 100theorem diffEnergy8_mode_eq_four_sin_sq (k : Fin 8) :
 101    diffEnergy8 (dft8_mode k) =
 102      4 * (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 := by
 103  rw [diffEnergy8_mode k]
 104  exact normSq_omega8_pow_sub_one k.val
 105
 106/-- **SPECTRAL FORCING.** For every nonzero mode, the gap-weight mode
 107weight factors as (difference-operator spectrum / 4) times the T9 forced
 108measure:
 109`geometricWeight k = (diffEnergy8(mode k)/4) · latticeWeight k`.
 110Both factors are theorems; neither is an input. -/
 111theorem geometricWeight_eq_spectrum_mul_measure (k : Fin 8) (hk : ¬ k.val = 0) :
 112    GapWeight.geometricWeight k =
 113      (diffEnergy8 (dft8_mode k) / 4) *
 114        Foundation.MeasureForcing.latticeWeight k.val := by
 115  rw [geometricWeight_eq_sin_mul_forced_measure k hk,
 116    diffEnergy8_mode_eq_four_sin_sq k]
 117  ring
 118
 119/-- **SPECTRAL FORCING CERTIFICATE.** Bundles the M6 closure:
 1201. the trig closure `|ω₈ᵏ − 1|² = 4 sin²(kπ/8)`;
 1212. the spectrum identity for every DFT mode;
 1223. the full factorization of the mode weight into spectrum × measure. -/
 123structure SpectralForcingCert where
 124  deriving Inhabited
 125
 126@[simp] def SpectralForcingCert.verified (_c : SpectralForcingCert) : Prop :=
 127  (∀ k : ℕ, Complex.normSq (omega8 ^ k - 1) =
 128    4 * (Real.sin ((k : ℝ) * Real.pi / 8)) ^ 2) ∧
 129  (∀ k : Fin 8, diffEnergy8 (dft8_mode k) =
 130    4 * (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2) ∧
 131  (∀ k : Fin 8, ¬ k.val = 0 →
 132    GapWeight.geometricWeight k =
 133      (diffEnergy8 (dft8_mode k) / 4) *
 134        Foundation.MeasureForcing.latticeWeight k.val)
 135
 136theorem SpectralForcingCert.verified_any (c : SpectralForcingCert) :
 137    SpectralForcingCert.verified c := by
 138  refine ⟨normSq_omega8_pow_sub_one, diffEnergy8_mode_eq_four_sin_sq,
 139    geometricWeight_eq_spectrum_mul_measure⟩
 140
 141end
 142
 143end AlphaGenesis
 144end Constants
 145end IndisputableMonolith
 146