gap upper checks 25 28

Proved

Freiman.gap_upper_checks_25_28

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

freimangaphall-ray

Exact upper-cylinder and cap contradiction leaf checks for rows 25–28, with no lower-row exclusions assumed.

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

theorem gap_upper_checks_25_28 : ∀ n : ℕ, 4 ≤ n → n < 8 → gapChecks [] [] (.upper (gapUpperRows[n]!).bound) (gapUpperTrees[n]!) := by
  sorry

end Freiman

Source

Freiman Hall ray report, certificates/gap/upper_table_partitions.json

View graph