Pith. sign in
module module moderate

IndisputableMonolith.Physics.ElectronMass.Necessity

show as:
view Lean formalization →

Numerical necessity layer for the electron-mass derivation: rigorous interval bounds on φ and on the exp/log comparisons that pin the electron rung and residue. Cited by T9 (electron mass), T10 (lepton ladder), and the mass-residue no-go. Argument is algebraic √5 bounds plus Taylor remainder control for exp at fixed rational points.

claimThe golden ratio $\varphi=(1+\sqrt{5})/2$ is confined to an explicit rational interval via $\sqrt{5}$ bounds, and the exponential/log inequalities needed for the electron mass residue (Taylor expansions of $\exp$ at the fixed rationals near $4.81211$ and $4.81212$, with controlled remainders) hold strictly.

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 break (T9): its rung and residue must be forced, not fitted. That forcing needs certified inequalities on $\varphi$ and on $\exp$ and $\log$ at a handful of rational sample points that appear in the residue arithmetic.

Upstream, PhiBounds supplies the strategy $2.236^2<5<2.237^2$ for algebraic enclosure of $\varphi$. Interval power machinery reduces $x^y$ to $\exp(y\log x)$. Alpha-side modules contribute the recognition-scale seed and interval bounds on $\alpha^{-1}$, which enter the electron residue bookkeeping but are not re-derived here. Electron-mass definitions and mass-topology fix the local vocabulary (rung, gap, residue band).

This module is the necessity bridge: it turns those enclosures into the concrete strict inequalities the electron-mass theorems invoke.

proof idea

Structure is a stack of certified numeric lemmas, not a single narrative proof.

  1. Bound $\varphi$ directly from rational squares bracketing $5$ (no floating-point axioms).
  2. Evaluate degree-10 Taylor sums for $\exp$ at the two rationals near $4.81211$ and $4.81212$; rewrite each partial sum and Lagrange-style remainder as exact rationals.
  3. Compare those rationals to the target thresholds to obtain strict $<$ or $>$ on the Taylor piece and on the error piece separately, then combine.
  4. Convert the exp comparisons into the matching $\log$ lower/upper numerical bounds used by the residue inequalities.

Each step is a short algebraic or interval lemma; the module exports the conjunction as the necessity package for T9.

why it matters in Recognition Science

T9 (electron mass) imports this module as the numeric spine of the first-break derivation: without certified $\varphi$ and exp/log bounds, the ledger-fraction residue stays conditional. Downstream, lepton-generation necessity (T10) reuses the same inequalities to force muon and tau from the electron anchor; the mass-residue no-go cites the geometric band value against literal SM RG integrals; neutrino, quark, and recognition-coupling modules inherit the electron-side constants and bounds when they extend the ladder. In the forcing chain this sits after T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$) and supplies the analytic inequalities that make the electron the parameter-free base of the mass tower.

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)