The joint weight bound for signed two-variable conjunctions

An edge contributes its two-literal conjunction to the message. The entropy bound charges each edge and each used primary coordinate, allowing arbitrary parallel edges and signs and making no graph acyclicity assumption.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.edgeCost : ℝ

The natural-log cost charged to each edge in the joint message.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.edgeCost = 3 / 2 * Real.log 2 - Real.binEntropy (1 / 4)

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.vertexCost : ℝ

The natural-log cost charged to each primary variable used by the message.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.vertexCost = Real.binEntropy (1 / 4) - 3 / 4 * Real.log 2

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.tuple {V : Type u_1} {E : Type u_2} (edge : E → SignedEdge V) (selected : Finset E) (x : V → Bool) : ↥selected → Bool

The message consisting of the conjunction values of selected edges.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.tuple edge selected x e = (edge ↑e).eval x