Edge-insertion assembly of local conditional weights #
The induction uses the exact number of new endpoints. An edge with no new endpoint uses two earlier incident edges, an edge with one new endpoint uses one, and an edge with two new endpoints uses its unconditional weight.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.exists_weightBound_tuple_of_local
{V : Type u_1}
{E : Type u_2}
[Fintype V]
[DecidableEq V]
[DecidableEq E]
(seed : (e : SignedEdge V) → WeightBound e.eval (Real.binEntropy (1 / 4)))
(one :
(e f : SignedEdge V) →
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))
(two :
(e f g : SignedEdge V) →
e.left = f.left ∨ e.left = f.right →
e.right = g.left ∨ e.right = g.right →
ConditionalWeightBound e.eval (fun (x : V → Bool) => (f.eval x, g.eval x)) edgeCost)
(edge : E → SignedEdge V)
(selected : Finset E)
:
Local zero-, one-, and two-parent kernels assemble into a joint edge-message weight.