Constants Gap Weight Formula Phi Dftamplitude Nonneg

A nonnegative amplitude

The discrete Fourier transform (DFT) is a standard tool that breaks a sampled signal into its component frequencies. For any such transform, the squared amplitude of a mode is, by definition, a sum of squares and therefore cannot be negative. The declaration phiDFTAmplitude_nonneg is a machine-checked proof of exactly this fact for a specific eight-sample pattern used in the Recognition Science framework.

The pattern in question is the sequence phi^0, phi^1, ..., phi^7, where phi is the golden ratio, about 1.618. The framework's library defines this as the canonical phi-power pattern, converts it to complex numbers, and computes its DFT coefficients. The squared amplitude of each mode is then defined as the sum of the squares of the real and imaginary parts of that coefficient. The lemma phiDFTAmplitude_nonneg states that this squared amplitude is greater than or equal to zero for every one of the eight modes. Its proof is one line: it invokes the general fact that the norm squared of a complex number is nonnegative.

This lemma matters because the framework uses these amplitudes as ingredients in a candidate formula for a quantity called the gap weight. The candidate weight is a sum, over all nonzero modes, of the amplitude multiplied by a geometric weight that depends on the mode's frequency. Since both factors are nonnegative, the candidate weight itself is positive, a fact the library proves as a separate theorem. The nonnegativity lemma is the foundation for that positivity result.

What the lemma does not claim is more important than what it does. It says nothing about whether this candidate formula is the correct gap weight. The library's own documentation marks the formula as a scaffold, explicitly noting that it is not currently proven to match the certified weight used in the framework's alpha pipeline. The lemma also does not assert that the amplitudes are positive, only nonnegative; the zero mode, for instance, has zero amplitude. Finally, it makes no claim about the physical meaning of the pattern or the weight, only about a mathematical property of a defined quantity.

In plain terms, this is a small, verified building block. It certifies that a particular sum of squares is not negative, which is necessary for a later positivity result but is far from a statement about the physical world. The framework's library keeps such steps audited so that larger claims rest on checked foundations, but the scope of this particular check is deliberately narrow.

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

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

/-- 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 lemma does not prove that the candidate formula equals the certified gap weight used in the alpha pipeline. The lemma does not assert that any amplitude is positive, only that it is nonnegative. The lemma makes no claim about the physical meaning of the pattern or the 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: