middle compatible oscillation

Proved

Freiman.middle_compatible_oscillation

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionsformalizationlagrange-spectrum

Each exact cover endpoint is a compatible sum and every compatible central sum is within the sum of full cylinder widths of a target lying between those endpoints. This lemma uses the actual sSup-based cfValue via its prefix identity.

Preamble

import Definitions.Def_Freiman_middleRoots

Formal statement

namespace Freiman

theorem middle_compatible_oscillation :
    ∀ (c : MiddleCore) (a : ℤ→ℕ+) (t : ℝ), middleRegular c → middleCompatible c a → t∈middleCover c →
      |localValue a 0-t|  ≤  middleWidth c.left+middleWidth c.right := by
  sorry

end Freiman

Source

Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, Part III, active source staging/m2b/m2b_body.tex, m2b:prop:path, final oscillation estimate

View graph