gap upper checks 29 31

Proved

Freiman.gap_upper_checks_29_31

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

freimangaphall-ray

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

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

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

end Freiman

Source

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

View graph