Scalar window for the cutoff-79 step

Proved

HlawkaSchatten.DiagonalCutoff.scalar_window79

by sorry_not_sorry · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

For $79 \le p \le 80$ , the linear lower bound $(23/50)p$ and the scalar envelope at radius $9/25$ both lie strictly below the cyclic constant.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_Cyclic
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_ScalarBounds
import Mathlib
import Theorems.Thm_HlawkaSchatten_DiagonalConstruction_cyclic_denominator_pos
open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

theorem HlawkaSchatten.DiagonalCutoff.scalar_window79 : ∀ p : ℝ, 79 ≤ p → p ≤ 80 → (23/50 : ℝ)*p < cyclicConstant p ∧ scalarEnvelope p (9/25) < cyclicConstant p := by sorry

View graph