Encyclopedia Constants Constants Gap Weight Projection Diff Energy8 Mode

ARTICLE 3 claims 3 theorems

Constants Gap Weight Projection Diff Energy8 Mode

A machine-checked lemma shows how much energy a vibration mode carries in a discrete eight-step cycle, tying a familiar trigonometric factor to the mathematics of difference operators.

Verify this page

The discrete difference energy

In the mathematics of discrete signals, a difference operator measures how much a sequence changes from one step to the next. For a cycle of eight steps, the operator takes a sequence of eight complex numbers and, at each position, subtracts the previous value from the current one. The total squared energy of these differences, summed over all eight positions, is a standard way to quantify how rapidly a signal fluctuates.

The lemma diffEnergy8_mode computes this energy for the eight basis modes of the discrete Fourier transform on the cycle. Each mode is a pure oscillation at a frequency indexed by an integer k from 0 to 7. The result states that the energy equals the squared magnitude of (ωk − 1), where ω is a primitive eighth root of unity. This expression simplifies to 4 sin²(πk/8), a factor that appears throughout the framework's weight calculations. The lemma is proved in the machine-checked library of formal theorems, meaning the algebraic identity is verified by a computer.

The content of the lemma is purely mathematical: it identifies the energy of a specific basis vector under a specific linear operator. It does not assign physical meaning to that energy, nor does it claim that any particular physical system realizes this cycle. The lemma is a definitional fact about the discrete Fourier transform and the difference operator, not an empirical statement about nature. It establishes a relationship between two mathematical objects, and that relationship is exact.

In Recognition Science, this lemma serves as the spectral justification for why a sin²(πk/8) factor appears in geometric weights. The framework models a fundamental cell with eight ticks and eight spatial vertices, and the difference operator on the eight-tick cycle is a canonical local quadratic form. The lemma shows that this operator's action on Fourier modes produces exactly the trigonometric factor used elsewhere. This is a statement about the framework's internal consistency, not a derivation of a physical law.

The lemma does not prove that the total energy of an arbitrary signal equals the sum of mode energies; that is Parseval's theorem, a separate result. It also does not establish that the discrete difference energy is the correct measure for any physical application. The lemma is one clean algebraic fact, and its role in the framework is to make explicit a choice of measure that was previously implicit.

THEOREM diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean
diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean:139 
/-- Discrete difference energy of a DFT mode is the squared magnitude of its shift eigenvalue minus 1.

This is the precise mathematical reason a `sin²(πk/8)` factor appears: it is (up to a fixed factor 4)
the spectrum of the 8-tick discrete derivative/Laplacian. -/
lemma diffEnergy8_mode (k : Fin 8) :
    diffEnergy8 (dft8_mode k) = Complex.normSq (omega8 ^ k.val - 1) := by
  unfold diffEnergy8 diff8
  -- Use that cyclic_shift (mode k) = ω^k • mode k.
  have hshift := dft8_shift_eigenvector k
  -- rewrite the difference pointwise
  have hpoint : ∀ t : Fin 8, cyclic_shift (dft8_mode k) t - dft8_mode k t =
      (omega8 ^ k.val - 1) * dft8_mode k t := by
    intro t
    have ht := congrArg (fun f => f t) hshift
    -- ht : cyclic_shift (dft8_mode k) t = (omega8 ^ k.val) • dft8_mode k t
    simp [Pi.smul_apply, smul_eq_mul] at ht
    -- subtract and factor
    calc
      cyclic_shift (dft8_mode k) t - dft8_mode k t
          = (omega8 ^ k.val) * dft8_mode k t - dft8_mode k t := by simpa [ht]
      _   = (omega8 ^ k.val - 1) * dft8_mode k t := by ring
  -- push through normSq and sum
  have hns : ∀ t : Fin 8, Complex.normSq (cyclic_shift (dft8_mode k) t - dft8_mode k t) =
      Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t) := by
    intro t
    -- use hpoint and normSq_mul
    simp [hpoint t, Complex.normSq_mul]
  simp_rw [hns]
  -- factor out the constant eigenvalue term
  have hfac :
      (∑ t : Fin 8, Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t)) =
        Complex.normSq (omega8 ^ k.val - 1) * (∑ t : Fin 8, Complex.normSq (dft8_mode k t)) := by
    -- `Finset.mul_sum` gives the reverse direction, so we use `.symm`.
    simpa using
      (Finset.mul_sum
        (s := (Finset.univ : Finset (Fin 8)))
        (f := fun t : Fin 8 => Complex.normSq (dft8_mode k t))
        (a := Complex.normSq (omega8 ^ k.val - 1))).symm
  rw [hfac, dft8_mode_normSq_sum]
  ring
THEOREM diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean
diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean:139 
/-- Discrete difference energy of a DFT mode is the squared magnitude of its shift eigenvalue minus 1.

This is the precise mathematical reason a `sin²(πk/8)` factor appears: it is (up to a fixed factor 4)
the spectrum of the 8-tick discrete derivative/Laplacian. -/
lemma diffEnergy8_mode (k : Fin 8) :
    diffEnergy8 (dft8_mode k) = Complex.normSq (omega8 ^ k.val - 1) := by
  unfold diffEnergy8 diff8
  -- Use that cyclic_shift (mode k) = ω^k • mode k.
  have hshift := dft8_shift_eigenvector k
  -- rewrite the difference pointwise
  have hpoint : ∀ t : Fin 8, cyclic_shift (dft8_mode k) t - dft8_mode k t =
      (omega8 ^ k.val - 1) * dft8_mode k t := by
    intro t
    have ht := congrArg (fun f => f t) hshift
    -- ht : cyclic_shift (dft8_mode k) t = (omega8 ^ k.val) • dft8_mode k t
    simp [Pi.smul_apply, smul_eq_mul] at ht
    -- subtract and factor
    calc
      cyclic_shift (dft8_mode k) t - dft8_mode k t
          = (omega8 ^ k.val) * dft8_mode k t - dft8_mode k t := by simpa [ht]
      _   = (omega8 ^ k.val - 1) * dft8_mode k t := by ring
  -- push through normSq and sum
  have hns : ∀ t : Fin 8, Complex.normSq (cyclic_shift (dft8_mode k) t - dft8_mode k t) =
      Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t) := by
    intro t
    -- use hpoint and normSq_mul
    simp [hpoint t, Complex.normSq_mul]
  simp_rw [hns]
  -- factor out the constant eigenvalue term
  have hfac :
      (∑ t : Fin 8, Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t)) =
        Complex.normSq (omega8 ^ k.val - 1) * (∑ t : Fin 8, Complex.normSq (dft8_mode k t)) := by
    -- `Finset.mul_sum` gives the reverse direction, so we use `.symm`.
    simpa using
      (Finset.mul_sum
        (s := (Finset.univ : Finset (Fin 8)))
        (f := fun t : Fin 8 => Complex.normSq (dft8_mode k t))
        (a := Complex.normSq (omega8 ^ k.val - 1))).symm
  rw [hfac, dft8_mode_normSq_sum]
  ring
THEOREM diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean
diffEnergy8_mode · IndisputableMonolith/Constants/GapWeight/Projection.lean:139 
/-- Discrete difference energy of a DFT mode is the squared magnitude of its shift eigenvalue minus 1.

This is the precise mathematical reason a `sin²(πk/8)` factor appears: it is (up to a fixed factor 4)
the spectrum of the 8-tick discrete derivative/Laplacian. -/
lemma diffEnergy8_mode (k : Fin 8) :
    diffEnergy8 (dft8_mode k) = Complex.normSq (omega8 ^ k.val - 1) := by
  unfold diffEnergy8 diff8
  -- Use that cyclic_shift (mode k) = ω^k • mode k.
  have hshift := dft8_shift_eigenvector k
  -- rewrite the difference pointwise
  have hpoint : ∀ t : Fin 8, cyclic_shift (dft8_mode k) t - dft8_mode k t =
      (omega8 ^ k.val - 1) * dft8_mode k t := by
    intro t
    have ht := congrArg (fun f => f t) hshift
    -- ht : cyclic_shift (dft8_mode k) t = (omega8 ^ k.val) • dft8_mode k t
    simp [Pi.smul_apply, smul_eq_mul] at ht
    -- subtract and factor
    calc
      cyclic_shift (dft8_mode k) t - dft8_mode k t
          = (omega8 ^ k.val) * dft8_mode k t - dft8_mode k t := by simpa [ht]
      _   = (omega8 ^ k.val - 1) * dft8_mode k t := by ring
  -- push through normSq and sum
  have hns : ∀ t : Fin 8, Complex.normSq (cyclic_shift (dft8_mode k) t - dft8_mode k t) =
      Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t) := by
    intro t
    -- use hpoint and normSq_mul
    simp [hpoint t, Complex.normSq_mul]
  simp_rw [hns]
  -- factor out the constant eigenvalue term
  have hfac :
      (∑ t : Fin 8, Complex.normSq (omega8 ^ k.val - 1) * Complex.normSq (dft8_mode k t)) =
        Complex.normSq (omega8 ^ k.val - 1) * (∑ t : Fin 8, Complex.normSq (dft8_mode k t)) := by
    -- `Finset.mul_sum` gives the reverse direction, so we use `.symm`.
    simpa using
      (Finset.mul_sum
        (s := (Finset.univ : Finset (Fin 8)))
        (f := fun t : Fin 8 => Complex.normSq (dft8_mode k t))
        (a := Complex.normSq (omega8 ^ k.val - 1))).symm
  rw [hfac, dft8_mode_normSq_sum]
  ring

What this page does not claim

The lemma does not assign physical meaning to the energy it computes. The lemma does not prove that the discrete difference energy is the correct measure for any physical application. The lemma does not establish that the total energy of an arbitrary signal equals the sum of its mode energies.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/GapWeight/Projection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND