Conditional weights for incident signed conjunctions

The finite two-, three-, and four-variable cases cover every overlap pattern of an edge with one or two earlier incident edges. Coordinate embeddings transport their certificates to arbitrary Boolean cubes. These local bounds make no independence assumption about the remaining circuit messages.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.weightBound {V : Type u_1} [Fintype V] [DecidableEq V] (e : SignedEdge V) : WeightBound e.eval (Real.binEntropy (1 / 4))

A two-literal conjunction costs at most the entropy of a quarter-biased bit.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.conditionalParallel {V : Type u_1} [Fintype V] [DecidableEq V] (e f : SignedEdge V) (left : e.left = f.left) (right : e.right = f.right) : ConditionalWeightBound e.eval f.eval (3 / 2 * Real.log 2 - Real.binEntropy (1 / 4))

A parent on the same two coordinates gives the chord cost, for every choice of signs.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.conditionalSharedLeft {V : Type u_1} [Fintype V] [DecidableEq V] (e f : SignedEdge V) (left : e.left = f.left) : ConditionalWeightBound e.eval f.eval (3 / 4 * Real.log 2)

Edges sharing their left endpoint admit a three-quarter-bit conditional certificate.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.conditionalOne {V : Type u_1} [Fintype V] [DecidableEq V] (e f : SignedEdge V) (overlap : e.left = f.left ∨ e.left = f.right ∨ e.right = f.left ∨ e.right = f.right) : ConditionalWeightBound e.eval f.eval (3 / 4 * Real.log 2)

Any earlier incident edge lowers the conditional cost to at most three quarters of a bit.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.conditionalTwoLeft {V : Type u_1} [Fintype V] [DecidableEq V] (e f g : SignedEdge V) (left : e.left = f.left) (right : e.right = g.left) : ConditionalWeightBound e.eval (fun (x : V → Bool) => (f.eval x, g.eval x)) (3 / 2 * Real.log 2 - Real.binEntropy (1 / 4))

Parents oriented toward the target endpoints supply the remaining-edge certificate.

Equations

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

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.conditionalTwo {V : Type u_1} [Fintype V] [DecidableEq V] (e f g : SignedEdge V) (left : e.left = f.left ∨ e.left = f.right) (right : e.right = g.left ∨ e.right = g.right) : ConditionalWeightBound e.eval (fun (x : V → Bool) => (f.eval x, g.eval x)) (3 / 2 * Real.log 2 - Real.binEntropy (1 / 4))

Earlier incident edges at both endpoints give the chord cost, including parallel edges.

Equations

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