f_Schumann_RS_pos
plain-language theorem explainer
The theorem asserts that the BIT carrier frequency, defined as five times the golden ratio in hertz, is strictly positive. Researchers deriving Schumann resonances from the Recognition Science framework cite it to anchor the predicted band before comparing to the empirical 7.83 Hz value. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic to the positivity of the golden ratio.
Claim. Let $f = 5phi$ denote the BIT carrier frequency in hertz, where $phi$ is the golden ratio. Then $f > 0$.
background
The module identifies the Schumann resonance fundamental with the BIT carrier frequency $f = 5 phi$ Hz. This follows from the gauge-boson-mass scaffolding of Foundation.RecognitionSpectrum together with the eight-tick octave of T7 in the forcing chain. The definition sets this frequency to five times phi, and the positivity result is a prerequisite for the master certificate that collects all structural properties of the resonance.
proof idea
The proof unfolds the definition of the frequency to 5 times phi, applies the known positivity of phi, and uses linear arithmetic to conclude the inequality.
why it matters
This result populates the positivity component of the master certificate schumannResonanceCert. It supports the structural theorem linking the empirical Schumann frequency 7.83 Hz to the predicted BIT carrier band derived from the phi-ladder and the eight-tick octave. The module notes that a measurement outside [7.5, 8.10] Hz would falsify the identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.