gap lower checks 7 11

Proved

Freiman.gap_lower_checks_7_11

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 7–11.

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

theorem gap_lower_checks_7_11 : ∀ n : ℕ, 5 ≤ n → n < 10 → gapChecks (gapLowerRows.take n) [] .forbidden (gapLowerTrees[n]!) := by
  sorry

end Freiman

Source

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

View graph