Refined information weights for the actual circuit message #
Disjoint original conjunction classes receive their separate graph and one-eighth costs. All other actual gate bits and the designated output bit retain the unrestricted Boolean cost.
noncomputable def
Algebraic.Cutwidth.Aggregate.Geometry.Joint.outputKeyWeightBoundOfClasses
{n g : ℕ}
(p : Program Aggregate.Geometry.signature n g)
(U : Finset (Fin n))
(out : Wire n g)
(T W : Finset (Fin g))
(disjoint : Disjoint T W)
(two : ∀ i ∈ T, Aggregate.Geometry.SelectedPair (p.lines i) U)
(three : ∀ i ∈ W, 3 ≤ (literalVars (lineLiterals (p.lines i) U)).card)
:
Entropy.WeightBound (fun (x : ↥U → Bool) => Aggregate.Geometry.outputKey p U out (glue U x fun (x : ↥Uᶜ) => false))
((↑g + 1) * Real.log 2 - ↑T.card * (Real.binEntropy (1 / 4) - 1 / 2 * Real.log 2) - ↑W.card * (Real.log 2 - Real.binEntropy (1 / 8)) + ↑U.card * (Real.binEntropy (1 / 4) - 3 / 4 * Real.log 2))
Separate conjunction classes extend to a certificate for the actual whole message.
Equations
- One or more equations did not get rendered due to their size.