Encyclopedia Constants Constants Gap Weight Formula Phi Pattern Complex

ARTICLE 4 claims 3 theorems 1 model

Constants Gap Weight Formula Phi Pattern Complex

A simple definition: the golden ratio powers, written as complex numbers so a frequency analysis can be run on them.

Verify this page

The phi pattern in complex form

The golden ratio φ, about 1.618, is the number that solves r² = r + 1. It appears throughout mathematics, from the regular pentagon to the Fibonacci sequence. In the Recognition Science framework, the same number appears in a specific construction: a pattern of eight values, each one a power of φ. The first value is φ⁰ = 1, the second is φ¹ ≈ 1.618, the third is φ² ≈ 2.618, and so on up to φ⁷ ≈ 29.0. This eight-term sequence is called the canonical φ-pattern.

To study this pattern with the tools of frequency analysis, the framework's machine-checked library of formal theorems defines a companion object: the same eight real numbers, but each one marked as a complex number. A complex number is a pair of real numbers, usually written a + bi, where i is the imaginary unit. Here the imaginary part is zero for every entry, so the complex version is just a relabeling of the real pattern. The declaration phiPatternComplex makes this conversion explicit: it takes the real pattern and casts each value into the complex plane. This is a definition, not a theorem; it does not assert any property of the pattern, only names a way to view it.

Why bother with the complex form? The framework uses this pattern in a broader construction involving the discrete Fourier transform, a standard tool that decomposes a sequence of numbers into a sum of sine and cosine waves. The transform naturally operates on complex numbers, so the pattern must be cast into that form before the analysis can begin. The library then defines the transform coefficients, their squared amplitudes, and a candidate weight built from those amplitudes. That candidate weight is explicitly labeled a scaffold: it is not yet proven to match the certified weight used elsewhere in the framework's pipeline. The only verified properties attached to this construction are non-negativity: the squared amplitudes are never negative, the geometric weights are never negative, and the candidate weight is positive. These are proved in the library, but they are modest facts about the definitions, not deep claims about the physical world.

In Recognition Science, the framework models a discrete record of events, called a ledger, and derives structures from the cost of recognition. The φ-pattern is one piece of that larger apparatus, but this declaration alone does not connect to any physical measurement. It does not claim that the golden ratio is fundamental to nature, nor that the candidate weight is correct. It simply provides a formal bridge from a real sequence to its complex counterpart, so that frequency analysis can proceed.

MODEL phiPatternComplex · IndisputableMonolith/Constants/GapWeight/Formula.lean
phiPatternComplex · IndisputableMonolith/Constants/GapWeight/Formula.lean:18 
/-- Convert the real pattern to complex for DFT analysis. -/
noncomputable def phiPatternComplex : Fin 8 → ℂ :=
  fun t => (phiPattern t : ℂ)
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 _
THEOREM geometricWeight_nonneg · geometricWeight_pos · 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) _
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 _
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)

What this page does not claim

The candidate weight w8_dft_candidate is not proven to equal the certified weight used in the alpha pipeline. The declaration phiPatternComplex does not assert any property of the golden ratio itself, only defines a complex-valued sequence. No claim is made that the phi pattern or its DFT amplitudes correspond to any 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/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