schumannRS_strictMono
plain-language theorem explainer
The theorem proves that the resonance frequency function f(n) = (4n − 1)φ + 3 is strictly increasing for natural numbers n. Researchers modeling Earth-Brain resonance in the Recognition Science framework would cite it to confirm the harmonics form an ordered sequence. The short tactic proof computes the difference f(n) − f(m) as 4φ(n − m) and verifies positivity when m < n.
Claim. For all natural numbers $m, n$ with $m < n$, one has $f(m) < f(n)$, where $f(k) = (4k-1)φ + 3$ and $φ = (1 + √5)/2$.
background
The module derives the Schumann resonance harmonics from Recognition Science using only forced constants. The frequency function is given by f(n) = (4n − 1)φ + 3, where the leading 3 is the spatial dimension D forced by the eight-tick octave at T8 and the factor 4φ is the half-octave spacing derived from φ at T6. The auxiliary positivity fact asserts 0 < 4φ. This setting reproduces the five measured Schumann frequencies within 0.06 Hz. Upstream lemmas on spectral emergence supply the D-dimensional cube context, while the inflaton potential definition illustrates the J-cost manifold used elsewhere in the framework.
proof idea
The proof introduces natural numbers m and n together with the assumption m < n. It establishes that the difference between the frequencies at n and m equals 4φ times (n − m) by definition simplification and ring arithmetic. The difference is shown positive by multiplying the known positivity of 4φ with the positivity of n − m obtained from casting the natural number inequality. Linear arithmetic then yields the strict inequality.
why it matters
This monotonicity statement is invoked inside the master theorem earthBrainResonance_forced that certifies the full Earth-Brain resonance match from the Recognition Composition Law. It supplies the ordering property required for the five-harmonic sequence, relying on φ forced by self-similarity (T6) and D = 3 forced by linking and synchronization (T8). The result closes the combinatorial part of the zero-parameter prediction with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.