Card (8,4,7) Fin560 w70c

Proved

ShaoThreeUnits.cover_row_8_4_7_fin560_w70c

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

additive-combinatoricsnumber-theory

Tag 847 window 140 <= n.val /\ n.val < 210. 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_8_4_7_fin560_w70c (n : Fin 560) (hn : 140 <= n.val /\ n.val < 210) : ((({1, 2, 4, 7, 8, 11, 13, 14} : Finset (ZMod 15)) + #[({ 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]! : Finset (ZMod 15)) = univ) := by sorry
end ShaoThreeUnits

Source

Shao arXiv:1206.6139 Lemma 2.3 cover_row_8_4_7_fin560_w70c

View graph