proof

Smoothing margin

Lean spine source

formal/AlignmentProofSpine/Boundaries.lean

Declarations: margin_survives_distortion, margin_survives_distortion_positive

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). 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