Primary-support facts for retained conjunction classes

Selected literal variables count exactly the intersection of the original primary support with the cut. This relates the information classes to finite pair and triple witnesses in the actual circuit.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.card_literalVars_lineLiterals {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (conjunction : Aggregate.Geometry.Op.isConjunction line.op = true) (U : Finset (Fin n)) : (literalVars (lineLiterals line U)).card = (Aggregate.Geometry.primaryInputs line ∩ U).card

Selected conjunction variables count exactly the retained original primary support.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedTwo.selectedPair {n g : ℕ} {line : Line Aggregate.Geometry.signature n g} {U : Finset (Fin n)} (retained : RetainedTwo line U) : Aggregate.Geometry.SelectedPair line U

A retained exact-two conjunction has a selected primary pair.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedWide.selectedPair {n g : ℕ} {line : Line Aggregate.Geometry.signature n g} {U : Finset (Fin n)} (retained : RetainedWide line U) : Aggregate.Geometry.SelectedPair line U

A retained wide conjunction also has a selected primary pair.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedTwo.not_retainedWide {n g : ℕ} {line : Line Aggregate.Geometry.signature n g} {U : Finset (Fin n)} (retained : RetainedTwo line U) : ¬RetainedWide line U

An original exact-two line cannot simultaneously retain three inputs.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.disjoint_retained {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Disjoint (retainedTwo p U) (retainedWide p U)

The actual retained classes contain disjoint sets of gate indices.