f_Schumann_empirical
plain-language theorem explainer
The definition records the accepted empirical Schumann resonance fundamental as the real constant 7.83 Hz. Recognition theorists cite it to anchor the BIT carrier 5 phi Hz against 1952 data when testing the predicted band. The entry is a bare numeric assignment with no reduction steps.
Claim. Let $f_{Schumann,emp} := 7.83$ denote the measured fundamental frequency (in Hz) of the Earth-ionosphere cavity resonance.
background
The module identifies the Schumann fundamental with the BIT carrier oscillation at 5 phi Hz, where phi is the self-similar fixed point forced by the T5-T7 chain. J(phi) supplies the J-cost distance in Hz units that quantifies the observed deficit. Upstream results supply the canonical arithmetic object (realization-independent Peano surface) and the cost function on recognition events (derived from the multiplicative comparator), ensuring the carrier derivation inherits the invariant arithmetic content.
proof idea
One-line definition that directly assigns the literal constant 7.83. No lemmas or tactics are invoked.
why it matters
The constant supplies the left-hand side for empirical_below_predicted_upper and empirical_within_two_J_phi_of_band, which close the master certificate SchumannResonanceCert and the one-statement theorem schumann_one_statement. It tests the T7 eight-tick octave prediction against observation, with the J(phi) deficit structurally tied to the 1/45 K-gate factor on cavity Q.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.