Card (4,7,8) Fin560 w70h

Proved

ShaoThreeUnits.cover_row_4_7_8_fin560_w70h

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

additive-combinatoricsnumber-theory

Tag 478 window 490 <= n.val /\ n.val < 560. 728-habit fat 560. Not ABC. Not CoverProp. Not glue.

Preamble

import Mathlib
open Finset
open scoped Pointwise

Formal statement

namespace ShaoThreeUnits
theorem cover_row_4_7_8_fin560_w70h (n : Fin 560) (hn : 490 <= n.val /\ n.val < 560) : ((#[({ 1, 2, 4, 7 } : Finset (ZMod 15)), ({ 1, 2, 4, 8 } : Finset (ZMod 15)), ({ 1, 2, 4, 11 } : Finset (ZMod 15)), ({ 1, 2, 4, 13 } : Finset (ZMod 15)), ({ 1, 2, 4, 14 } : Finset (ZMod 15)), ({ 1, 2, 7, 8 } : Finset (ZMod 15)), ({ 1, 2, 7, 11 } : Finset (ZMod 15)), ({ 1, 2, 7, 13 } : Finset (ZMod 15)), ({ 1, 2, 7, 14 } : Finset (ZMod 15)), ({ 1, 2, 8, 11 } : Finset (ZMod 15)), ({ 1, 2, 8, 13 } : Finset (ZMod 15)), ({ 1, 2, 8, 14 } : Finset (ZMod 15)), ({ 1, 2, 11, 13 } : Finset (ZMod 15)), ({ 1, 2, 11, 14 } : Finset (ZMod 15)), ({ 1, 2, 13, 14 } : Finset (ZMod 15)), ({ 1, 4, 7, 8 } : Finset (ZMod 15)), ({ 1, 4, 7, 11 } : Finset (ZMod 15)), ({ 1, 4, 7, 13 } : Finset (ZMod 15)), ({ 1, 4, 7, 14 } : Finset (ZMod 15)), ({ 1, 4, 8, 11 } : Finset (ZMod 15)), ({ 1, 4, 8, 13 } : Finset (ZMod 15)), ({ 1, 4, 8, 14 } : Finset (ZMod 15)), ({ 1, 4, 11, 13 } : Finset (ZMod 15)), ({ 1, 4, 11, 14 } : Finset (ZMod 15)), ({ 1, 4, 13, 14 } : Finset (ZMod 15)), ({ 1, 7, 8, 11 } : Finset (ZMod 15)), ({ 1, 7, 8, 13 } : Finset (ZMod 15)), ({ 1, 7, 8, 14 } : Finset (ZMod 15)), ({ 1, 7, 11, 13 } : Finset (ZMod 15)), ({ 1, 7, 11, 14 } : Finset (ZMod 15)), ({ 1, 7, 13, 14 } : Finset (ZMod 15)), ({ 1, 8, 11, 13 } : Finset (ZMod 15)), ({ 1, 8, 11, 14 } : Finset (ZMod 15)), ({ 1, 8, 13, 14 } : Finset (ZMod 15)), ({ 1, 11, 13, 14 } : Finset (ZMod 15)), ({ 2, 4, 7, 8 } : Finset (ZMod 15)), ({ 2, 4, 7, 11 } : Finset (ZMod 15)), ({ 2, 4, 7, 13 } : Finset (ZMod 15)), ({ 2, 4, 7, 14 } : Finset (ZMod 15)), ({ 2, 4, 8, 11 } : Finset (ZMod 15)), ({ 2, 4, 8, 13 } : Finset (ZMod 15)), ({ 2, 4, 8, 14 } : Finset (ZMod 15)), ({ 2, 4, 11, 13 } : Finset (ZMod 15)), ({ 2, 4, 11, 14 } : Finset (ZMod 15)), ({ 2, 4, 13, 14 } : Finset (ZMod 15)), ({ 2, 7, 8, 11 } : Finset (ZMod 15)), ({ 2, 7, 8, 13 } : Finset (ZMod 15)), ({ 2, 7, 8, 14 } : Finset (ZMod 15)), ({ 2, 7, 11, 13 } : Finset (ZMod 15)), ({ 2, 7, 11, 14 } : Finset (ZMod 15)), ({ 2, 7, 13, 14 } : Finset (ZMod 15)), ({ 2, 8, 11, 13 } : Finset (ZMod 15)), ({ 2, 8, 11, 14 } : Finset (ZMod 15)), ({ 2, 8, 13, 14 } : Finset (ZMod 15)), ({ 2, 11, 13, 14 } : Finset (ZMod 15)), ({ 4, 7, 8, 11 } : Finset (ZMod 15)), ({ 4, 7, 8, 13 } : Finset (ZMod 15)), ({ 4, 7, 8, 14 } : Finset (ZMod 15)), ({ 4, 7, 11, 13 } : Finset (ZMod 15)), ({ 4, 7, 11, 14 } : Finset (ZMod 15)), ({ 4, 7, 13, 14 } : Finset (ZMod 15)), ({ 4, 8, 11, 13 } : Finset (ZMod 15)), ({ 4, 8, 11, 14 } : Finset (ZMod 15)), ({ 4, 8, 13, 14 } : Finset (ZMod 15)), ({ 4, 11, 13, 14 } : Finset (ZMod 15)), ({ 7, 8, 11, 13 } : Finset (ZMod 15)), ({ 7, 8, 11, 14 } : Finset (ZMod 15)), ({ 7, 8, 13, 14 } : Finset (ZMod 15)), ({ 7, 11, 13, 14 } : Finset (ZMod 15)), ({ 8, 11, 13, 14 } : Finset (ZMod 15))][n.val % 70]! + #[({ 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 / 70]! + ({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_4_7_8_fin560_w70h

View graph