pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Physics.ElectronMass.Necessity

show as:
view Lean formalization →

This module proves that the golden ratio φ is bounded using direct algebraic comparisons of √5 squares. It supplies the numerical foundation required for the electron mass derivation within the Recognition Science phi-ladder. Researchers deriving lepton masses from T9 would cite these bounds to anchor the geometric mass formula. The argument proceeds by importing interval bounds on φ and combining them with Taylor expansions for exponential error control at fixed points.

claimThe golden ratio satisfies $1.6180339887 < (1 + 5^{1/2})/2 < 1.6180339888$, established directly from the inequalities $2.236^2 < 5 < 2.237^2$.

background

Recognition Science derives all constants from the J-cost functional J(x) = (x + x^{-1})/2 - 1 and the self-similar fixed point φ forced at T6. The phi-ladder then supplies mass values via yardstick · φ^(rung - 8 + gap(Z)). This module imports PhiBounds, which establishes the √5 interval 2.236² = 4.999696 < 5 < 5.001956 = 2.237², together with AlphaBounds and Pow for interval arithmetic on exp and log. It sits inside the T9 electron-mass block and supplies the concrete numerical anchors needed before the mass residue can be compared with the geometric band.

proof idea

The module is organized as a collection of interval lemmas. phi_bounds applies the algebraic √5 comparison from the imported PhiBounds module. Subsequent definitions (exp_taylor_10_at_481211, exp_error_10_at_481211, taylor_sum_eq_rational, log_lower_numerical, etc.) use the Pow interval arithmetic to bound the Taylor remainder for exp at the specific points required by the electron-mass necessity calculation. The overall structure is a direct algebraic reduction followed by verified numerical inequalities; no external axioms beyond the imported bounds are introduced.

why it matters in Recognition Science

The module feeds the T9 electron-mass derivation in IndisputableMonolith.Physics.ElectronMass and the necessity proofs for the lepton ladder in LeptonGenerations.Necessity. It also supplies the numerical closure required by MassResidueNoGo and the downstream quark and neutrino sectors. By discharging the concrete φ-bound hypothesis that appears in the T5–T8 forcing chain, it removes one layer of scaffolding between the abstract Recognition Composition Law and the first observable mass scale.

scope and limits

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.

declarations in this module (45)