carrierFreq_pos
plain-language theorem explainer
The theorem establishes that the carrier frequency 5φ is strictly positive. Researchers modeling the DFT-8 harmonic spectrum for brain-rhythm combs cite it to place the fundamental mode inside the theta band. The proof is a one-line term-mode reduction that unfolds the definition and applies multiplication positivity to the constant 5 and phi_pos.
Claim. $0 < 5φ$ where $φ$ is the self-similar fixed point of the Recognition Science framework.
background
The module CrossDomain.DFTHarmonicSpectrum defines the eight-mode DFT frequency comb ν_k = (k · 5φ / 8) Hz for k = 0..7, with carrier frequency 5φ ≈ 8.09 Hz lying in the theta band. The definition carrierFreq := 5 * phi supplies the fundamental scale; phi itself originates in the Foundation layer as the fixed point forced by the J-uniqueness relation. The sibling band operation from PreLogicalCost performs arithmetic conjunction on stable states (0/1 multiplication) but is not invoked in this positivity check.
proof idea
Unfolds carrierFreq to the product 5 * phi, then applies the mul_pos lemma with norm_num discharging 5 > 0 and the upstream phi_pos lemma supplying 0 < phi.
why it matters
Positivity of the carrier anchors the entire RS frequency comb inside the positive reals and confirms placement within the theta band as required by the module's structural claim (RS_PAT_026). It supplies the base case for sibling results on non-negative harmonics and mode ordering, consistent with the eight-tick octave and T7 period-8 structure. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.