IndisputableMonolith.Constants.GapWeight.Projection

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.GapWeight.Formula
   4import IndisputableMonolith.Spectral.DFT8
   5
   6namespace IndisputableMonolith
   7namespace Constants
   8namespace GapWeight
   9
  10open scoped BigOperators
  11
  12open Complex
  13open IndisputableMonolith.Spectral
  14
  15/-!
  16# GapWeight.Projection — closing the “weights + normalization” ambiguity
  17
  18This module defines, explicitly, the two pieces that were historically left implicit:
  19
  201) **Why the geometric weights have a `sin²(πk/8)` factor.**
  21   This is the spectral (eigenvalue) weight induced by the *discrete derivative / Laplacian*
  22   on the 8-tick cyclic shift. In DFT language, it is forced by shift-diagonalization.
  23
  242) **Why the normalization uses a factor of `64`.**
  25   `64 = 8×8` is the cardinality of the fundamental RS interface cell when we take:
  26   - 8 ticks (the octave clock), and
  27   - 8 spatial vertices (the Q₃ cell has 8 vertices).
  28   The normalization converts a scale-invariant *fraction* into a per-cell integrated weight.
  29
  30This is claim hygiene: we’re making the operator/measure choice explicit, so there is no
  31hidden degree of freedom.
  32-/
  33
  34/-! ## Canonical counts (no ambiguity) -/
  35
  36/-- Number of ticks in the fundamental octave. -/
  37@[simp] def N_ticks : ℕ := Fintype.card (Fin 8)
  38
  39@[simp] theorem N_ticks_eq : N_ticks = 8 := by
  40  decide
  41
  42/-- Number of spatial vertices in a `Q₃` cell (8 vertices). We model this as `Fin 8`. -/
  43@[simp] def N_vertices : ℕ := Fintype.card (Fin 8)
  44
  45@[simp] theorem N_vertices_eq : N_vertices = 8 := by
  46  decide
  47
  48/-- Size of the fundamental “cell index” set: ticks × vertices = 8×8 = 64. -/
  49@[simp] def N_cell : ℕ := Fintype.card (Fin 8 × Fin 8)
  50
  51@[simp] theorem N_cell_eq : N_cell = 64 := by
  52  -- card (Fin 8 × Fin 8) = 8 * 8
  53  decide
  54
  55/-- The projection scaling used to convert a dimensionless fraction into a per-cell weight. -/
  56@[simp] def projectionScale : ℝ := (N_cell : ℝ)
  57
  58@[simp] theorem projectionScale_eq : projectionScale = 64 := by
  59  simp [projectionScale, N_cell_eq]
  60
  61/-! ## A canonical normalization denominator -/
  62
  63/-- Total DFT energy of the φ-pattern (Parseval denominator). -/
  64noncomputable def phiDFTEnergyTotal : ℝ :=
  65  Finset.univ.sum fun k : Fin 8 => phiDFTAmplitude k
  66
  67lemma phiDFTEnergyTotal_nonneg : 0 ≤ phiDFTEnergyTotal := by
  68  unfold phiDFTEnergyTotal
  69  apply Finset.sum_nonneg
  70  intro k _
  71  exact phiDFTAmplitude_nonneg k
  72
  73/-! ## The explicit projection operator (minimal actionable closure) -/
  74
  75/-- **Projection weight** of the φ-pattern onto the 8-tick basis:
  76
  77`projectionScale * (rawWeightedNeutralEnergy / totalEnergy)`.
  78
  79This makes the normalization and measure choice explicit. -/
  80noncomputable def w8_projected : ℝ :=
  81  projectionScale * (w8_dft_candidate / phiDFTEnergyTotal)
  82
  83lemma w8_projected_nonneg : 0 ≤ w8_projected := by
  84  unfold w8_projected
  85  have hscale : 0 ≤ projectionScale := by simp [projectionScale]
  86  have hnum : 0 ≤ w8_dft_candidate := le_of_lt w8_dft_candidate_pos
  87  have hden : 0 ≤ phiDFTEnergyTotal := phiDFTEnergyTotal_nonneg
  88  -- If total energy is 0, then the ratio is 0 (since numerator is 0 as well). Otherwise nonneg by div_nonneg.
  89  by_cases hE : phiDFTEnergyTotal = 0
  90  · simp [hE, hnum, hscale]
  91  · have hdiv : 0 ≤ w8_dft_candidate / phiDFTEnergyTotal := div_nonneg hnum (le_of_lt (lt_of_le_of_ne' hden hE))
  92    exact mul_nonneg hscale hdiv
  93
  94/-!
  95## Important note
  96
  97At present, the pipeline constant `Constants.w8_from_eight_tick` is defined in a closed form
  98in `Constants/GapWeight.lean` and evaluates to ≈ 2.49056927545.
  99
 100The operator `w8_projected` above is the *definition-level closure* of what “projection weight”
 101means: it makes explicit the normalization and the 8×8 measure.
 102
 103Proving `w8_projected = Constants.w8_from_eight_tick` inside Lean is a tractable (but nontrivial)
 104algebraic/trigonometric reduction problem and is tracked as a follow-up theorem.
 105-/
 106
 107/-! ## Why `sin²(πk/8)` is canonical (spectral footprint of the 8-tick derivative) -/
 108
 109/-- Discrete one-step difference on the 8-tick cycle: `(S - I)v`. -/
 110def diff8 (v : Fin 8 → ℂ) : Fin 8 → ℂ :=
 111  fun t => cyclic_shift v t - v t
 112
 113/-- Total squared energy of the discrete difference (a canonical local, shift-invariant quadratic form). -/
 114noncomputable def diffEnergy8 (v : Fin 8 → ℂ) : ℝ :=
 115  ∑ t : Fin 8, Complex.normSq (diff8 v t)
 116
 117lemma diffEnergy8_nonneg (v : Fin 8 → ℂ) : 0 ≤ diffEnergy8 v := by
 118  unfold diffEnergy8
 119  exact Finset.sum_nonneg (fun _ _ => Complex.normSq_nonneg _)
 120
 121/-- DFT-8 mode `k` has unit norm (columns are orthonormal). -/
 122lemma dft8_mode_normSq_sum (k : Fin 8) :
 123    (∑ t : Fin 8, Complex.normSq (dft8_mode k t)) = 1 := by
 124  -- ⟨column k, column k⟩ = 1, and ⟨v,v⟩ = ∑ conj(v_t) * v_t = ∑ normSq(v_t).
 125  have hcol := dft8_column_orthonormal k k
 126  have h1 : (∑ t : Fin 8, star (dft8_entry t k) * dft8_entry t k) = (1 : ℂ) := by
 127    simpa using (by simpa using hcol)
 128  -- Rewrite each term `star z * z` as `(normSq z : ℂ)`.
 129  have h1' : (∑ t : Fin 8, ((Complex.normSq (dft8_entry t k) : ℝ) : ℂ)) = (1 : ℂ) := by
 130    simpa [Complex.normSq_eq_conj_mul_self] using h1
 131  -- Pull the cast out of the sum.
 132  have h1'' : ((∑ t : Fin 8, (Complex.normSq (dft8_entry t k) : ℝ)) : ℂ) = (1 : ℂ) := by
 133    simpa [Complex.ofReal_sum] using h1'
 134  -- Back to ℝ, and rewrite `dft8_mode`.
 135  have hreal : (∑ t : Fin 8, (Complex.normSq (dft8_entry t k) : ℝ)) = (1 : ℝ) :=
 136    Complex.ofReal_injective (by simpa using h1'')
 137  simpa [dft8_mode] using hreal
 138
 139/-- Discrete difference energy of a DFT mode is the squared magnitude of its shift eigenvalue minus 1.
 140
 141This is the precise mathematical reason a `sin²(πk/8)` factor appears: it is (up to a fixed factor 4)
 142the spectrum of the 8-tick discrete derivative/Laplacian. -/
 143lemma diffEnergy8_mode (k : Fin 8) :
 144    diffEnergy8 (dft8_mode k) = Complex.normSq (omega8 ^ k.val - 1) := by
 145  unfold diffEnergy8 diff8
 146  -- Use that cyclic_shift (mode k) = ω^k • mode k.
 147  have hshift := dft8_shift_eigenvector k
 148  -- rewrite the difference pointwise
 149  have hpoint : ∀ t : Fin 8, cyclic_shift (dft8_mode k) t - dft8_mode k t =
 150      (omega8 ^ k.val - 1) * dft8_mode k t := by
 151    intro t
 152    have ht := congrArg (fun f => f t) hshift
 153    -- ht : cyclic_shift (dft8_mode k) t = (omega8 ^ k.val) • dft8_mode k t
 154    simp [Pi.smul_apply, smul_eq_mul] at ht
 155    -- subtract and factor
 156    calc
 157      cyclic_shift (dft8_mode k) t - dft8_mode k t
 158          = (omega8 ^ k.val) * dft8_mode k t - dft8_mode k t := by simpa [ht]
 159      _   = (omega8 ^ k.val - 1) * dft8_mode k t := by ring
 160  -- push through normSq and sum
 161  have hns : ∀ t : Fin 8, Complex.normSq (cyclic_shift (dft8_mode k) t - dft8_mode k t) =
 162      Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t) := by
 163    intro t
 164    -- use hpoint and normSq_mul
 165    simp [hpoint t, Complex.normSq_mul]
 166  simp_rw [hns]
 167  -- factor out the constant eigenvalue term
 168  have hfac :
 169      (∑ t : Fin 8, Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t)) =
 170        Complex.normSq (omega8 ^ k.val - 1) * (∑ t : Fin 8, Complex.normSq (dft8_mode k t)) := by
 171    -- `Finset.mul_sum` gives the reverse direction, so we use `.symm`.
 172    simpa using
 173      (Finset.mul_sum
 174        (s := (Finset.univ : Finset (Fin 8)))
 175        (f := fun t : Fin 8 => Complex.normSq (dft8_mode k t))
 176        (a := Complex.normSq (omega8 ^ k.val - 1))).symm
 177  rw [hfac, dft8_mode_normSq_sum]
 178  ring
 179
 180end GapWeight
 181end Constants
 182end IndisputableMonolith
 183