Refined message bound for original narrow and wide conjunctions

The actual whole-program message pays the support-graph cost for retained original exact-two conjunctions, and the sharper one-eighth entropy cost for conjunctions retaining at least three primary inputs.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Joint.outputKeyRefinedWeightBound {n g : ℕ} (p : Program Aggregate.Geometry.signature n g) (U : Finset (Fin n)) (out : Wire n g) : Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.outputKey p U out (glue U x fun (x : ↥Uᶜ) => false)) ((↑g + 1) * Real.log 2 - ↑(retainedTwo p U).card * (Real.binEntropy (1 / 4) - 1 / 2 * Real.log 2) - ↑(retainedWide p U).card * (Real.log 2 - Real.binEntropy (1 / 8)) + ↑U.card * (Real.binEntropy (1 / 4) - 3 / 4 * Real.log 2))

The actual output message retains the separate narrow and wide information savings.

Equations

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