log_upper_numerical
plain-language theorem explainer
This theorem establishes that the natural logarithm of 1.618034 is strictly less than 0.481212. It supplies the upper half of the numerical sandwich used to bound log phi in the electron mass necessity arguments. The proof rewrites the log inequality via the exponential comparison, invokes a tenth-order Taylor bound with explicit remainder, and closes the chain by linear arithmetic on the rational approximations.
Claim. $log(1.618034) < 0.481212$
background
The module derives the electron mass formula as forced from T8 ledger quantization together with the geometric constants obtained earlier in the chain. The golden ratio phi appears as the self-similar fixed point (T6) and satisfies phi ≈ 1.618034; its logarithm must therefore lie inside a narrow numerical interval to match the observed alpha band. Upstream results supply the tenth-order Taylor polynomial for exp at 0.481212 together with its explicit error term, the arithmetic successor operation, and the lower-bounding trigonometric polynomial used in related interval arithmetic.
proof idea
Rewrite the target via log x < y iff x < exp y. Apply the exponential bound lemma for |x| ≤ 1 and n = 10 to obtain the absolute-error estimate. Equate the partial sum to the named rational exp_taylor_10_at_481212 and the remainder to exp_error_10_at_481212. Use the cast of the sibling inequality exp_taylor_481212_gt_target to place 1.618034 strictly below the lower envelope of the exponential; finish with linarith on the rearranged error inequality.
why it matters
The declaration is the upper half of the sandwich lemma log_phi_bounds that pins 0.481211 < log phi < 0.481212. That lemma is invoked inside the T9 necessity proof that the electron mass is forced once the phi-ladder and alpha derivation are in place. It therefore closes a concrete numerical verification step between the J-uniqueness fixed point (T5) and the eight-tick octave (T7) that yields D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.