pith. sign in
module module high

IndisputableMonolith.Physics.ElectronMass.Necessity

show as:
view Lean formalization →

This module proves that φ is bounded using direct √5 comparisons in the context of electron mass necessity. It supplies the interval arithmetic required by the T9 electron mass derivation and the T10 lepton ladder proofs. The argument relies on algebraic bounds propagated from √5 inequalities without external hypotheses.

claim$2.236^2 < 5 < 2.237^2$ implies tight interval bounds on φ = (1 + √5)/2 that close the electron mass residue calculation.

background

The module sits inside the electron mass necessity layer and imports the RS time quantum τ₀ = 1 tick together with the alpha derivation from the cubic ledger geometry. It draws on the PhiBounds strategy that starts from the algebraic fact 2.236² = 4.999696 < 5 < 5.001956 = 2.237² and on the Pow module for rigorous interval arithmetic on x^y = exp(y log x). These bounds are required to close the ledger-fraction step in the T9 mass formula.

proof idea

The module assembles a collection of lemmas that first fix √5 bounds, then apply Taylor expansions of exp at the points 481211 and 481212 together with error-term comparisons to obtain matching rational bounds on log and exp. These combine into the final phi interval via direct algebraic reduction; no external theorem beyond the imported interval primitives is invoked.

why it matters in Recognition Science

The bounds close the numerical gap in the ElectronMass module (T9) and are imported by LeptonGenerations.Necessity (T10), MassResidueNoGo, NeutrinoSector, QuarkMasses and RecognitionCoupling. They thereby convert the structural mass formula into a fully rigorous, parameter-free statement inside the Recognition Science chain.

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)