Balanced sign-vector families on Fin 4 have an anti-dominating pair

The finite combinatorial core of the Fin 4 cancellation theorem.

Main declarations

• SignVec.posSupport, SignVec.negSupport — positive and negative supports of a {-1,0,1}-valued vector on four coordinates (the sign values and the arity are deliberately hardcoded: the pigeonhole and decide steps below are irreducibly Fin 4-specific).
• SignVec.exists_antidom_pair — any family of sign vectors, each with a positive coordinate, balanced by strictly positive weights, of size at most 5, and pairwise non-generalized-mergeable (every pair shares a same-sign coordinate), contains an anti-dominating pair: two members whose positive supports sit inside each other's negative supports.

Implementation notes

Sizes 1–3 fall to coefficient arithmetic. For sizes 4–5: full-support families are forced into 2-element positive supports by the 𝟙-functional and die by a pigeonhole on the three complementary pairs of 2-subsets; families with a zero coordinate die through the s-shape chain — a singleton-positive weight-3 member forces a cascade closing into a 3-cycle whose Stiemke witness is nonnegative on every admissible sign pattern and positive somewhere, contradicting balance.

The recurring hypothesis bundle (sign-valued, positive coordinate, no g-merge, positively weighted balance) is threaded flat rather than packaged in a structure: every consumer below exists_antidom_pair is private, and the theorem has a single external caller.

def SignVec.posSupport (v : Fin 4 → ℚ) : Finset (Fin 4)

Equations

• SignVec.posSupport v = {i : Fin 4 | v i = 1}

def SignVec.negSupport (v : Fin 4 → ℚ) : Finset (Fin 4)

Equations

• SignVec.negSupport v = {i : Fin 4 | v i = -1}

@[simp]

theorem SignVec.mem_posSupport {v : Fin 4 → ℚ} {i : Fin 4} : i ∈ posSupport v ↔ v i = 1

@[simp]

theorem SignVec.mem_negSupport {v : Fin 4 → ℚ} {i : Fin 4} : i ∈ negSupport v ↔ v i = -1

Phase 1: balance and the both-signs corollary

Sizes 1 and 2 are impossible

Weight-4 dichotomy, sharing, and the size-3 case

A1: members have at most one zero coordinate (weight ≥ 3)

The weight-3 singleton-positive kill

A singleton-positive weight-3 member x (one +1, one 0, two -1s) forces, via the functional w ↦ w p + w ζ, an s-shape companion y₁ (zero at x's positive coordinate, -1 at x's zero); y₁ is again singleton-positive weight-3, so the forcing iterates. Pairwise admissibility kills one branch of the second iterate, pinning the 3-cycle x, y₁, y₂, whose Stiemke witness w ↦ w p + w i + w ζ - w j is nonnegative on every admissible sign pattern and positive at x — contradicting balance.

Sizes 4 and 5

theorem SignVec.exists_antidom_pair (S : Finset (Fin 4 → ℚ)) (d : (Fin 4 → ℚ) → ℚ) (hd : ∀ v ∈ S, 0 < d v) (hsign : ∀ v ∈ S, ∀ (i : Fin 4), v i = -1 ∨ v i = 0 ∨ v i = 1) (hposne : ∀ v ∈ S, ∃ (i : Fin 4), v i = 1) (hnogm : ∀ v ∈ S, ∀ w ∈ S, v ≠ w → ¬(Disjoint (posSupport v) (posSupport w) ∧ Disjoint (negSupport v) (negSupport w))) (hsum : ∑ v ∈ S, d v • v = 0) (hSne : S.Nonempty) (hcard : S.card ≤ 5) : ∃ v ∈ S, ∃ w ∈ S, v ≠ w ∧ posSupport v ⊆ negSupport w ∧ posSupport w ⊆ negSupport v

Anti-domination from balance: a balanced family of at most five pairwise non-generalized-mergeable sign vectors contains an anti-dominating pair.