+# Signed conjunctions on two distinct variables

Each sign records the input value making its literal true. These edges describe the nonconstant two-variable primary-input summaries of conjunction gates.

structure Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge (V : Type u_1) : Type u_1

A conjunction of two signed literals on distinct primary coordinates.

• left : V

  First primary variable.

• right : V

  Second primary variable.

• distinct : self.left ≠ self.right
• leftSign : Bool

  Required value of the first variable.

• rightSign : Bool

  Required value of the second variable.

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.eval {V : Type u_1} (e : SignedEdge V) (x : V → Bool) : Bool

The conjunction is true precisely when both coordinates match their signs.

Equations

• e.eval x = (x e.left == e.leftSign && x e.right == e.rightSign)