+# Coordinate witnesses for the local conjunction cases

Two incident edges use at most three coordinates, and a chord with two parent edges uses at most four. These embeddings let finite truth-table certificates apply to arbitrary finite Boolean cubes.

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.reverse {V : Type u_1} (e : SignedEdge V) : SignedEdge V

Reverse an edge while retaining the same Boolean conjunction.

Equations

• e.reverse = { left := e.right, right := e.left, distinct := ⋯, leftSign := e.rightSign, rightSign := e.leftSign }

@[simp]

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.eval_reverse {V : Type u_1} (e : SignedEdge V) : e.reverse.eval = e.eval

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairCoordinates {V : Type u_1} (a b : V) (hab : a ≠ b) : Fin 2 ↪ V

Two distinct chosen coordinates.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairCoordinates a b hab = { toFun := ![a, b], inj' := ⋯ }

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tripleCoordinates {V : Type u_1} (a b c : V) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : Fin 3 ↪ V

Three distinct chosen coordinates.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.tripleCoordinates a b c hab hac hbc = { toFun := ![a, b, c], inj' := ⋯ }

def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.quadCoordinates {V : Type u_1} (a b c d : V) (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : Fin 4 ↪ V

Four distinct chosen coordinates.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Entropy.quadCoordinates a b c d hab hac had hbc hbd hcd = { toFun := ![a, b, c, d], inj' := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.withRightParent {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Fintype X] [Fintype Y] {key : X → Y} {parent : X → Z} {cost : ℝ} (bound : ConditionalWeightBound key parent cost) (extra : X → W) : ConditionalWeightBound key (fun (x : X) => (parent x, extra x)) cost

A conditional certificate may ignore an additional right-hand parent.

Equations

• bound.withRightParent extra = { weight := fun (z : Z × W) => bound.weight z.1, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.ConditionalWeightBound.withLeftParent {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [Fintype X] [Fintype Y] {key : X → Y} {parent : X → Z} {cost : ℝ} (bound : ConditionalWeightBound key parent cost) (extra : X → W) : ConditionalWeightBound key (fun (x : X) => (extra x, parent x)) cost

A conditional certificate may ignore an additional left-hand parent.

Equations

• bound.withLeftParent extra = { weight := fun (z : W × Z) => bound.weight z.2, nonneg := ⋯, mass := ⋯, positive := ⋯, log_bound := ⋯ }