diff --git a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy.lean b/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy.lean index 5b611f79..e5c04143 100644 --- a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy.lean +++ b/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 diff --git a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Finite.lean b/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Finite.lean index 04aae06e..5353de27 100644 --- a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Finite.lean +++ b/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 : ℝ} diff --git a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair.lean b/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair.lean new file mode 100644 index 00000000..5b411d9d --- /dev/null +++ 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 diff --git a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Defs.lean b/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Defs.lean new file mode 100644 index 00000000..958069c5 --- /dev/null +++ b/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 diff --git a/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Internal.lean b/Complexitylib/Algebraic/LowerBound/Cutwidth/Aggregate/Geometry/Entropy/Pair/Internal.lean new file mode 100644 index 00000000..12c66afe --- /dev/null +++ b/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 diff --git a/blueprint/src/chapters/lowerbounds.tex b/blueprint/src/chapters/lowerbounds.tex index 2c7fcc56..4a30235a 100644 --- a/blueprint/src/chapters/lowerbounds.tex +++ b/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,