exp_sub_trunc6_le
plain-language theorem explainer
The theorem supplies a concrete remainder bound for the real exponential Taylor series truncated after the fifth-order term. Effective-field theorists matching Recognition cost geometry to the Standard Model Higgs potential cite it to control O(h^6) errors in the quartic approximation. The proof is a one-line wrapper that lifts the real expression to ℂ, equates the remainders, and invokes the Mathlib complex norm lemma Complex.norm_exp_sub_sum_le_norm_mul_exp.
Claim. For every real number $t$, $|e^t - (1 + t + t^2/2 + t^3/6 + t^4/24 + t^5/120)| ≤ e^{|t|} |t|^6$.
background
The Higgs EFT Bridge module defines the recognition-cost potential as $V_{RS}(Λ,v,h) = Λ^4 · J(exp(h/v))$ with $J(x) = ½(x + x^{-1}) - 1$, which equals cosh(ε) - 1 for the dimensionless coordinate ε = h/v. This truncation bound is required to extract the quadratic and quartic coefficients that match onto the Standard-Model form ½ m_H² h² + (λ_SM/4) h⁴. The local setting is the first two arrows of the RS-to-SM dictionary: m_H² = Λ⁴/v² and λ_SM = Λ⁴/(6 v⁴). The result rests on the complex-analysis remainder lemma Complex.norm_exp_sub_sum_le_norm_mul_exp supplied by Mathlib.
proof idea
The tactic proof first calls Complex.norm_exp_sub_sum_le_norm_mul_exp (t : ℂ) 6. It then proves the auxiliary equality hexpr that identifies the real remainder with the complex one after casting to ℂ. Rewriting via Complex.norm_real and Real.norm_eq_abs converts the complex norm into the absolute-value expression on the left-hand side. The final simpa step rearranges the right-hand side using mul_comm, mul_left_comm and mul_assoc to obtain the stated real bound.
why it matters
The bound is invoked inside cosh_quartic_error to produce the quartic-error estimate |cosh ε - 1 - ε²/2 - ε⁴/24| ≤ exp|ε| · |ε|^6 on |ε| ≤ 1/2. That error control closes the Taylor-coefficient extraction step in the Higgs EFT bridge, allowing the RS cost geometry to determine the SM mass and quartic coupling without additional free parameters. Within the Recognition framework it supports the vacuum expansion of J(exp ε) that yields the canonical Higgs potential while keeping the eight-tick octave and phi-ladder structure intact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.