Encyclopedia Constants Constants Gap Weight Formula W8 Dft Candidate Pos

ARTICLE 3 claims 2 theorems 1 model

Constants Gap Weight Formula W8 Dft Candidate Pos

A machine-checked proof that a proposed formula for a recognition-cycle weight is positive, with the honest caveat that the formula is a scaffold, not the certified value.

Verify this page

The candidate weight

The declaration w8_dft_candidate_pos proves a narrow but useful fact: a particular proposed formula for a weight, built from a discrete Fourier transform of a golden-ratio pattern, always gives a positive number. The weight in question is meant to sit inside the Recognition Science framework's account of an eight-tick recognition cycle, where the framework models a discrete record of events, a ledger, and the cost of recognizing each event is forced by five plain conditions. The candidate formula combines two pieces: the squared amplitude of each of eight frequency modes, and a geometric weight that decays by powers of the golden ratio while oscillating sinusoidally. The theorem states that when you sum these products over all nonzero modes, the result is strictly greater than zero.

The proof is direct and machine-checked in the framework's library, a collection of formal theorems verified by a computer. It rests on two lemmas: the squared amplitude of any mode is nonnegative because it is the squared norm of a complex number, and the geometric weight is positive for every nonzero mode because it is a product of a squared sine and a positive power of the golden ratio. Since the sum includes at least one nonzero mode, the total must be positive. The declaration itself is a theorem in the library, meaning it is fully proved from the definitions with no gaps.

What the declaration does not claim matters as much as what it proves. The name of the file says it plainly: this is a candidate weight, a scaffold for exploration. The library's own documentation states that this DFT-based candidate is not currently proven to match the certified weight w8_from_eight_tick that the framework's alpha pipeline actually uses. The positivity theorem says nothing about whether the candidate equals the certified value, whether it is the right weight for any physical prediction, or whether the DFT construction has any special status. It only guarantees that the proposed formula yields a positive number, which is a necessary but far from sufficient condition for the candidate to be useful.

The practical consequence is modest but real: anyone exploring this candidate formula can rely on its positivity without re-checking the algebra. The theorem clears one hurdle, and the remaining question, whether this candidate is the true weight, stays open in the library's own accounting.

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 phiDFTAmplitude_nonneg · geometricWeight_pos · 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 _
geometricWeight_pos · IndisputableMonolith/Constants/GapWeight/Formula.lean:68 
/-- geometricWeight is positive for neutral modes. -/
lemma geometricWeight_pos {k : Fin 8} (hk : k.val ≠ 0) : 0 < geometricWeight k := by
  unfold geometricWeight
  simp only [hk, ↓reduceIte]
  apply mul_pos
  · apply sq_pos_of_pos
    apply Real.sin_pos_of_pos_of_lt_pi
    · have hk_pos : 0 < k.val := Nat.pos_of_ne_zero hk
      positivity
    · have h1 : k.val ≤ 7 := Nat.lt_succ_iff.mp k.isLt
      have h2 : (k.val : ℝ) ≤ 7 := by exact Nat.cast_le.mpr h1
      calc (k.val : ℝ) * Real.pi / 8
          ≤ 7 * Real.pi / 8 := by nlinarith [Real.pi_pos]
        _ < Real.pi := by nlinarith [Real.pi_pos]
  · exact zpow_pos phi_pos _
MODEL w8_dft_candidate · IndisputableMonolith/Constants/GapWeight/Formula.lean
w8_dft_candidate · IndisputableMonolith/Constants/GapWeight/Formula.lean:45 
/-- A DFT-based candidate weight (scaffold).

This is *not* currently proven to match the certified `Constants.w8_from_eight_tick`
used by the α pipeline (see `Constants/GapWeight.lean`). -/
noncomputable def w8_dft_candidate : ℝ :=
  Finset.sum (Finset.filter (· ≠ 0) Finset.univ) fun k =>
    phiDFTAmplitude k * geometricWeight k

What this page does not claim

The candidate weight equals the certified w8_from_eight_tick value. The DFT construction has any special physical status beyond being a proposed scaffold. The positivity of the candidate is sufficient for it to be the correct 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