Anti-dominating pairs among balanced comparisons on four atoms

A comparison on four atoms is a sign vector v : Fin 4 → SignType, with positive side posSupport v and negative side negSupport v. Two comparisons are mergeable when no atom carries the same nonzero sign in both, and anti-dominating when the positive side of each lies in the negative side of the other. Every nonempty multiset of pairwise non-mergeable comparisons with nonempty positive sides that sums to zero contains an anti-dominating pair; this is the combinatorial core of cancellation on Fin 4.

Main declarations

• ComparativeProbability.Mergeable, ComparativeProbability.AntiDominating: the two relations between comparisons.
• ComparativeProbability.dotProduct_eq_zero_of_comparisonSum_eq_zero: an integer functional that is nonnegative on a multiset of comparisons summing to zero vanishes on it.
• ComparativeProbability.exists_antiDominating: the anti-domination theorem.

Implementation notes

Every case closes by a witness, an integer functional that is nonnegative on the family and positive on a member, which dotProduct_eq_zero_of_comparisonSum_eq_zero rules out; the cases read the family as the finset of its distinct members. A family of at most three members falls to the functional reading the signs that one member shares with the others. In a larger family, a member with a single positive coordinate k falls to e_k when it has full support; otherwise it has the shape +1 at p, 0 at ζ, -1 elsewhere, the functional e_p + e_ζ forces a second member of the same shape, and the next iterate closes a 3-cycle that e_p + e_i + e_ζ - e_j refutes. Once every member has two positive coordinates, 𝟙 forces each to have exactly two of each sign, and a pigeonhole on the three complementary pairs of 2-subsets of Fin 4 yields an anti-dominating pair.

def ComparativeProbability.Mergeable {W : Type u_1} (v w : W → SignType) : Prop

Two comparisons are mergeable when no atom carries the same nonzero sign in both.

Equations

• One or more equations did not get rendered due to their size.

theorem ComparativeProbability.Mergeable.symm {W : Type u_1} {v w : W → SignType} (h : Mergeable v w) : Mergeable w v

def ComparativeProbability.AntiDominating {W : Type u_1} (v w : W → SignType) : Prop

Two comparisons are anti-dominating when the positive side of each lies in the negative side of the other.

Equations

• One or more equations did not get rendered due to their size.

theorem ComparativeProbability.dotProduct_eq_zero_of_comparisonSum_eq_zero {W : Type u_1} [Fintype W] {M : Multiset (W → SignType)} (hM : comparisonSum M = 0) {u : W → ℤ} (hu : ∀ v ∈ M, 0 ≤ u ⬝ᵥ fun (i : W) => ↑(v i)) {v : W → SignType} (hv : v ∈ M) : (u ⬝ᵥ fun (i : W) => ↑(v i)) = 0

An integer functional that is nonnegative on a multiset of comparisons summing to zero vanishes on each of them.

At most three members

Members have at most one zero coordinate

The weight-3 singleton-positive kill

A singleton-positive weight-3 member x (one +1, one 0, two -1s) forces, via the functional e_p + e_ζ, 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 witness e_p + e_i + e_ζ - e_j is nonnegative on every admissible sign pattern and positive at x, contradicting balance.

Four or more members

theorem ComparativeProbability.exists_antiDominating {M : Multiset (Fin 4 → SignType)} (hM : comparisonSum M = 0) (hpos : ∀ v ∈ M, (posSupport v).Nonempty) (hmerge : ∀ v ∈ M, ∀ w ∈ M, v ≠ w → ¬Mergeable v w) (hne : M ≠ 0) : ∃ v ∈ M, ∃ w ∈ M, v ≠ w ∧ AntiDominating v w

Anti-domination from balance. A nonempty multiset of pairwise non-mergeable comparisons on four atoms, each with a nonempty positive side, that sums to zero contains an anti-dominating pair.