A six-column three-group census

This file isolates the small arithmetic obstruction used at the order-15 endpoint of the shared-star moat. Each column records how many of its three incidences land in three two-vertex groups. If too few pairs are repeated inside the groups and across the first group, the six columns cannot exist.

theorem ACMax.six_triple_census_impossible {α : Type u_1} (B : Finset α) (a c d : α → ℕ) (hB : B.card = 6) (hcol : ∀ x ∈ B, a x ≤ 2 ∧ c x ≤ 2 ∧ d x ≤ 2 ∧ a x + c x + d x = 3) (ha : ∑ x ∈ B, a x = 6) (hwithin : ∑ x ∈ B, (((if a x = 2 then 1 else 0) + if c x = 2 then 1 else 0) + if d x = 2 then 1 else 0) ≤ 3) (hac : ∑ x ∈ B, a x * c x ≤ 4) (had : ∑ x ∈ B, a x * d x ≤ 4) : False

Six triples with entries at most two and column sum three cannot have first-coordinate sum six while all three indicated pair counts stay small.

The three indicator sums count repeated pairs within the groups. The product sums count pairs crossing the first group with the other two groups.

theorem ACMax.six_binary_columns_force_repeated_pair {α : Type u_1} (B : Finset α) (a₁ a₂ c₁ c₂ d₁ d₂ : α → Prop) (hB : B.card = 6) (hcol : ∀ x ∈ B, ((((((if a₁ x then 1 else 0) + if a₂ x then 1 else 0) + if c₁ x then 1 else 0) + if c₂ x then 1 else 0) + if d₁ x then 1 else 0) + if d₂ x then 1 else 0) = 3) (ha₁ : (Finset.filter a₁ B).card = 3) (ha₂ : (Finset.filter a₂ B).card = 3) : 2 ≤ {x ∈ B | a₁ x ∧ a₂ x}.card ∨ 2 ≤ {x ∈ B | c₁ x ∧ c₂ x}.card ∨ 2 ≤ {x ∈ B | d₁ x ∧ d₂ x}.card ∨ 2 ≤ {x ∈ B | a₁ x ∧ c₁ x}.card ∨ 2 ≤ {x ∈ B | a₁ x ∧ c₂ x}.card ∨ 2 ≤ {x ∈ B | a₂ x ∧ c₁ x}.card ∨ 2 ≤ {x ∈ B | a₂ x ∧ c₂ x}.card ∨ 2 ≤ {x ∈ B | a₁ x ∧ d₁ x}.card ∨ 2 ≤ {x ∈ B | a₁ x ∧ d₂ x}.card ∨ 2 ≤ {x ∈ B | a₂ x ∧ d₁ x}.card ∨ 2 ≤ {x ∈ B | a₂ x ∧ d₂ x}.card

Binary incidence form of six_triple_census_impossible. Six three-incidence columns on three pairs of rows force a repeated pair either within one row-pair, or between the first row-pair and one of the other two.