Provedattentioninnovationexternal-review-3
Positive exponential secant: certified residual bound
For all , if and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- Δ, x range over real numbers: the statement must hold for every choice. (
(Δ x : ℝ)) - <Less than
- 0 is strictly smaller than Δ. (
0 < Δ) - −xNegation
- The negative of Δ. (
-Δ) - ≤At most
- −Δ is less than or equal to x. (
-Δ ≤ x) - ∧And
- Both hold: −Δ ≤ x, and x ≤ 0. (
-Δ ≤ x ∧ x ≤ 0) - eˣExponential function
- e raised to the power −Δ, where e ≈ 2.718. (
Real.exp (-Δ)) - +Addition
- 1 plus (1 − exp(−Δ))/Δ · x. (
1 + ((1 - Real.exp (-Δ)) / Δ) * x) - ·Multiplication
- (1 − exp(−Δ))/Δ times x. (
((1 - Real.exp (-Δ)) / Δ) * x) - a/bDivision
- 1 − exp(−Δ) divided by Δ. In Lean, dividing by 0 gives 0. (
(1 - Real.exp (-Δ)) / Δ) - -Subtraction
- 1 minus exp(−Δ). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - Real.exp (-Δ)) - aᵇPower
- Δ raised to the power 2. (
Δ ^ 2)
theorem innov-positive-exponential-secant (Δ x : ℝ) (hΔ : 0 < Δ) (hx : -Δ ≤ x ∧ x ≤ 0) :
Real.exp (-Δ) ≤ Real.exp x ∧ Real.exp x ≤ 1 + ((1 - Real.exp (-Δ)) / Δ) * x ∧ 1 + ((1 - Real.exp (-Δ)) / Δ) * x ≤ 1 ∧ 0 ≤ 1 + ((1 - Real.exp (-Δ)) / Δ) * x - Real.exp x ∧ 1 + ((1 - Real.exp (-Δ)) / Δ) * x - Real.exp x ≤ (x + Δ) * (-x) / 2 ∧ (x + Δ) * (-x) / 2 ≤ Δ ^ 2 / 8For positive interval width and x in [-width,0], proves exponential positivity via its endpoint, chord majorization, upper bound one, and residual bounded by the interpolation parabola and width squared over eight.
How it was proved
- Proved
- 6 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 51 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.