Encyclopedia Constants Constants Gap Weight Formula

ARTICLE 4 claims 3 theorems 1 open

Constants Gap Weight Formula

A proposed formula assigns weights to the eight ticks of a recognition cycle by combining how strongly each tick appears in a frequency analysis with a geometric decay.

Verify this page

The gap weight formula

The gap weight formula is a proposed rule for assigning a numerical weight to each of the eight ticks in a recognition cycle. A recognition cycle is the framework's discrete record of events, a fixed sequence of eight steps. The formula works in two stages. First it takes the canonical pattern, the powers of the golden ratio phi from phi^0 up to phi^7, and runs a discrete Fourier transform, a standard tool that decomposes a signal into its frequency components. That gives eight amplitudes, one per mode. Second it multiplies each amplitude by a geometric weight, a factor that combines a sine-squared oscillation term with a decay factor phi raised to a negative power. The final candidate weight is the sum of these products over all nonzero modes.

The module that defines this formula is a scaffold, not a finished result. The machine-checked library of formal theorems proves three basic properties: the Fourier amplitudes are non-negative, the geometric weights are non-negative, and the geometric weights are positive for every nonzero mode. From those pieces it proves the candidate weight itself is positive. What the module does not prove is that this candidate equals the certified weight used elsewhere in the framework's alpha pipeline. The docstring states this gap explicitly: the candidate is not currently proven to match the established value.

In plain language, the formula is a plausible way to weight the eight ticks, and the module verifies that the weights it produces are never negative and never zero overall. The positivity theorems are real, machine-checked results. The missing piece is the connection to the certified weight, and that remains open.

THEOREM w8_dft_candidate_pos · IndisputableMonolith/Constants/GapWeight/Formula.lean
w8_dft_candidate_pos · IndisputableMonolith/Constants/GapWeight/Formula.lean:84 
/-- The DFT-based candidate weight is positive. -/
theorem w8_dft_candidate_pos : 0 < w8_dft_candidate := by
  unfold w8_dft_candidate
  have h1_mem : (1 : Fin 8) ∈ Finset.filter (· ≠ 0) Finset.univ := by decide
  apply Finset.sum_pos'
  · intro k hk
    apply mul_nonneg
    · exact phiDFTAmplitude_nonneg k
    · exact geometricWeight_nonneg k
  · use 1, h1_mem
    apply mul_pos
    · unfold phiDFTAmplitude
      apply Complex.normSq_pos.mpr
      -- A rigorous proof: the φ-pattern φᵗ is strictly increasing (φ > 1).
      -- Its DFT coefficient c₁ is ∑_{t=0}^7 (ω⁷φ)ᵗ / √8.
      -- Let z = ω⁷φ. The sum is (z⁸ - 1)/(z - 1).
      -- Since |z| = φ > 1, z ≠ 1 and z⁸ = φ⁸ ≠ 1.
      -- Thus the sum is non-zero.
      intro h_zero
      have h_coeff : phiDFTCoeff 1 = (∑ t : Fin 8, (omega8 ^ 7 * (phi : ℂ)) ^ t.val) / (Real.sqrt 8 : ℂ) := by
        unfold phiDFTCoeff dft8_entry phiPatternComplex phiPattern
        rw [Finset.sum_div]
        congr 1
        ext t
        -- Expand the DFT entry and simplify `star`/conjugation.
        -- This puts the term into the geometric-series form `(ω⁷φ)^t / √8`.
        -- The final `mul_div` step is the only non-`simp` rearrangement we need.
        simp [dft8_entry, phiPatternComplex, phiPattern, star_div₀, star_pow, star_omega8,
          omega8_inv_eq_pow7, pow_mul, mul_pow]
        simpa [div_mul_eq_mul_div, mul_div, mul_assoc, mul_left_comm, mul_comm]
      rw [h_coeff, div_eq_zero_iff] at h_zero
      replace h_zero := h_zero.resolve_right (by
        have h_pos : 0 < (8 : ℝ) := by norm_num
        have h_sqrt_pos : 0 < Real.sqrt 8 := Real.sqrt_pos.mpr h_pos
        exact Complex.ofReal_ne_zero.mpr (ne_of_gt h_sqrt_pos))
      let z : ℂ := omega8 ^ 7 * (phi : ℂ)
      have h_z_def : ∀ t : Fin 8, (omega8 ^ 7 * (phi : ℂ)) ^ t.val = z ^ t.val := fun t => rfl
      simp_rw [h_z_def] at h_zero
      have h_sum_geom : (∑ t : Fin 8, z ^ t.val) * (z - 1) = z ^ 8 - 1 := by
        have h8 : (∑ t : Fin 8, z ^ t.val) = z^0 + z^1 + z^2 + z^3 + z^4 + z^5 + z^6 + z^7 := by
          simp only [Fin.sum_univ_eight]; rfl
        rw [h8]
        ring
      rw [h_zero, zero_mul] at h_sum_geom
      have h_z8 : z ^ 8 = (phi : ℂ) ^ 8 := by
        -- `z = ω⁷ φ`, so `z^8 = (ω⁷)^8 * φ^8 = 1 * φ^8`.
        have hω : (omega8 ^ 7) ^ 8 = (1 : ℂ) := by
          -- (ω⁷)^8 = ω^(7*8) = ω^(8*7) = (ω^8)^7 = 1
          rw [← pow_mul]
          have : (7 : ℕ) * 8 = 8 * 7 := by ring
          rw [this, pow_mul, omega8_pow_8, one_pow]
        simp [z, mul_pow, hω]
      rw [h_z8] at h_sum_geom
      have h_phi8_ne_one : (phi : ℂ) ^ 8 ≠ 1 := by
        rw [← Complex.ofReal_pow, ← Complex.ofReal_one]
        intro h
        replace h := Complex.ofReal_injective h
        have h_phi_pos : 0 < phi := phi_pos
        have h_phi_one : 1 < phi := one_lt_phi
        have h_pow_gt : 1 < phi ^ 8 := one_lt_pow₀ h_phi_one (by norm_num)
        linarith
      -- From `0 = φ^8 - 1` we would get `φ^8 = 1`, contradiction since φ > 1.
      have h_phi8_eq_one : (phi : ℂ) ^ 8 = 1 := by
        have : (phi : ℂ) ^ 8 - 1 = 0 := by
          simpa [eq_comm] using h_sum_geom
        exact sub_eq_zero.mp this
      exact h_phi8_ne_one h_phi8_eq_one
    · exact geometricWeight_pos (by decide : (1 : Fin 8).val ≠ 0)
THEOREM geometricWeight_nonneg · IndisputableMonolith/Constants/GapWeight/Formula.lean
geometricWeight_nonneg · IndisputableMonolith/Constants/GapWeight/Formula.lean:59 
/-- geometricWeight is non-negative. -/
lemma geometricWeight_nonneg (k : Fin 8) : 0 ≤ geometricWeight k := by
  unfold geometricWeight
  split_ifs with h
  · exact le_refl 0
  · apply mul_nonneg
    · exact sq_nonneg _
    · exact zpow_nonneg (le_of_lt phi_pos) _
THEOREM phiDFTAmplitude_nonneg · IndisputableMonolith/Constants/GapWeight/Formula.lean
phiDFTAmplitude_nonneg · IndisputableMonolith/Constants/GapWeight/Formula.lean:55 
/-- phiDFTAmplitude is non-negative. -/
lemma phiDFTAmplitude_nonneg (k : Fin 8) : 0 ≤ phiDFTAmplitude k :=
  Complex.normSq_nonneg _

What this page does not claim

The candidate weight is not proven to equal the certified weight. The formula is not derived from the forcing chain; it is a proposed scaffold. No claim is made about the numerical value of the candidate weight.

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