Exact entropy cap for overlapping actual conjunction features

Each Boolean feature need only imply a signed conjunction on two primary coordinates. It may include arbitrary predicates of all inputs, as actual conjunction gates with internal predecessors do. If the primary pairs overlap, the two features together cost at most the entropy of (5/8, 1/8, 1/8, 1/8).

Constant false features are included. Consequently the saving over the two quarter-biased marginal caps is not a mutual-information lower bound.

noncomputable def Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.dominatedPairWeightBound {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) (first second : (V → Bool) → Bool) (hfirst : ∀ (x : V → Bool), first x = true → e.eval x = true) (hsecond : ∀ (x : V → Bool), second x = true → f.eval x = true) : WeightBound (fun (x : V → Bool) => (first x, second x)) pairEntropyCost

Intersecting primary pairs bound the joint cost even with arbitrary extra predicates.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairEntropySaving_pos : 0 < pairEntropySaving

The joint cap is strictly smaller than two separate quarter-biased marginal caps.