gap_second_difference_neg

formal source

 261    simpa using h
 262  exact hfinal
 263
 264theorem gap_second_difference_neg (n : ℕ) :
 265    gap ((n + 2 : ℕ) : ℤ) + gap (n : ℤ) < 2 * gap ((n + 1 : ℕ) : ℤ) := by
 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) -/
 292lemma phi_bounds : (1.618033 : ℝ) < phi ∧ phi < (1.618034 : ℝ) := by
 293  -- φ = (1 + √5)/2
 294  -- We need: 2.236066 < √5 < 2.236068