Card (7,5,8) Fin448 w56g

Proved

ShaoThreeUnits.cover_row_7_5_8_fin448_w56g

by hitme development · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsnumber-theory

Tag 758 window 336 <= n.val /\ n.val < 392. 728-habit fat. Not ABC. Not CoverProp. Not glue.

Preamble

import Mathlib
open Finset
open scoped Pointwise

Formal statement

namespace ShaoThreeUnits
theorem cover_row_7_5_8_fin448_w56g (n : Fin 448) (hn : 336 <= n.val /\ n.val < 392) : ((#[({ 1, 2, 4, 7, 8, 11, 13 } : Finset (ZMod 15)), ({ 1, 2, 4, 7, 8, 11, 14 } : Finset (ZMod 15)), ({ 1, 2, 4, 7, 8, 13, 14 } : Finset (ZMod 15)), ({ 1, 2, 4, 7, 11, 13, 14 } : Finset (ZMod 15)), ({ 1, 2, 4, 8, 11, 13, 14 } : Finset (ZMod 15)), ({ 1, 2, 7, 8, 11, 13, 14 } : Finset (ZMod 15)), ({ 1, 4, 7, 8, 11, 13, 14 } : Finset (ZMod 15)), ({ 2, 4, 7, 8, 11, 13, 14 } : Finset (ZMod 15))][n.val / 56]! + #[({ 1, 2, 4 } : Finset (ZMod 15)), ({ 1, 2, 7 } : Finset (ZMod 15)), ({ 1, 2, 8 } : Finset (ZMod 15)), ({ 1, 2, 11 } : Finset (ZMod 15)), ({ 1, 2, 13 } : Finset (ZMod 15)), ({ 1, 2, 14 } : Finset (ZMod 15)), ({ 1, 4, 7 } : Finset (ZMod 15)), ({ 1, 4, 8 } : Finset (ZMod 15)), ({ 1, 4, 11 } : Finset (ZMod 15)), ({ 1, 4, 13 } : Finset (ZMod 15)), ({ 1, 4, 14 } : Finset (ZMod 15)), ({ 1, 7, 8 } : Finset (ZMod 15)), ({ 1, 7, 11 } : Finset (ZMod 15)), ({ 1, 7, 13 } : Finset (ZMod 15)), ({ 1, 7, 14 } : Finset (ZMod 15)), ({ 1, 8, 11 } : Finset (ZMod 15)), ({ 1, 8, 13 } : Finset (ZMod 15)), ({ 1, 8, 14 } : Finset (ZMod 15)), ({ 1, 11, 13 } : Finset (ZMod 15)), ({ 1, 11, 14 } : Finset (ZMod 15)), ({ 1, 13, 14 } : Finset (ZMod 15)), ({ 2, 4, 7 } : Finset (ZMod 15)), ({ 2, 4, 8 } : Finset (ZMod 15)), ({ 2, 4, 11 } : Finset (ZMod 15)), ({ 2, 4, 13 } : Finset (ZMod 15)), ({ 2, 4, 14 } : Finset (ZMod 15)), ({ 2, 7, 8 } : Finset (ZMod 15)), ({ 2, 7, 11 } : Finset (ZMod 15)), ({ 2, 7, 13 } : Finset (ZMod 15)), ({ 2, 7, 14 } : Finset (ZMod 15)), ({ 2, 8, 11 } : Finset (ZMod 15)), ({ 2, 8, 13 } : Finset (ZMod 15)), ({ 2, 8, 14 } : Finset (ZMod 15)), ({ 2, 11, 13 } : Finset (ZMod 15)), ({ 2, 11, 14 } : Finset (ZMod 15)), ({ 2, 13, 14 } : Finset (ZMod 15)), ({ 4, 7, 8 } : Finset (ZMod 15)), ({ 4, 7, 11 } : Finset (ZMod 15)), ({ 4, 7, 13 } : Finset (ZMod 15)), ({ 4, 7, 14 } : Finset (ZMod 15)), ({ 4, 8, 11 } : Finset (ZMod 15)), ({ 4, 8, 13 } : Finset (ZMod 15)), ({ 4, 8, 14 } : Finset (ZMod 15)), ({ 4, 11, 13 } : Finset (ZMod 15)), ({ 4, 11, 14 } : Finset (ZMod 15)), ({ 4, 13, 14 } : Finset (ZMod 15)), ({ 7, 8, 11 } : Finset (ZMod 15)), ({ 7, 8, 13 } : Finset (ZMod 15)), ({ 7, 8, 14 } : Finset (ZMod 15)), ({ 7, 11, 13 } : Finset (ZMod 15)), ({ 7, 11, 14 } : Finset (ZMod 15)), ({ 7, 13, 14 } : Finset (ZMod 15)), ({ 8, 11, 13 } : Finset (ZMod 15)), ({ 8, 11, 14 } : Finset (ZMod 15)), ({ 8, 13, 14 } : Finset (ZMod 15)), ({ 11, 13, 14 } : Finset (ZMod 15))][n.val % 56]! + ({1, 2, 4, 7, 8, 11, 13, 14} : Finset (ZMod 15)) : Finset (ZMod 15)) = univ) := by sorry
end ShaoThreeUnits

Source

Shao arXiv:1206.6139 Lemma 2.3 cover_row_7_5_8_fin448_w56g

View graph