phi_bounds
plain-language theorem explainer
Physicists deriving forced electron mass values in the Recognition Science framework cite this lemma to pin the golden ratio phi inside a 10^{-6} interval. It supplies the numerical anchor required for gap and logarithm bounds that close the T9 necessity argument. The proof works by establishing tight square bounds on √5 via direct comparison and norm_num, then substituting into the definition of phi and applying division inequalities with linarith.
Claim. $1.618033 < phi < 1.618034$ where $phi = (1 + sqrt(5))/2$.
background
The module belongs to the T9 necessity section, which shows that the electron mass formula is forced from T8 ledger quantization together with geometric constants obtained earlier. Phi is the golden ratio, the self-similar fixed point forced at T6 of the unified forcing chain. Upstream results supply a coarser version 1 < phi < 2 in MassToLight and an identical tight interval in GapProperties.
proof idea
The tactic proof first constructs sqrt5_lower by showing (2.236066)^2 < 5 and applying Real.sqrt_lt_sqrt after rewriting the square root. It builds sqrt5_upper symmetrically by showing 5 < (2.236068)^2. After unfolding phi it splits the conjunction and uses div_lt_div_of_pos_right plus linarith on the rewritten expressions (1 + bound)/2.
why it matters
The lemma anchors numerical precision for all subsequent gap calculations inside the electron-mass necessity proofs and is invoked directly by gap_1332_bounds and log_phi_bounds in the same module. It propagates to GapProperties and MassToLight, supporting the claim that the electron mass is forced from the phi-ladder. This step closes part of the T9 necessity chain that begins from T8 and the self-similar fixed point at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.