pith. machine review for the scientific record. sign in
def definition def or abbrev high

carrierFreq

show as:
view Lean formalization →

Carrier frequency is set to 5φ to anchor the DFT-8 spectrum in the theta band near 8.09 Hz. RS brain-rhythm researchers cite it as the base for the eight-mode frequency comb ν_k = k·5φ/8. The declaration is a direct definition with no computational content.

claimThe carrier frequency is defined as $5φ$, where $φ$ is the golden ratio.

background

The module defines the DFT-8 Harmonic Spectrum as eight modes with frequencies ν_k = (k · 5φ / 8) Hz for k = 0 to 7, one per Q₃ vertex. The carrier 5φ ≈ 8.09 Hz places the comb in the theta band and supplies the scaling for all harmonics. Phi is the self-similar fixed point from upstream Constants and the forcing chain T6.

proof idea

One-line definition that directly assigns the product 5 * phi to carrierFreq.

why it matters in Recognition Science

This supplies the base frequency used by DFTHarmonicSpectrumCert to certify eight modes, theta-band bounds, and non-negative harmonics. It realizes the C24 structural claim in the module documentation for RS_PAT_026 and RS_PAT_025. It instantiates the eight-tick octave from the Recognition Science framework.

scope and limits

formal statement (Lean)

  38noncomputable def carrierFreq : ℝ := 5 * phi

proof body

Definition body.

  39

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.