exp_18093_lower
plain-language theorem explainer
A numerical lemma establishes that exp(1.8093) strictly exceeds 6.105. Researchers deriving lepton generation masses from the phi-ladder cite this bound to close residue calculations in the T10 necessity proofs. The tactic proof factors the argument additively, invokes separate lower bounds on each exponential factor, and chains the product inequality via linear arithmetic.
Claim. $exp(1.8093) > 6.105$ holds.
background
The T10 module proves the muon and tau masses are forced from the electron structural mass (T9), step functions from cube geometry and alpha, and the golden ratio fixed point (T4). The lepton ladder uses E_passive = 11, faces = 6, W = 17, alpha in (137.030, 137.039), and pi from spherical geometry, all derived from the eight-tick structure. This lemma supplies a concrete exponential anchor at the 1.8093 residue endpoint.
proof idea
The proof rewrites 1.8093 as 1 + 0.8093 and applies the exponential addition formula. It invokes the library lower bound exp(1) > 2.7182818283 together with the sibling lemma giving exp(0.8093) > 2.2463. Linear arithmetic confirms the product exceeds 6.105, after which transitivity closes the result.
why it matters
The bound feeds the upper estimate on goldenRatio to the power -3.76, which supports the necessity theorems for distinct lepton rungs and torsion minimality in the same module. It closes a numerical step in the chain from T7 (eight-tick octave) and T8 (D = 3) through the Recognition Composition Law to the predicted lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.