exp_46316_lower
plain-language theorem explainer
The inequality 102.67 < exp(4.6316) supplies a concrete numerical lower bound required to certify an upper limit on a negative power of the golden ratio inside the lepton mass predictions. Physicists checking the forced muon and tau masses under T10 would cite it when confirming consistency of the phi-ladder steps with the electron mass from T9. The proof factors the argument at 4 + 0.6316, applies separate exponential lower bounds, establishes the product inequality by positivity, and chains the comparison via transitivity.
Claim. $102.67 < e^{4.6316}$
background
Module T10 proves the lepton ladder is forced once the electron structural mass (T9) and the geometric constants (cube edges, faces, wallpaper groups, alpha, pi) are fixed. The phi-ladder supplies the rung spacings via the golden ratio and the eight-tick structure. This lemma is one of the numerical anchors that convert those geometric inputs into explicit bounds on the predicted muon and tau masses.
proof idea
The tactic proof splits the exponent via the addition formula, invokes the companion lemmas establishing 54.598150 < exp(4) and 1.8806 < exp(0.6316), uses nlinarith on the positivity of both exponentials to obtain the product lower bound, compares the numerical product against 102.67 by norm_num, and finishes with the transitivity lemma from ArithmeticFromLogic.
why it matters
The result feeds directly into the theorem phi_pow_neg9625_upper_v2 that bounds the golden-ratio term appearing in the higher-rung mass formula. It therefore helps discharge the original axioms for muon and tau masses in favor of derived inequalities, reinforcing the T10 claim that the entire lepton spectrum is fixed by the cube geometry and the phi fixed point. No open scaffolding remains at this numerical step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.