Normalizing conjunctions with two primary variables

An inconsistent literal set computes false. Every consistent literal set on exactly two variables computes a signed edge, independently of literal order and of repetitions in the circuit that supplied the set.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.mem_literalVars {V : Type u_1} [DecidableEq V] {L : Finset (V × Bool)} {v : V} : v ∈ literalVars L ↔ ∃ (b : Bool), (v, b) ∈ L

Every variable in the literal set has a required Boolean value.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiterals_eq_false_of_not_consistent {V : Type u_1} {L : Finset (V × Bool)} (bad : ¬ConsistentLiterals L) : evalLiterals L = fun (x : V → Bool) => false

An inconsistent literal set has no satisfying assignment.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.exists_signedEdge_of_card_eq_two {V : Type u_1} [DecidableEq V] {L : Finset (V × Bool)} (consistent : ConsistentLiterals L) (two : (literalVars L).card = 2) : ∃ (e : Entropy.SignedEdge V), e.eval = evalLiterals L

A consistent conjunction on exactly two variables is a signed two-variable edge.