theorem
proved
term proof
gap_second_difference_neg
show as:
view Lean formalization →
formal statement (Lean)
264theorem gap_second_difference_neg (n : ℕ) :
265 gap ((n + 2 : ℕ) : ℤ) + gap (n : ℤ) < 2 * gap ((n + 1 : ℕ) : ℤ) := by
proof body
Term-mode proof.
266 have h := gap_diminishing_increments (n := n)
267 -- rearrange: g(n+2) - g(n+1) < g(n+1) - g(n) ↔ g(n+2) + g(n) < 2 g(n+1)
268 linarith
269
270end
271
272/-! ## Numerical interval bounds for canonical bands
273
274The following theorems establish verified numerical bounds for the `gap` function
275at the canonical Z-values (24, 276, 1332) used in the three fermion mass bands.
276
277These are structured as certified intervals matching the style in
278`Physics/ElectronMass/Necessity.lean`.
279-/
280
281section IntervalBounds
282
283/-! ### Foundational bounds on φ and log(φ)
284
285These numerical bounds are used to certify interval arithmetic for gap values.
286The bounds on φ come from √5 computation; bounds on log(φ) are represented as hypotheses
287as they require Taylor polynomial evaluation (see Physics/ElectronMass/Necessity.lean
288for the full proof machinery).
289-/
290
291/-- φ is bounded: φ ∈ (1.618033, 1.618034) -/