gap lower checks 17 20

Proved

Freiman.gap_lower_checks_17_20

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

freimangaphall-ray

Exact rational leaf inequalities and strictly earlier forbidden-row references for lower rows 17–20.

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

theorem gap_lower_checks_17_20 : ∀ n : ℕ, 15 ≤ n → n < 19 → gapChecks (gapLowerRows.take n) [] .forbidden (gapLowerTrees[n]!) := by
  sorry

end Freiman

Source

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

View graph