module module moderate

`IndisputableMonolith.Physics.EarthBrainResonance`

The module states the RS-predicted Schumann harmonic frequencies f(n) = (4n-1)φ + 3 for n ≥ 1. Atmospheric physicists or researchers linking global resonances to biological rhythms would cite these expressions. It consists of a collection of definitions and equalities that tie the golden ratio to measured harmonic values and dimension-dependent relations.

claimThe central object is the frequency $f(n) = (4n-1)\phi + 3$ for integer $n \geq 1$, together with the supporting statements schumannRS, schumannMeasured, harmonic1_eq through harmonic5_eq, fundamental_eq_D_phi_sq and three_phi_sq_eq_phi4_plus_1.

background

The module imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants and works inside the Recognition Science setting where φ is the self-similar fixed point. It introduces the predicted Schumann frequency via the formula given in the module doc-comment and supplies auxiliary bounds phi_gt_1618, phi_lt_1619 together with the five explicit harmonic equalities. Additional relations connect the expressions to D = 3 spatial dimensions through fundamental_eq_D_phi_sq and the algebraic identity three_phi_sq_eq_phi4_plus_1.

proof idea

This is a definition module, no proofs. It declares the frequency formula, the comparison between predicted and measured values, and the supporting phi and dimension identities as sibling definitions and equations.

why it matters in Recognition Science

The module supplies the concrete frequency predictions that link the phi-ladder and D = 3 to observed Schumann resonances, thereby feeding the EarthBrainResonance application. It closes the step from the T6 phi fixed-point result to a testable physical observable.

scope and limits

Does not derive the frequency formula from the forcing chain inside this module.
Does not perform numerical evaluation or error analysis against data.
Does not extend the harmonic list past the five explicit cases.
Does not address coupling to brain-wave models beyond the module title.

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