Pith. sign in
module module moderate

IndisputableMonolith.Physics.ElectronMass.Necessity

show as:
view Lean formalization →

Certified numerical bounds on the golden ratio and on exp/log at the electron-mass anchor points. Physicists citing T9 (electron mass) or T10 (lepton ladder necessity) use these inequalities to close residue comparisons without floating-point trust. The module chains algebraic √5 bounds with degree-10 Taylor remainders and rational target comparisons.

claimA suite of rigorous inequalities: bounds on $\varphi=(1+\sqrt{5})/2$ from $\sqrt{5}$ sandwiches; Taylor expansions of $\exp$ at the anchors $\approx 4.81211$ and $\approx 4.81212$ with explicit remainder control; and matching lower/upper bounds on $\log$ that force the electron-mass residue comparisons used downstream.

background

Recognition Science places particle masses on a $\varphi$-ladder: mass equals a yardstick times $\varphi$ raised to a rung offset by a geometric gap. The electron is the first charged rung (T9). Closing that derivation needs certified comparisons of transcendental expressions against rational targets, not machine floats.

This module sits under Physics.ElectronMass and imports interval infrastructure for $\varphi$, $\alpha^{-1}$, and $x^y=\exp(y\log x)$, plus the electron-mass definitions and mass-topology scaffolding. Upstream PhiBounds records the strategy $2.236^2<5<2.237^2$; Pow supplies the exp-log power identity used when ladder exponents appear.

Sibling lemmas named in the module (phi bounds, degree-10 Taylor sums and errors at the 4.81211/4.81212 anchors, rational equalities for sum and remainder, and numerical log lower/upper bounds) are the concrete certificates those comparisons rest on.

proof idea

Argument structure is numerical certification, not a single theorem.

  1. Bound $\varphi$ algebraically from tight rational squares around $\sqrt{5}$ (direct, as the module note states).
  2. Expand $\exp$ to order 10 at the two anchor abscissae near 4.81211 and 4.81212; identify the partial sum and Lagrange-style remainder with explicit rationals.
  3. Prove the Taylor sum lies below (or the combined sum-plus-error lies below) a fixed rational target, and the companion expansion lies above its target.
  4. Convert those exp inequalities into matching numerical lower and upper bounds on $\log$ at the dual points needed by the electron residue arithmetic.

No single wrapper: each lemma is a short interval or rational comparison discharging one side of a sandwich.

why it matters in Recognition Science

T9 (electron mass) imports this module to replace floating checks with Lean-checked inequalities in the ledger-fraction residue. Downstream, LeptonGenerations.Necessity (T10) uses the same certificates to force muon and tau masses from the electron anchor and geometric constants, aiming to retire axioms in the lepton ladder.

Further consumers: MassResidueNoGo (literal SM RG residue cannot hit the geometric band), NeutrinoSector (deep-ladder scale), QuarkMasses (quarter-ladder numerics), RecognitionCoupling (geometric vs perturbative residue gap), and Verification.LeptonCoefficientPerturbation. Without these bounds, the mass-ladder necessity claims stay conditional on external numerics. Landmarks touched: $\varphi$ from T6, the mass formula on the $\varphi$-ladder, and the electron as the first break after the eight-tick and $D=3$ forcing chain.

scope and limits

used by (7)

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)