proof

Smoothing margin

Lean spine source

Declarations: margin_survives_distortion, margin_survives_distortion_positive

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem margin_survives_distortion
    {margin distortion est : Int}
    (h : 2 * distortion + 2 * est < margin) :
    0 < margin - 2 * distortion - 2 * est := by
  omega

theorem margin_survives_distortion_positive
    {margin distortion est : Int}
    (h : 2 * distortion + 2 * est < margin) :
    PositiveBoundaryMargin margin distortion est := by
  unfold PositiveBoundaryMargin; omega