Retained original conjunction classes

Exact-two gates keep their original two primary inputs in the selected cut. Wider gates retain at least three primary inputs. These classes are disjoint, and the definitions refer to actual lines and their literal-set messages.

def Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedTwo {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Prop

An original exact-two conjunction retains both primary inputs in the cut.

Equations

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

def Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedWide {n g : ℕ} (line : Line Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Prop

A conjunction retains at least three distinct primary inputs in the cut.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.retainedTwo {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Finset (Fin g)

Actual original exact-two gates retained by the selected cut.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.retainedTwo p U = {i : Fin g | Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedTwo (p.lines i) U}

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.retainedWide {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) : Finset (Fin g)

Actual gates retaining at least three primary inputs in the selected cut.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.retainedWide p U = {i : Fin g | Algebraic.Cutwidth.Aggregate.Geometry.Joint.RetainedWide (p.lines i) U}