Encyclopedia Constants Constants Gap Weight Projection Diff Energy8 Nonneg

ARTICLE 3 claims 3 theorems

Constants Gap Weight Projection Diff Energy8 Nonneg

A machine-checked proof that a certain way of measuring change on an eight-step cycle can never give a negative number, and what that proof does not say.

Verify this page

The discrete difference energy

In classical terms, the object is a discrete difference operator. Given a sequence of eight complex numbers arranged on a circle, take each number, subtract its predecessor, and sum the squared magnitudes of those eight differences. That sum is the discrete difference energy. The lemma diffEnergy8_nonneg proves, in the machine-checked library of formal theorems, that this sum is always greater than or equal to zero. The proof is short: each squared magnitude is nonnegative, and a sum of nonnegative terms is nonnegative.

The result belongs to a family of standard facts in Fourier analysis. The discrete derivative on an eight-point cycle is a linear operator, and its eigenvalues are the numbers ω^k − 1, where ω is a primitive eighth root of unity. The squared magnitude of each such eigenvalue is proportional to sin²(πk/8). This is the spectral footprint of the derivative: it explains why the factor sin²(πk/8) appears when one projects a pattern onto the eight frequency modes. The lemma diffEnergy8_mode states this connection precisely: the difference energy of a mode equals the squared magnitude of its shift eigenvalue minus one.

In Recognition Science, this lemma serves a bookkeeping role. The framework models recognition events as a discrete ledger, and the eight-tick cycle is its fundamental clock. The lemma guarantees that a certain measure of change, the energy of the difference between a pattern and its shifted copy, is a well-behaved nonnegative quantity. That is all it does. It does not prove that any particular pattern has positive energy, nor does it fix the value of any constant. It is a hygiene result: it certifies that a quantity used in later definitions cannot go negative.

The lemma also does not compare the projected weight w8_projected to the closed-form constant w8_from_eight_tick. That comparison is a separate, tractable algebraic problem, explicitly tracked as a follow-up theorem. The nonnegativity lemma is a foundation stone, not a bridge.

THEOREM diffEnergy8_nonneg · IndisputableMonolith/Constants/GapWeight/Projection.lean
diffEnergy8_nonneg · IndisputableMonolith/Constants/GapWeight/Projection.lean:117 
lemma diffEnergy8_nonneg (v : Fin 8 → ℂ) : 0 ≤ diffEnergy8 v := by
  unfold diffEnergy8
  exact Finset.sum_nonneg (fun _ _ => Complex.normSq_nonneg _)
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

This lemma does not prove that any particular pattern has positive difference energy. This lemma does not establish the value of any physical constant. This lemma does not prove the equality between w8_projected and w8_from_eight_tick.

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