Encyclopedia Constants Constants Gap Weight Formula Geometric Weight

ARTICLE 4 claims 3 theorems 1 model

Constants Gap Weight Formula Geometric Weight

A formula that assigns each frequency in an eight-step pattern a weight, combining how fast it oscillates with how fast it decays.

Verify this page

The geometric weight

A geometric weight is a number assigned to each of eight frequency modes, or oscillation patterns, in a discrete signal. The formula takes two factors and multiplies them. The first factor is the squared sine of the frequency, which measures how much the mode oscillates. The second factor is the golden ratio raised to a negative power, which makes higher modes decay geometrically. The weight for the zero mode is set to zero. In plain terms, the weight rewards modes that oscillate and penalizes modes that decay quickly, with the balance set by the golden ratio.

The formula was introduced in a machine-checked library of formal theorems as part of a larger project on recognition cycles. The library defines the weight for each of the eight modes and proves two basic facts about it. First, the weight is never negative. Second, the weight is strictly positive for every mode except the zero mode, which is exactly zero. These are the only properties of the weight that have been verified in the library. The weight itself is a definition, a choice of how to assign numbers, not a derived result.

The library also defines a candidate weight for a specific gap by summing the product of each mode's amplitude and its geometric weight. That candidate is shown to be positive, but it is explicitly marked as a scaffold. The library states that this candidate is not currently proven to match the certified weight used in the alpha pipeline. The geometric weight is therefore a building block, not a finished bridge.

In Recognition Science, the weight appears as one ingredient in a larger story about how an eight-tick cycle might connect to physical constants. The framework models a discrete record of events, and this weight is a proposed way to emphasize certain frequencies over others. The definition is a model, not a theorem. What the library proves is only the non-negativity and positivity of the weight, and the positivity of the summed candidate.

The practical consequence is that the weight is usable as a filter: it selects modes that oscillate and suppresses those that do not, while preserving all values non-negative. That property matters for any later step that needs a probability-like or amplitude-like quantity. But the weight does not by itself establish any connection to measured physics. That connection, if it exists, would have to come from further theorems that are not in this part of the library.

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 geometricWeight_pos · IndisputableMonolith/Constants/GapWeight/Formula.lean
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)
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 geometric weight does not establish any connection to measured physical constants. The geometric weight is not proven to be the unique or optimal weight for any purpose. The candidate weight is not the certified weight used in the alpha pipeline.

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