log_824_upper
plain-language theorem explainer
This inequality supplies an upper bound on the natural log of one plus 1332 over the golden-ratio approximation. Researchers deriving the forced electron mass on the phi-ladder cite it to close numerical gaps in the T9 necessity argument. The proof rewrites the log claim via log_lt_iff_lt_exp then chains an arithmetic bound on the argument to a split-exponential comparison.
Claim. $log(1 + 1332 / 1.618033) < 6.7145$
background
Module T9 proves the electron mass formula is forced from T8 ledger quantization together with geometric constants. The gap function returns the defect distance on the phi-ladder that sets mass rungs via yardstick times phi to a power. Upstream, one_plus_1332_div_phi_upper shows 1 + 1332/1.618033 < 824.2218 by nlinarith on the reciprocal inequality. val_824_lt_exp_67145 splits exp(6.7145) = exp(6) * exp(0.7145) to establish the target exponential exceeds 824.
proof idea
Apply Real.log_lt_iff_lt_exp after positivity to convert the claim into an exponential inequality. The calc tactic then inserts one_plus_1332_div_phi_upper to bound the argument below 824.2218 and val_824_lt_exp_67145 to finish the comparison with exp(6.7145).
why it matters
The result feeds gap_1332_bounds, which pins gap(1332) inside (13.953, 13.954) and thereby anchors the electron mass rung. It supplies a concrete numerical link from the abstract forcing chain (T5 J-uniqueness, T6 phi fixed point, T8 D=3) to the observed electron mass on the phi-ladder. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.