phi_lt_1619
The lemma establishes that the golden ratio is strictly less than 1.619. It is invoked by the bounding and matching theorems for the first four Schumann harmonics inside the Earth-Brain Resonance module. The proof reduces the claim to a numerical comparison on the square root of five and discharges the arithmetic with linarith.
claimLet $phi = (1 + sqrt(5))/2$. Then $phi < 1.619$.
background
The Earth-Brain Resonance module constructs Schumann frequencies from the Recognition Science forcing chain. The golden ratio phi is the self-similar fixed point fixed by T6; the spatial dimension D equals 3 by T8. The zero-parameter formula is f(n) = (4n - 1) phi + 3, which expands to D phi^2 + (n-1)(D+1) phi. This lemma supplies the strict upper bound required to certify that the predicted values lie inside the measured intervals (7.83 Hz, 14.3 Hz, 20.8 Hz, 27.3 Hz).
proof idea
The tactic sequence first unfolds the definition of phi. It proves sqrt(5) < 2.238 by showing 5 < (2.238)^2 and invoking the monotonicity of the square-root function on the non-negative reals. Linear arithmetic then concludes the target inequality.
why it matters in Recognition Science
The bound is used directly by harmonic1_bounds, harmonic2_bounds, harmonic3_bounds, harmonic4_bounds and the alpha-beta ratio theorem to obtain the numerical matches within 0.03-0.04 Hz. It anchors the zero-parameter claim that links the eight-tick octave and three-dimensional forcing to the observed Earth cavity spectrum and EEG band boundaries. No scaffolding remains; the lemma is a finished numerical anchor.
scope and limits
- Does not establish the matching lower bound on phi.
- Does not derive phi from the forcing axioms inside this module.
- Does not extend the inequality to non-real or matrix-valued analogues.
- Does not quantify the distance to the true value of phi beyond the stated threshold.
formal statement (Lean)
79private lemma phi_lt_1619 : phi < (1.619 : ℝ) := by
proof body
Tactic-mode proof.
80 simp only [phi]
81 have h5 : Real.sqrt 5 < (2.238 : ℝ) := by
82 have h : (5 : ℝ) < (2.238 : ℝ) ^ 2 := by norm_num
83 rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.238)]
84 exact Real.sqrt_lt_sqrt (by norm_num) h
85 linarith
86
87/-! ## Part II: The Schumann Formula
88
89**Definition**: f(n) = (4n − 1)·φ + 3
90
91This is the RS prediction for the n-th Schumann harmonic (n ≥ 1).
92Uses only D = 3 (T8) and φ (T6). Zero free parameters. -/
93
94/-- RS-predicted n-th Schumann harmonic frequency.
95 f(n) = (4n − 1)·φ + 3, valid for n ≥ 1. -/