module module high

`IndisputableMonolith.Physics.EarthBrainResonance`

The module defines the RS-predicted n-th Schumann harmonic frequency via f(n) = (4n − 1)·φ + 3 for n ≥ 1. Geophysicists or RS modelers comparing theory to the observed 7.83 Hz fundamental would cite these objects. The module consists of direct definitions plus auxiliary bounds on φ, with no inductive steps or external lemmas beyond the constants import.

claimThe RS-predicted frequency of the n-th Schumann harmonic is given by $f(n) = (4n-1)φ + 3$ for integer $n ≥ 1$, where $φ$ is the golden ratio.

background

The module sits in the Physics domain and imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum τ₀ = 1 tick. It introduces the frequency formula together with the five explicit harmonic equalities and the two-sided bounds phi_gt_1618 and phi_lt_1619 that pin φ numerically. The local setting therefore supplies concrete RS-native predictions for Earth electromagnetic resonances without further derivation.

proof idea

This is a definition module, no proofs. The structure consists of direct definitions of the frequency formula, the five harmonic equalities, and the two numerical bounds on φ.

why it matters in Recognition Science

The module supplies the RS Schumann frequency predictions that can be referenced by any downstream treatment of resonance phenomena in the Physics domain. No used_by edges are recorded, so its immediate parent is the broader Recognition Science forcing chain that already fixes φ and the eight-tick structure.

scope and limits

Does not derive the frequency formula from the Recognition Composition Law.
Does not contain measured data or statistical comparison.
Does not extend the formula past the first five harmonics.
Does not address units conversion from RS-native ticks.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (42)

lemma phi_gt_1618 L71
lemma phi_lt_1619 L79
def schumannRS L96
def schumannMeasured L99
theorem harmonic1_eq L110
theorem harmonic2_eq L113
theorem harmonic3_eq L116
theorem harmonic4_eq L119
theorem harmonic5_eq L122
abbrev D L130
theorem fundamental_eq_D_phi_sq L133
theorem three_phi_sq_eq_phi4_plus_1 L138
theorem fundamental_eq_phi4_plus_1 L142
theorem spacing_eq L146
theorem spacing_pos L151
theorem schumannRS_strictMono L155
theorem harmonic1_bounds L170
theorem harmonic1_matches L174
theorem harmonic2_bounds L179
theorem harmonic2_matches L183
theorem harmonic3_bounds L188
theorem harmonic3_matches L192
theorem harmonic4_bounds L197
theorem harmonic4_matches L201
theorem harmonic5_bounds L206
theorem harmonic5_matches L210
theorem all_harmonics_match L215
def inFreqBand L234
theorem harmonic1_in_theta L238
theorem fundamental_near_theta_alpha_boundary L243
theorem harmonic2_in_beta L248
theorem harmonic3_in_beta L253
theorem harmonic4_in_beta L258
theorem harmonic5_in_gamma L263
theorem schumann_spans_eeg_bands L269
theorem alpha_beta_ratio_near_phi L284
theorem spacing_bounds L289
inductive Provenance L297
structure EarthBrainResonanceCert L302
def earthBrainResonance_forced L341
structure FalsificationCriteria L359
def falsification L372