empirical_within_two_J_phi_of_band
plain-language theorem explainer
The theorem confirms that the empirical Schumann fundamental of 7.83 Hz satisfies 7.83 + 2 J(phi) > 8.05, placing it within two J-cost units of the predicted lower band edge. ELF resonance modelers would reference this bound when validating the BIT carrier assignment against observation. The proof unfolds the constant definitions and applies linear arithmetic after citing the lower bound on phi.
Claim. $7.83 + 2 J_0 > 8.05$ where $J_0 = J_0 = phi - 3/2$ is the golden-section J-cost in Hz units and 7.83 Hz is the recorded empirical Schumann fundamental.
background
The module treats the Earth-ionosphere cavity as supporting a transverse electromagnetic mode whose fundamental is identified with the BIT carrier 5 phi Hz. This carrier lies in the interval (8.05, 8.10) Hz by the eight-tick octave construction. The empirical datum is fixed at the constant 7.83 Hz. J_phi_Hz is defined as phi - 3/2, the canonical golden-section J-cost ceiling expressed in frequency units. The upstream lemma phi_gt_onePointSixOne supplies the strict lower bound phi > 1.61 used in the arithmetic check. Module documentation notes that the small deficit relative to the upper edge is accounted for by the 1/45 K-gate suppression on the consciousness-sector contribution to cavity Q.
proof idea
The proof is a term-mode script. It unfolds the definitions of f_Schumann_empirical and J_phi_Hz to obtain the concrete expression 7.83 + 2*(phi - 3/2) > 8.05. The lemma phi_gt_onePointSixOne is introduced to supply phi > 1.61, after which linarith closes the inequality by linear arithmetic over the reals.
why it matters
This bound supplies the final numerical ingredient required by the master one-statement theorem schumann_one_statement, which packages the full identification of the Schumann fundamental with the BIT carrier together with the empirical proximity claim. It thereby completes the structural theorem for the eight-tick octave mode in the RS framework. The module documentation supplies the falsifier: a median fundamental outside [7.5, 8.10] Hz after diurnal correction would refute the carrier assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.