Unique pairwise conflicts

Fix distinct i, j with an arc i → j. The certificate C_i fixes the gate coordinate q_{ij} = (j, γ(i,j)) to false, while C_j fixes the whole block B_j — in particular q_{ij} — to true. So q_{ij} is a conflicting literal, and Section 4 shows it is the only one.

Consequences proved here:

• conflict_gateCoord / exists_conflict_of_ne / eq_gateCoord_of_conflict / filter_conflict_eq_singleton — existence and uniqueness of the conflict;
• disjoint_cube_cert / sat_cert_unique — the subcubes C_i are pairwise disjoint, so every positive input has a unique owner;
• gateCoord_mem_violSet, eq_gateCoord_of_mem_violSet_of_fixed, one_le_dist_cert — the quantitative facts used in Section 11.2.

Note that the statement dist(C_i, C_j) = 1 of Section 4 refers to the distance between the two subcubes, i.e. to the projection of a point of C_i that is extremal for C_j; it is not true that every x ∈ C_i is at distance 1 from C_j (a point of C_i may violate many gate literals of C_j in third blocks, where C_i leaves the coordinate free). Accordingly we prove the two correct statements one_le_dist_cert and eq_gateCoord_of_mem_violSet_of_fixed.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem BSLambda.Construction.conflict_gateCoord {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hji : j ≠ i) (hij : Arc i j = true) : (cert Arc γ i).Conflict (cert Arc γ j) (gateCoord γ i j)

If i → j then q_{ij} = (j, γ(i,j)) is a conflicting literal between C_i and C_j (Section 4).

theorem BSLambda.Construction.exists_conflict_of_ne {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hij : i ≠ j) : ∃ (v : Coord ι r), (cert Arc γ i).Conflict (cert Arc γ j) v

Distinct certificates always conflict: at the gate coordinate of whichever of the two arcs joins i and j (Section 4).

theorem BSLambda.Construction.eq_gateCoord_of_conflict {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hji : j ≠ i) (hij : Arc i j = true) {v : Coord ι r} (h : (cert Arc γ i).Conflict (cert Arc γ j) v) : v = gateCoord γ i j

q_{ij} is the unique conflicting literal between C_i and C_j (Section 4).

theorem BSLambda.Construction.sat_cert_unique {ι : Type u_1} {r : ℕ} [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) {x : Input (Coord ι r)} (hi : (cert Arc γ i).Sat x) (hj : (cert Arc γ j).Sat x) : i = j

Every positive input lies in exactly one certificate subcube: the owner (Section 4).

theorem BSLambda.Construction.filter_conflict_eq_singleton {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hji : j ≠ i) (hij : Arc i j = true) : {v : Coord ι r | (cert Arc γ i).Conflict (cert Arc γ j) v} = {gateCoord γ i j}

The set of coordinates on which C_i and C_j conflict is the singleton {q_{ij}} (Section 4).

theorem BSLambda.Construction.disjoint_cube_cert {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hij : i ≠ j) : Disjoint (cert Arc γ i).cube (cert Arc γ j).cube

Distinct certificate subcubes are disjoint (Section 4).

theorem BSLambda.Construction.gateCoord_mem_violSet {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hji : j ≠ i) (hij : Arc i j = true) {x : Input (Coord ι r)} (hx : (cert Arc γ i).Sat x) : gateCoord γ i j ∈ (cert Arc γ j).violSet x

The unique conflict is always violated: q_{ij} ∈ violSet (C_j) x for x ∈ C_i (Section 4).

theorem BSLambda.Construction.eq_gateCoord_of_mem_violSet_of_fixed {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hji : j ≠ i) (hij : Arc i j = true) {x : Input (Coord ι r)} (hx : (cert Arc γ i).Sat x) {v : Coord ι r} (hv : v ∈ (cert Arc γ j).violSet x) (hfix : v ∈ (cert Arc γ i).fixedSet) : v = gateCoord γ i j

Any violated literal of C_j at a point of C_i that is also fixed by C_i must be the unique conflict q_{ij} (Section 4, used in Section 11.2).

theorem BSLambda.Construction.one_le_dist_cert {ι : Type u_1} {r : ℕ} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i j : ι} (hT : IsTournament Arc) (hij : i ≠ j) {x : Input (Coord ι r)} (hx : (cert Arc γ i).Sat x) : 1 ≤ (cert Arc γ j).dist x

A point of C_i is at distance at least 1 from C_j when i ≠ j; in particular C_i ∩ C_j = ∅ (Section 4).