IndisputableMonolith.Constants.GapWeight.Formula

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Spectral.DFT8
   4
   5namespace IndisputableMonolith
   6namespace Constants
   7namespace GapWeight
   8
   9open Complex
  10open IndisputableMonolith.Spectral
  11
  12/-! ## The Canonical φ-Pattern -/
  13
  14/-- The canonical φ-power pattern: samples φᵗ for t ∈ Fin 8. -/
  15noncomputable def phiPattern : Fin 8 → ℝ :=
  16  fun t => phi ^ t.val
  17
  18/-- Convert the real pattern to complex for DFT analysis. -/
  19noncomputable def phiPatternComplex : Fin 8 → ℂ :=
  20  fun t => (phiPattern t : ℂ)
  21
  22/-! ## DFT Coefficients of the φ-Pattern -/
  23
  24/-- The DFT coefficient cₖ of the φ-pattern. -/
  25noncomputable def phiDFTCoeff (k : Fin 8) : ℂ :=
  26  Finset.univ.sum fun t => star (dft8_entry t k) * phiPatternComplex t
  27
  28/-- The squared amplitude of mode k for the φ-pattern. -/
  29noncomputable def phiDFTAmplitude (k : Fin 8) : ℝ :=
  30  Complex.normSq (phiDFTCoeff k)
  31
  32/-! ## Geometric Weights -/
  33
  34/-- Geometric weight for mode k. -/
  35noncomputable def geometricWeight (k : Fin 8) : ℝ :=
  36  if k.val = 0 then 0
  37  else
  38    let freq := (k.val : ℝ) * Real.pi / 8
  39    let oscillation := (Real.sin freq) ^ 2
  40    let phiDecay := phi ^ (-(k.val : ℤ))
  41    oscillation * phiDecay
  42
  43/-! ## A DFT-based *candidate* for the Gap Weight w₈ -/
  44
  45/-- A DFT-based candidate weight (scaffold).
  46
  47This is *not* currently proven to match the certified `Constants.w8_from_eight_tick`
  48used by the α pipeline (see `Constants/GapWeight.lean`). -/
  49noncomputable def w8_dft_candidate : ℝ :=
  50  Finset.sum (Finset.filter (· ≠ 0) Finset.univ) fun k =>
  51    phiDFTAmplitude k * geometricWeight k
  52
  53/-! ## Basic Properties (Verified) -/
  54
  55/-- phiDFTAmplitude is non-negative. -/
  56lemma phiDFTAmplitude_nonneg (k : Fin 8) : 0 ≤ phiDFTAmplitude k :=
  57  Complex.normSq_nonneg _
  58
  59/-- geometricWeight is non-negative. -/
  60lemma geometricWeight_nonneg (k : Fin 8) : 0 ≤ geometricWeight k := by
  61  unfold geometricWeight
  62  split_ifs with h
  63  · exact le_refl 0
  64  · apply mul_nonneg
  65    · exact sq_nonneg _
  66    · exact zpow_nonneg (le_of_lt phi_pos) _
  67
  68/-- geometricWeight is positive for neutral modes. -/
  69lemma geometricWeight_pos {k : Fin 8} (hk : k.val ≠ 0) : 0 < geometricWeight k := by
  70  unfold geometricWeight
  71  simp only [hk, ↓reduceIte]
  72  apply mul_pos
  73  · apply sq_pos_of_pos
  74    apply Real.sin_pos_of_pos_of_lt_pi
  75    · have hk_pos : 0 < k.val := Nat.pos_of_ne_zero hk
  76      positivity
  77    · have h1 : k.val ≤ 7 := Nat.lt_succ_iff.mp k.isLt
  78      have h2 : (k.val : ℝ) ≤ 7 := by exact Nat.cast_le.mpr h1
  79      calc (k.val : ℝ) * Real.pi / 8
  80          ≤ 7 * Real.pi / 8 := by nlinarith [Real.pi_pos]
  81        _ < Real.pi := by nlinarith [Real.pi_pos]
  82  · exact zpow_pos phi_pos _
  83
  84/-- The DFT-based candidate weight is positive. -/
  85theorem w8_dft_candidate_pos : 0 < w8_dft_candidate := by
  86  unfold w8_dft_candidate
  87  have h1_mem : (1 : Fin 8) ∈ Finset.filter (· ≠ 0) Finset.univ := by decide
  88  apply Finset.sum_pos'
  89  · intro k hk
  90    apply mul_nonneg
  91    · exact phiDFTAmplitude_nonneg k
  92    · exact geometricWeight_nonneg k
  93  · use 1, h1_mem
  94    apply mul_pos
  95    · unfold phiDFTAmplitude
  96      apply Complex.normSq_pos.mpr
  97      -- A rigorous proof: the φ-pattern φᵗ is strictly increasing (φ > 1).
  98      -- Its DFT coefficient c₁ is ∑_{t=0}^7 (ω⁷φ)ᵗ / √8.
  99      -- Let z = ω⁷φ. The sum is (z⁸ - 1)/(z - 1).
 100      -- Since |z| = φ > 1, z ≠ 1 and z⁸ = φ⁸ ≠ 1.
 101      -- Thus the sum is non-zero.
 102      intro h_zero
 103      have h_coeff : phiDFTCoeff 1 = (∑ t : Fin 8, (omega8 ^ 7 * (phi : ℂ)) ^ t.val) / (Real.sqrt 8 : ℂ) := by
 104        unfold phiDFTCoeff dft8_entry phiPatternComplex phiPattern
 105        rw [Finset.sum_div]
 106        congr 1
 107        ext t
 108        -- Expand the DFT entry and simplify `star`/conjugation.
 109        -- This puts the term into the geometric-series form `(ω⁷φ)^t / √8`.
 110        -- The final `mul_div` step is the only non-`simp` rearrangement we need.
 111        simp [dft8_entry, phiPatternComplex, phiPattern, star_div₀, star_pow, star_omega8,
 112          omega8_inv_eq_pow7, pow_mul, mul_pow]
 113        simpa [div_mul_eq_mul_div, mul_div, mul_assoc, mul_left_comm, mul_comm]
 114      rw [h_coeff, div_eq_zero_iff] at h_zero
 115      replace h_zero := h_zero.resolve_right (by
 116        have h_pos : 0 < (8 : ℝ) := by norm_num
 117        have h_sqrt_pos : 0 < Real.sqrt 8 := Real.sqrt_pos.mpr h_pos
 118        exact Complex.ofReal_ne_zero.mpr (ne_of_gt h_sqrt_pos))
 119      let z : ℂ := omega8 ^ 7 * (phi : ℂ)
 120      have h_z_def : ∀ t : Fin 8, (omega8 ^ 7 * (phi : ℂ)) ^ t.val = z ^ t.val := fun t => rfl
 121      simp_rw [h_z_def] at h_zero
 122      have h_sum_geom : (∑ t : Fin 8, z ^ t.val) * (z - 1) = z ^ 8 - 1 := by
 123        have h8 : (∑ t : Fin 8, z ^ t.val) = z^0 + z^1 + z^2 + z^3 + z^4 + z^5 + z^6 + z^7 := by
 124          simp only [Fin.sum_univ_eight]; rfl
 125        rw [h8]
 126        ring
 127      rw [h_zero, zero_mul] at h_sum_geom
 128      have h_z8 : z ^ 8 = (phi : ℂ) ^ 8 := by
 129        -- `z = ω⁷ φ`, so `z^8 = (ω⁷)^8 * φ^8 = 1 * φ^8`.
 130        have hω : (omega8 ^ 7) ^ 8 = (1 : ℂ) := by
 131          -- (ω⁷)^8 = ω^(7*8) = ω^(8*7) = (ω^8)^7 = 1
 132          rw [← pow_mul]
 133          have : (7 : ℕ) * 8 = 8 * 7 := by ring
 134          rw [this, pow_mul, omega8_pow_8, one_pow]
 135        simp [z, mul_pow, hω]
 136      rw [h_z8] at h_sum_geom
 137      have h_phi8_ne_one : (phi : ℂ) ^ 8 ≠ 1 := by
 138        rw [← Complex.ofReal_pow, ← Complex.ofReal_one]
 139        intro h
 140        replace h := Complex.ofReal_injective h
 141        have h_phi_pos : 0 < phi := phi_pos
 142        have h_phi_one : 1 < phi := one_lt_phi
 143        have h_pow_gt : 1 < phi ^ 8 := one_lt_pow₀ h_phi_one (by norm_num)
 144        linarith
 145      -- From `0 = φ^8 - 1` we would get `φ^8 = 1`, contradiction since φ > 1.
 146      have h_phi8_eq_one : (phi : ℂ) ^ 8 = 1 := by
 147        have : (phi : ℂ) ^ 8 - 1 = 0 := by
 148          simpa [eq_comm] using h_sum_geom
 149        exact sub_eq_zero.mp this
 150      exact h_phi8_ne_one h_phi8_eq_one
 151    · exact geometricWeight_pos (by decide : (1 : Fin 8).val ≠ 0)
 152
 153end GapWeight
 154end Constants
 155end IndisputableMonolith
 156