Constants Gap Weight Projection

A defined weight

In Recognition Science, a ledger (a discrete record of events) uses geometric weights to balance its accounts. The constants gap weight projection is the operation that converts a scale-invariant fraction into a fixed per-cell weight. The module GapWeight.Projection defines this operation explicitly, closing an ambiguity that was historically left implicit.

The module pins down two pieces. First, it explains why the geometric weights carry a factor of sin²(πk/8). This factor is the spectral weight induced by the discrete derivative, or Laplacian, on an 8-tick cyclic shift. In discrete Fourier transform language, it is forced by shift-diagonalization. Second, it explains why the normalization uses a factor of 64. The number 64 equals 8×8, the cardinality of the fundamental interface cell when we take 8 ticks (the octave clock) and 8 spatial vertices (the Q₃ cell has 8 vertices). The normalization converts a scale-invariant fraction into a per-cell integrated weight.

The projection weight is defined as projectionScale * (rawWeightedNeutralEnergy / totalEnergy). Here projectionScale is 64, the raw weighted neutral energy is w8_dft_candidate, and the total energy is the sum of the DFT amplitudes of the φ-pattern, a Parseval denominator. The module proves the projection weight is nonnegative, and it proves the canonical counts: 8 ticks, 8 vertices, and 64 cells.

The module also establishes why the sin²(πk/8) factor is canonical. It defines a discrete one-step difference on the 8-tick cycle, (S - I)v, and the total squared energy of that difference. A lemma shows that the discrete difference energy of a DFT mode equals the squared magnitude of its shift eigenvalue minus 1. This is the precise mathematical reason the sin²(πk/8) factor appears: it is, up to a fixed factor of 4, the spectrum of the 8-tick discrete derivative or Laplacian.

The module does not prove that this projected weight equals the pipeline constant w8_from_eight_tick, which evaluates to approximately 2.49056927545. That equality is a tractable but nontrivial algebraic and trigonometric reduction problem, tracked as a follow-up theorem. What the module does establish is the definition-level closure of what projection weight means, making the operator and measure choice explicit with no hidden degree of freedom.

/-- **Projection weight** of the φ-pattern onto the 8-tick basis:

`projectionScale * (rawWeightedNeutralEnergy / totalEnergy)`.

This makes the normalization and measure choice explicit. -/
noncomputable def w8_projected : ℝ :=
  projectionScale * (w8_dft_candidate / phiDFTEnergyTotal)

@[simp] theorem N_cell_eq : N_cell = 64 := by
  -- card (Fin 8 × Fin 8) = 8 * 8
  decide

/-- 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

lemma w8_projected_nonneg : 0 ≤ w8_projected := by
  unfold w8_projected
  have hscale : 0 ≤ projectionScale := by simp [projectionScale]
  have hnum : 0 ≤ w8_dft_candidate := le_of_lt w8_dft_candidate_pos
  have hden : 0 ≤ phiDFTEnergyTotal := phiDFTEnergyTotal_nonneg
  -- If total energy is 0, then the ratio is 0 (since numerator is 0 as well). Otherwise nonneg by div_nonneg.
  by_cases hE : phiDFTEnergyTotal = 0
  · simp [hE, hnum, hscale]
  · have hdiv : 0 ≤ w8_dft_candidate / phiDFTEnergyTotal := div_nonneg hnum (le_of_lt (lt_of_le_of_ne' hden hE))
    exact mul_nonneg hscale hdiv

What this page does not claim

The module does not prove w8_projected equals the pipeline constant w8_from_eight_tick. The sin²(πk/8) factor is derived from a discrete derivative, not from a continuous Laplacian. The projection weight is a definition, not a measured physical quantity.

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: