gap upper checks 21 24

Proved

Freiman.gap_upper_checks_21_24

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

freimangaphall-ray

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

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

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

end Freiman

Source

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

View graph