schumannResonanceCert
plain-language theorem explainer
The schumannResonanceCert definition populates the seven-field master certificate that equates the Schumann fundamental to the BIT carrier 5 phi Hz and verifies its placement inside the (8.05, 8.10) Hz interval together with empirical compatibility. Recognition Science astrophysicists cite it to close the structural identification of the Earth-ionosphere cavity mode. Construction is a direct structure literal that discharges the equality by reflexivity and imports the six supporting lemmas for positivity, band bounds, and the J(phi) distance to
Claim. The master certificate is inhabited: the Schumann fundamental satisfies $f = 5phi$ Hz, $0 < f$, $8.05 < f < 8.10$, $7.5 < f$, $f < 8.10$, $0 < J(phi)$ (in Hz), and the empirical value obeys $7.83 + 2J(phi) > 8.05$.
background
The module identifies the BIT carrier, defined as the canonical Hz-scale oscillation 5 phi drawn from the gauge-boson scaffolding and the eight-tick octave of T7, with the fundamental Schumann resonance. f_Schumann_RS stands for this carrier frequency; J_phi_Hz is the J-cost of phi expressed in hertz. The upstream theorem empirical_within_two_J_phi_of_band states that the observed 7.83 Hz lies within 2 J(phi) of the predicted lower edge 8.05 Hz. Supporting lemmas establish positivity, the open interval (8.05, 8.10), and the stricter bounds 7.5 < f and f < 8.10.
proof idea
The definition builds an instance of the SchumannResonanceCert structure by supplying each of its seven fields. The equality clause is discharged by rfl. The remaining six fields are filled by direct reference to the upstream theorems f_Schumann_RS_pos, f_Schumann_RS_band, f_Schumann_RS_above_seven_point_five, f_Schumann_RS_below_eight_point_one, J_phi_Hz_pos, and empirical_within_two_J_phi_of_band.
why it matters
This definition completes the structural theorem for the Schumann resonance by inhabiting the master certificate that collects all seven clauses. It rests on the phi-ladder and the eight-tick octave (T7) that fix the carrier at 5 phi Hz, and it records the same 1/45 K-gate suppression factor that appears in the muon g-2 calculation. With zero recorded downstream uses it functions as the terminal summary object for the BIT carrier identification in the astrophysics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.