Constants Gap Weight Formula Phi Dftamplitude

The phi-pattern spectrum

The golden ratio φ, about 1.618, is the number that solves r² = r + 1. Its powers grow smoothly: φ⁰ = 1, φ¹ ≈ 1.618, φ² ≈ 2.618, and so on. The Recognition Science library defines a pattern that samples these powers at eight equally spaced steps, φ⁰ through φ⁷, and then asks a standard question: if you decompose that eight-number sequence into frequency components, how much energy sits in each component? The answer is the phiDFTAmplitude, a list of eight non-negative real numbers, one per frequency mode, computed by the ordinary discrete Fourier transform (DFT).

The DFT is a classical tool, used everywhere from audio engineering to image compression. It takes a sequence of values and expresses it as a sum of smooth oscillation patterns at different frequencies. The squared amplitude of each oscillation, the norm-squared of its complex coefficient, tells you how strongly that frequency appears in the original signal. The library's declaration phiDFTAmplitude is exactly that: for each of the eight frequency modes k, it returns the squared amplitude of that mode in the φ-power pattern. A companion lemma proves each of these amplitudes is non-negative, which is automatic for a squared magnitude but worth recording as a formal guarantee.

The library also defines a second quantity, geometricWeight, which assigns each mode a weight based on its frequency and a φ-decay factor. The product of amplitude and weight, summed over all nonzero modes, produces a candidate value called w8_dft_candidate. The docstring is explicit about its status: this candidate is a scaffold, not a certified constant. It is not proven to equal the framework's official w8_from_eight_tick, the value that feeds the α pipeline. The library proves only that the candidate is positive, not that it matches anything else.

In Recognition Science, the framework's own account, the eight-tick cycle and the golden ratio emerge from the forcing chain that starts with the cost function J. The φ-pattern and its DFT spectrum are a natural object to study in that context: they connect the framework's favored scaling constant to the classical mathematics of frequency analysis. But the connection is exploratory. The declaration establishes a definition and a positivity fact, nothing more. It does not claim that this candidate weight is the true gap weight, nor that the α pipeline uses it, nor that the spectrum has any physical interpretation beyond its mathematical definition.

What the declaration does give a reader is a concrete, checkable object: an eight-number sequence, its frequency decomposition, and a candidate weighted sum. The formal library records the definition and the proof that the candidate is positive. That is the whole claim. The rest, whether this candidate deserves a role in the framework's physics, remains open.

/-- The squared amplitude of mode k for the φ-pattern. -/
noncomputable def phiDFTAmplitude (k : Fin 8) : ℝ :=
  Complex.normSq (phiDFTCoeff k)

/-- phiDFTAmplitude is non-negative. -/
lemma phiDFTAmplitude_nonneg (k : Fin 8) : 0 ≤ phiDFTAmplitude k :=
  Complex.normSq_nonneg _

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

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

What this page does not claim

The declaration does not claim that w8_dft_candidate equals the certified w8_from_eight_tick. The declaration does not claim that the φ-pattern spectrum has any physical meaning beyond its mathematical definition. The declaration does not claim that the α pipeline uses this 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: