Constants Gap Weight Projection W8 Projected

The projected weight

The declaration w8_projected is a definition in the Recognition Science framework's machine-checked library of formal theorems. It fixes the precise meaning of a "projection weight" that appears in the framework's particle mass calculations. The definition takes a dimensionless fraction, the ratio of two energy-like quantities, and multiplies it by a fixed scaling factor of 64. This converts the fraction into a per-cell integrated weight, making the normalization and measure choice explicit.

The factor of 64 is not arbitrary. It is the cardinality of the fundamental cell index set: 8 ticks on the octave clock times 8 spatial vertices in a Q₃ cell. The framework models these as two copies of the finite set Fin 8, and the product has exactly 64 elements. This is a definitional choice, a model of the underlying structure, not a theorem derived from first principles.

The numerator of the fraction is w8_dft_candidate, a candidate weight derived from a discrete Fourier transform. The denominator is the total DFT energy of the φ-pattern, which provides a Parseval normalization. The framework proves that this projected weight is nonnegative, a basic sanity property. The definition also explains why a sin²(πk/8) factor appears in the geometric weights: it is the spectral footprint of the discrete derivative on the 8-tick cycle, forced by shift-diagonalization.

What the declaration does not claim is that this projected weight equals the closed-form constant w8_from_eight_tick, which evaluates to approximately 2.49056927545. That equality is a separate, tractable but nontrivial algebraic and trigonometric reduction problem, tracked as a follow-up theorem. The declaration also does not claim that this weight is a measured physical quantity or that it predicts a particle mass; it only defines a precise mathematical object.

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

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

/-- 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 declaration does not prove that w8_projected equals the closed-form constant w8_from_eight_tick. The declaration does not claim that the projected weight is a measured physical quantity. The declaration does not establish that the projection weight predicts a specific particle mass.

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: