Disjoint signed pairs in actual circuit messages

A selected conjunction message can be true only if its two chosen primary literals are true. Disjoint original primary supports therefore supply disjoint signed pairs, even when the actual lines contain repeated or contradictory literals.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.exists_edge_of_selectedPair {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (selected : Aggregate.Geometry.SelectedPair line U) : ∃ (e : Entropy.SignedEdge ↥U), ↑e.left ∈ Aggregate.Geometry.primaryInputs line ∧ ↑e.right ∈ Aggregate.Geometry.primaryInputs line ∧ ∀ (x : ↥U → Bool), Aggregate.Geometry.lineSummary line U (Wire.elim (glue U x fun (x : ↥Uᶜ) => false) fun (x : Fin g) => false) = true → e.eval x = true

Two selected primary slots force a signed pair whenever the actual message is true.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.endpoint_injective_of_disjoint {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (S : Finset (Fin g)) (edge : ↥S → Entropy.SignedEdge ↥U) (left : ∀ (i : ↥S), ↑(edge i).left ∈ Aggregate.Geometry.primaryInputs (p.lines ↑i)) (right : ∀ (i : ↥S), ↑(edge i).right ∈ Aggregate.Geometry.primaryInputs (p.lines ↑i)) (disjoint : (↑S).Pairwise fun (i j : Fin g) => Disjoint (Aggregate.Geometry.primaryInputs (p.lines i)) (Aggregate.Geometry.primaryInputs (p.lines j))) : Function.Injective (endpoint edge)

Pairwise disjoint primary supports make all chosen endpoints distinct.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_le_retained_add_complement {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (S : Finset (Fin g)) (U : Finset (Fin n)) (disjoint : (↑S).Pairwise fun (i j : Fin g) => Disjoint (Aggregate.Geometry.primaryInputs (p.lines i)) (Aggregate.Geometry.primaryInputs (p.lines j))) : S.card ≤ {i ∈ S | Aggregate.Geometry.primaryInputs (p.lines i) ⊆ U}.card + Uᶜ.card

Giving coordinates to the receiver destroys at most one disjoint summary per coordinate.