Transition capacity from the distribution of traces

Optimizing the existing pruning inequality charges each used transition by the smaller of its frontier allowance and the absolute weight of its inputs. This is a one-shot quantity: low average Shannon entropy alone does not bound it. A square-root moment provides a convenient sufficient bound without assuming independent boundary signals.

theorem Complexity.Frontier.sumOn_fibers {α : Type u_1} {β : Type u_2} [Finite α] (w : α → ℝ) (S : Set α) (f : α → β) (T : Finset β) : ∑ y ∈ T, sumOn w {x : α | x ∈ S ∧ f x = y} = sumOn w {x : α | x ∈ S ∧ f x ∈ T}

theorem Complexity.Frontier.exists_capped_codebook {α : Type u_1} {β : Type u_2} [Finite α] (w : α → ℝ) (S : Set α) (f : α → β) (c : ℝ) : ∃ (T : Finset β), c * ↑T.card + sumOn w {x : α | x ∈ S ∧ f x ∉ T} = ∑ y ∈ ⋯.toFinset, min c (sumOn w {x : α | x ∈ S ∧ f x = y})

Keep a fiber exactly when its weight exceeds the cost of describing it. The resulting description cost plus discarded weight is the sum of the capped fiber weights.

noncomputable def Complexity.Frontier.Sweep.cappedCapacity {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) (w : (ι → U) → ℝ) (c : ℝ) : ℝ

The capped mass of the transition fibers, summed over all steps.

Equations

• P.cappedCapacity w c = ∑ t ∈ Finset.range P.length, ∑ e ∈ ⋯.toFinset, min c (Complexity.Frontier.sumOn w {x : ι → U | x ∈ S ∧ P.transition t x = e})

theorem Complexity.Frontier.Sweep.abs_sumOn_le_capped {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) (hP : P.Coherent) (hmono : Monotone P.revealed) (hL : 0 < P.length) {KL KR : ℕ} (hKL : 1 < KL) (hKR : 1 < KR) {w cost : (ι → U) → ℝ} {a : ℝ} (ha : 0 ≤ a) (hw : ∀ (x : ι → U), |w x| ≤ a) (hc : ∀ (x : ι → U), 0 ≤ cost x) (hrect : RectangleBudget w cost KL KR) : |sumOn w S| ≤ sumOn cost S + P.cappedCapacity (fun (x : ι → U) => |w x|) (a * ↑((KL - 1) * (KR - 1)))

Distribution-sensitive frontier bound. A transition costs at most either its frontier allowance or the absolute weight of all inputs using it.

noncomputable def Complexity.Frontier.Sweep.rootCapacity {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) (w : (ι → U) → ℝ) : ℝ

The sum of square roots of transition fiber weights. After normalizing a single layer to probability one, twice its base-two logarithm is Renyi entropy of order 1/2.

Equations

• P.rootCapacity w = ∑ t ∈ Finset.range P.length, ∑ e ∈ ⋯.toFinset, √(Complexity.Frontier.sumOn w {x : ι → U | x ∈ S ∧ P.transition t x = e})

theorem Complexity.Frontier.Sweep.cappedCapacity_le_root {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) {w : (ι → U) → ℝ} (hw : ∀ (x : ι → U), 0 ≤ w x) {c : ℝ} (hc : 0 ≤ c) : P.cappedCapacity w c ≤ √c * P.rootCapacity w

theorem Complexity.Frontier.min_le_rpow_mul_rpow {c m θ : ℝ} (hc : 0 ≤ c) (hm : 0 ≤ m) (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1) : min c m ≤ c ^ (1 - θ) * m ^ θ

The capped charge is bounded by any fractional moment, not just the square root. The endpoints are included; entropy applications use 0 < θ < 1.

noncomputable def Complexity.Frontier.Sweep.momentCapacity {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) (w : (ι → U) → ℝ) (θ : ℝ) : ℝ

Sum of the θ-powers of the transition fiber weights.

Equations

• P.momentCapacity w θ = ∑ t ∈ Finset.range P.length, ∑ e ∈ ⋯.toFinset, Complexity.Frontier.sumOn w {x : ι → U | x ∈ S ∧ P.transition t x = e} ^ θ

theorem Complexity.Frontier.Sweep.cappedCapacity_le_moment {ι : Type u_3} {U : Type u_4} {M : Type u_5} [Finite ι] [Finite U] {S : Set (ι → U)} (P : Sweep S M) {w : (ι → U) → ℝ} (hw : ∀ (x : ι → U), 0 ≤ w x) {c θ : ℝ} (hc : 0 ≤ c) (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1) : P.cappedCapacity w c ≤ c ^ (1 - θ) * P.momentCapacity w θ

theorem Complexity.Frontier.agreement_le_capped_sweeps {ι : Type u_3} {U : Type u_4} [Finite ι] [Finite U] [Nonempty U] {f g : (ι → U) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) {Msg : Bool → Type u_6} (P : (b : Bool) → Sweep {x : ι → U | g x = b} (Msg b)) (hP : ∀ (b : Bool), (P b).Coherent) (hmono : ∀ (b : Bool), Monotone (P b).revealed) (hL : ∀ (b : Bool), 0 < (P b).length) : agreement f g ≤ (1 + β) / 2 + ((P true).cappedCapacity (fun (x : ι → U) => 1) ↑((K - 1) ^ 2) + (P false).cappedCapacity (fun (x : ι → U) => 1) ↑((K - 1) ^ 2)) / (2 * ↑(Nat.card (ι → U)))

Capped transition masses of both output classes control prediction agreement.

theorem Complexity.Frontier.agreement_le_root_sweeps {ι : Type u_3} {U : Type u_4} [Finite ι] [Finite U] [Nonempty U] {f g : (ι → U) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) {Msg : Bool → Type u_6} (P : (b : Bool) → Sweep {x : ι → U | g x = b} (Msg b)) (hP : ∀ (b : Bool), (P b).Coherent) (hmono : ∀ (b : Bool), Monotone (P b).revealed) (hL : ∀ (b : Bool), 0 < (P b).length) : agreement f g ≤ (1 + β) / 2 + √↑((K - 1) ^ 2) * (((P true).rootCapacity fun (x : ι → U) => 1) + (P false).rootCapacity fun (x : ι → U) => 1) / (2 * ↑(Nat.card (ι → U)))

A square-root moment of the complete transition replaces its support size. No independence between coordinates, boundary signals, or layers is assumed.

theorem Complexity.Frontier.agreement_le_moment_sweeps {ι : Type u_3} {U : Type u_4} [Finite ι] [Finite U] [Nonempty U] {f g : (ι → U) → Bool} {K : ℕ} {β θ : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) (hθ : 0 ≤ θ) (hθ1 : θ ≤ 1) {Msg : Bool → Type u_6} (P : (b : Bool) → Sweep {x : ι → U | g x = b} (Msg b)) (hP : ∀ (b : Bool), (P b).Coherent) (hmono : ∀ (b : Bool), Monotone (P b).revealed) (hL : ∀ (b : Bool), 0 < (P b).length) : agreement f g ≤ (1 + β) / 2 + ↑((K - 1) ^ 2) ^ (1 - θ) * ((P true).momentCapacity (fun (x : ι → U) => 1) θ + (P false).momentCapacity (fun (x : ι → U) => 1) θ) / (2 * ↑(Nat.card (ι → U)))

Arbitrary fractional moments bound agreement. Parameters close to one allow restriction-tree accounting to use average measure drops with arbitrarily small slack.