gap lower checks 12 16

Proved

Freiman.gap_lower_checks_12_16

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 12–16.

Preamble

import Definitions.Def_Freiman_gapCertificateData

Formal statement

namespace Freiman

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

end Freiman

Source

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

View graph