feat(Circuits): cap entropy of overlapping actual features

Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy.lean

@@ -8,6 +8,7 @@ module
 public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Collisions
 public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Averaging
 public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.OneWay
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Pair
 
 /-!
 # Entropy savings from designated primary-input pairs

Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Finite.lean

@@ -65,6 +65,18 @@ def WeightBound.mono {X Y : Type*} [Fintype X] [Fintype Y]
       exact le_trans (mul_le_mul_of_nonpos_left hab
         (neg_nonpos.mpr (Nat.cast_nonneg _))) bound.log_bound }
 
+/-- Reuse a weight when changing the message only increases its pointwise weight. -/
+def WeightBound.ofPointwiseWeightLE {X Y : Type*} [Fintype X] [Fintype Y]
+    {key : X → Y} {cost : ℝ} (bound : WeightBound key cost) (next : X → Y)
+    (increase : ∀ x, bound.weight (key x) ≤ bound.weight (next x)) :
+    WeightBound next cost where
+  weight := bound.weight
+  nonneg := bound.nonneg
+  mass := bound.mass
+  positive x := lt_of_lt_of_le (bound.positive x) (increase x)
+  log_bound := le_trans bound.log_bound
+    (Finset.sum_le_sum fun x _ => Real.log_le_log (bound.positive x) (increase x))
+
 /-- Increasing a conditional cost preserves its certificate. -/
 def ConditionalWeightBound.mono {X Y Z : Type*} [Fintype X] [Fintype Y]
     {key : X → Y} {parent : X → Z} {a b : ℝ}

Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under MIT license as described in the file Complexitylib/Algebraic/LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Pair.Internal
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace Algebraic.Cutwidth.Aggregate.Geometry.Entropy
+
+open scoped Classical
+
+/-- Intersecting primary pairs bound the joint cost even with arbitrary extra predicates. -/
+noncomputable def SignedEdge.dominatedPairWeightBound {V : Type*}
+    [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, first x = true → e.eval x = true)
+    (hsecond : ∀ x, second x = true → f.eval x = true) :
+    WeightBound (fun x => (first x, second x)) pairEntropyCost := by
+  by_cases h₁ : e.left = f.left
+  · exact PairInternal.dominatedSharedLeft e f h₁ first second hfirst hsecond
+  by_cases h₂ : e.left = f.right
+  · exact PairInternal.dominatedSharedLeft e f.reverse h₂ first second hfirst
+      (by simpa only [SignedEdge.eval_reverse] using hsecond)
+  by_cases h₃ : e.right = f.left
+  · exact PairInternal.dominatedSharedLeft e.reverse f h₃ first second
+      (by simpa only [SignedEdge.eval_reverse] using hfirst) hsecond
+  have h₄ := ((overlap.resolve_left h₁).resolve_left h₂).resolve_left h₃
+  exact PairInternal.dominatedSharedLeft e.reverse f.reverse h₄ first second
+    (by simpa only [SignedEdge.eval_reverse] using hfirst)
+    (by simpa only [SignedEdge.eval_reverse] using hsecond)
+
+/-- The joint cap is strictly smaller than two separate quarter-biased marginal caps. -/
+theorem pairEntropySaving_pos : 0 < pairEntropySaving := by
+  have bound : Real.log ((3 : ℝ) ^ 12) < Real.log ((2 : ℝ) ^ 8 * 5 ^ 5) :=
+    Real.log_lt_log (by norm_num) (by norm_num)
+  rw [Real.log_mul (by norm_num) (by norm_num), Real.log_pow, Real.log_pow,
+    Real.log_pow] at bound
+  norm_num only [Nat.cast_ofNat] at bound
+  rw [pairEntropySaving, pairEntropyCost, binEntropy_quarter_eq]
+  linarith
+
+end Algebraic.Cutwidth.Aggregate.Geometry.Entropy

Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Defs.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under MIT license as described in the file Complexitylib/Algebraic/LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Local.Defs
+
+/-!
+# The entropy cost of an overlapping pair of conjunction features
+
+The extremal four-outcome distribution is `(5/8, 1/8, 1/8, 1/8)`. Costs use
+natural logarithms, consistently with `WeightBound`; divide by `Real.log 2`
+to obtain bits. The saving compares this joint cost with two quarter-biased
+marginal costs, rather than asserting a mutual-information lower bound.
+-/
+
+@[expose] public section
+
+namespace Algebraic.Cutwidth.Aggregate.Geometry.Entropy
+
+/-- Natural-log entropy of the extremal overlapping two-conjunction table. -/
+noncomputable def pairEntropyCost : ℝ := 3 * Real.log 2 - (5 / 8) * Real.log 5
+
+/-- The saving over separately charging two quarter-biased Boolean messages. -/
+noncomputable def pairEntropySaving : ℝ := 2 * Real.binEntropy (1 / 4) - pairEntropyCost
+
+end Algebraic.Cutwidth.Aggregate.Geometry.Entropy

Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Internal.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under MIT license as described in the file Complexitylib/Algebraic/LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Pair.Defs
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Local.Coordinates
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Local.Cases.Defs
+public import Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Entropy.Local.Numbers
+public import Mathlib.Data.Fintype.Vector
+
+/-!
+# Exact pair weights and their transport to dominated Boolean features
+
+Compatible primary conjunctions use weights `(5/8, 1/8, 1/8, 1/8)`; incompatible
+ones use `(1/2, 1/4, 1/4, 0)`. Both weights increase when a true feature is
+turned false. Thus arbitrary additional gate predicates preserve the bound.
+-/
+
+@[expose] public section
+
+namespace Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal
+
+open scoped BigOperators Classical
+
+/-- Pair weights for compatible literals and for mutually exclusive conjunctions. -/
+noncomputable def weight (disjoint : Bool) (y : Bool × Bool) : ℝ :=
+  if disjoint then
+    if y.1 then (if y.2 then 0 else 1 / 4) else (if y.2 then 1 / 4 else 1 / 2)
+  else if y.1 || y.2 then 1 / 8 else 5 / 8
+
+theorem weight_nonneg (disjoint : Bool) (y : Bool × Bool) : 0 ≤ weight disjoint y := by
+  rcases y with ⟨a, b⟩
+  cases disjoint <;> cases a <;> cases b <;> norm_num [weight]
+
+theorem weight_mass (disjoint : Bool) : ∑ y, weight disjoint y = 1 := by
+  cases disjoint <;> norm_num [Fintype.sum_prod_type, Fintype.sum_bool, weight]
+
+theorem weight_le (disjoint a b c d : Bool)
+    (first : a = true → c = true) (second : b = true → d = true) :
+    weight disjoint (c, d) ≤ weight disjoint (a, b) := by
+  cases disjoint <;> cases a <;> cases b <;> cases c <;> cases d <;>
+    norm_num [weight] at *
+
+private theorem univ_bool_two : (Finset.univ : Finset (Fin 2 → Bool)) =
+    {![false, false], ![false, true], ![true, false], ![true, true]} := by decide
+
+private theorem univ_bool_three : (Finset.univ : Finset (Fin 3 → Bool)) =
+    {![false, false, false], ![false, false, true], ![false, true, false],
+      ![false, true, true], ![true, false, false], ![true, false, true],
+      ![true, true, false], ![true, true, true]} := by decide
+
+private theorem log_four : Real.log 4 = 2 * Real.log 2 := by
+  simpa only [show (2 : ℝ) ^ 2 = 4 by norm_num, Nat.cast_ofNat] using
+    Real.log_pow (2 : ℝ) 2
+
+private theorem log_eight : Real.log 8 = 3 * Real.log 2 := by
+  simpa only [show (2 : ℝ) ^ 3 = 8 by norm_num, Nat.cast_ofNat] using
+    Real.log_pow (2 : ℝ) 3
+
+theorem disjoint_cost_le : (3 / 2) * Real.log 2 ≤ pairEntropyCost := by
+  have bound : Real.log ((5 : ℝ) ^ 5) ≤ Real.log ((2 : ℝ) ^ 12) :=
+    Real.log_le_log (by norm_num) (by norm_num)
+  rw [Real.log_pow, Real.log_pow] at bound
+  norm_num only [Nat.cast_ofNat] at bound
+  unfold pairEntropyCost
+  linarith
+
+/-- Exact two-coordinate certificate, including equal and incompatible signed supports. -/
+noncomputable def parallel (a b c d : Bool) :
+    WeightBound (fun x : Fin 2 → Bool => (pairBit 0 1 a b x, pairBit 0 1 c d x))
+      pairEntropyCost where
+  weight := weight ((a != c) || (b != d))
+  nonneg := weight_nonneg _
+  mass := weight_mass _
+  positive x := by
+    cases a <;> cases b <;> cases c <;> cases d <;>
+      cases h₀ : x 0 <;> cases h₁ : x 1 <;> norm_num [pairBit, weight, h₀, h₁]
+  log_bound := by
+    have bound := disjoint_cost_le
+    have five : 0 ≤ Real.log 5 := Real.log_nonneg (by norm_num)
+    unfold pairEntropyCost at *
+    cases a <;> cases b <;> cases c <;> cases d <;>
+      norm_num [univ_bool_two, pairBit, weight, Real.log_div, Real.log_inv,
+        log_four, log_eight] <;> linarith
+
+/-- Exact three-coordinate certificate for a pair sharing its first coordinate. -/
+noncomputable def shared (a b c d : Bool) :
+    WeightBound (fun x : Fin 3 → Bool => (pairBit 0 1 a b x, pairBit 0 2 c d x))
+      pairEntropyCost where
+  weight := weight (a != c)
+  nonneg := weight_nonneg _
+  mass := weight_mass _
+  positive x := by
+    cases a <;> cases b <;> cases c <;> cases d <;>
+      cases h₀ : x 0 <;> cases h₁ : x 1 <;> cases h₂ : x 2 <;>
+        norm_num [pairBit, weight, h₀, h₁, h₂]
+  log_bound := by
+    have bound := disjoint_cost_le
+    unfold pairEntropyCost at *
+    cases a <;> cases b <;> cases c <;> cases d <;>
+      norm_num [univ_bool_three, pairBit, weight, Real.log_div, Real.log_inv,
+        log_four, log_eight] <;> linarith
+
+/-- Lift the local pair certificates and permit arbitrary additional Boolean predicates. -/
+noncomputable def dominatedSharedLeft {V : Type*} [Fintype V] [DecidableEq V]
+    (e f : SignedEdge V) (left : e.left = f.left)
+    (first second : (V → Bool) → Bool)
+    (hfirst : ∀ x, first x = true → e.eval x = true)
+    (hsecond : ∀ x, second x = true → f.eval x = true) :
+    WeightBound (fun x => (first x, second x)) pairEntropyCost := by
+  by_cases right : e.right = f.right
+  · let bound := (parallel e.leftSign e.rightSign f.leftSign f.rightSign).precompCoordinates
+      (pairCoordinates e.left e.right e.distinct)
+    apply bound.ofPointwiseWeightLE
+    intro x
+    apply weight_le
+    · simpa [SignedEdge.eval, pairBit, pairCoordinates, Function.comp_def] using hfirst x
+    · simpa [SignedEdge.eval, pairBit, pairCoordinates, Function.comp_def, ← left, ← right]
+        using hsecond x
+  · have distinct : e.left ≠ f.right := by simpa only [left] using f.distinct
+    let bound := (shared e.leftSign e.rightSign f.leftSign f.rightSign).precompCoordinates
+      (tripleCoordinates e.left e.right f.right e.distinct distinct right)
+    apply bound.ofPointwiseWeightLE
+    intro x
+    apply weight_le
+    · simpa [SignedEdge.eval, pairBit, tripleCoordinates, Function.comp_def] using hfirst x
+    · simpa [SignedEdge.eval, pairBit, tripleCoordinates, Function.comp_def, ← left]
+        using hsecond x
+
+end Algebraic.Cutwidth.Aggregate.Geometry.Entropy.PairInternal

blueprint/src/chapters/lowerbounds.tex

@@ -10610,6 +10610,36 @@ \section{Results from the algebraic-circuits library}
   gate saving in the joint message bound.
 \end{definition}
 
+\begin{theorem}[An exact overlap cap for actual Boolean features]
+  \label{thm:lowerbounds-algebraic-geometry-actual-pair-entropy}
+  \lean{Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairEntropyCost,
+    Algebraic.Cutwidth.Aggregate.Geometry.Entropy.SignedEdge.dominatedPairWeightBound,
+    Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pairEntropySaving_pos}
+  \leanok
+  Let $A_1,A_2$ be signed conjunctions on two distinct primary coordinates
+  each, with intersecting supports, under uniform independent primary bits.
+  Suppose Boolean features $Y_i$ satisfy $Y_i\le A_i$ pointwise. The features
+  may otherwise depend arbitrarily on all primary coordinates. There is a
+  normalized finite weight certificate for $(Y_1,Y_2)$ of natural-log cost
+  \[
+    J=3\log 2-\tfrac58\log 5
+      =H(5/8,1/8,1/8,1/8).
+  \]
+  The saving $2H(1/4,3/4)-J$ is strictly positive. Constant false features
+  are allowed, so this is not a positive lower bound on mutual information.
+\end{theorem}
+\begin{proof}
+  \leanok
+  For compatible literal patterns, use weights $(5/8,1/8,1/8,1/8)$ in
+  the order $(00,01,10,11)$. For incompatible patterns, use
+  $(1/2,1/4,1/4,0)$, whose cost is at most $J$. Exact two- and three-bit
+  truth tables cover equal supports and one-coordinate intersections.
+  Both weights increase when either Boolean coordinate changes from true
+  to false. Replacing $A_i$ by any dominated $Y_i$ therefore preserves the
+  average logarithmic weight bound, even when the extra predicates depend
+  on every primary bit. The strict saving reduces to $3^{12}<2^8 5^5$.
+\end{proof}
+
 \begin{theorem}[The finite joint-message inequality]
   \label{thm:lowerbounds-algebraic-geometry-joint-finite}
   \lean{Algebraic.Cutwidth.Aggregate.Geometry.Entropy.Graph.input_le_cost_of_fibres,