Constants Gap Weight Formula Geometric Weight Nonneg

The geometric weight

The geometric weight, a candidate weighting scheme, assigns a real number to each of eight frequency modes. The declaration geometricWeight_nonneg establishes a basic sanity property: for every one of the eight modes, the assigned weight is greater than or equal to zero. This is a purely formal, machine-checked statement about a definition, not an empirical measurement or a physical law.

The weight is defined as a product of two factors. The first factor is the square of the sine of a frequency term, which is always nonnegative. The second factor is a power of the golden ratio phi, specifically phi raised to the negative mode index, which is also always nonnegative because phi is positive. The lemma simply verifies that the product of two nonnegative factors is nonnegative. A companion lemma, geometricWeight_pos, goes further and shows the weight is strictly positive for all modes except the zeroth, where the weight is defined to be zero.

This weight is part of a larger, explicitly labeled scaffold. The framework's library defines a candidate weight w8_dft_candidate, built by summing, over the nonzero modes, the product of a DFT amplitude and this geometric weight. The library's own documentation states that this candidate is not currently proven to match the certified weight used in the alpha pipeline. The positivity lemma is a necessary but far from sufficient condition for the candidate to be useful; it rules out one obvious pathology but says nothing about whether the candidate is correct.

In Recognition Science, the framework models recognition events as a discrete ledger and derives structure from a forced cost function. Within that account, the geometric weight is a definitional choice, a proposed way to emphasize low-frequency modes with a geometric decay. The lemma geometricWeight_nonneg is a formal check on that choice, ensuring it does not produce nonsensical negative weights. The value of the lemma is not that it proves anything deep, but that it is a verified prerequisite for any future claim that the candidate weight is meaningful.

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

/-- Geometric weight for mode k. -/
noncomputable def geometricWeight (k : Fin 8) : ℝ :=
  if k.val = 0 then 0
  else
    let freq := (k.val : ℝ) * Real.pi / 8
    let oscillation := (Real.sin freq) ^ 2
    let phiDecay := phi ^ (-(k.val : ℤ))
    oscillation * phiDecay

/-- 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 is not proven to be the correct or certified gap weight. The lemma does not claim the candidate weight w8_dft_candidate is positive, only the individual geometric weights are nonnegative. The declaration does not establish any physical meaning for the weight, only a formal property of a definition.

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: