Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Fiber.Counting

Large fibers from disjoint conjunction summaries #

Each disjoint signed conjunction has three majority assignments on its two variables. After selecting all these majority outcomes, any remaining finite message partitions a set of exactly 3 ^ |E| * 2 ^ (|V| - 2 * |E|) inputs.

source
@[simp]
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.endpoint_false {E : Type u_1} {V : Type u_2} (edge : E → Entropy.SignedEdge V) (e : E) :
endpoint edge (e, false) = (edge e).left

The false endpoint is the left input of the selected conjunction.

source
@[simp]
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.endpoint_true {E : Type u_1} {V : Type u_2} (edge : E → Entropy.SignedEdge V) (e : E) :
endpoint edge (e, true) = (edge e).right

The true endpoint is the right input of the selected conjunction.

source
@[simp]
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.mem_majorityInputs {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (x : V → Bool) :
x ∈ majorityInputs edge ↔ ∀ (e : E), (edge e).eval x = false

Majority inputs make every selected signed conjunction false.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.two_mul_card_le {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) :
2 * Fintype.card E ≤ Fintype.card V

Disjoint signed pairs occupy exactly two distinct coordinates per edge.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_majorityInputs {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) :
(majorityInputs edge).card = 3 ^ Fintype.card E * 2 ^ (Fintype.card V - 2 * Fintype.card E)

All majority outcomes of disjoint signed conjunctions occur on this many inputs.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_le_mul_of_fibers {X : Type u_1} {Y : Type u_2} [Fintype Y] (inputs : Finset X) (key : X → Y) {K : ℕ} (fibers : ∀ (y : Y), {x ∈ inputs | key x = y}.card ≤ K) :
inputs.card ≤ Fintype.card Y * K

A finite key with fibers of size at most K covers at most |Y| * K inputs.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_majorityInputs_le_mul_of_fibers {E : Type u_1} {V : Type u_2} {Y : Type u_3} [Fintype E] [Fintype V] [Fintype Y] (edge : E → Entropy.SignedEdge V) (key : (V → Bool) → Y) {K : ℕ} (fibers : ∀ (y : Y), {x ∈ majorityInputs edge | key x = y}.card ≤ K) :
(majorityInputs edge).card ≤ Fintype.card Y * K

Restricting to majority outcomes leaves the same finite-key fiber bound.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.majority_product_le_of_fibers {E : Type u_1} {V : Type u_2} {Y : Type u_3} [Fintype E] [Fintype V] [Fintype Y] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (key : (V → Bool) → Y) {K : ℕ} (fibers : ∀ (y : Y), {x ∈ majorityInputs edge | key x = y}.card ≤ K) :
3 ^ Fintype.card E * 2 ^ (Fintype.card V - 2 * Fintype.card E) ≤ Fintype.card Y * K

Exact majority counting and a fiber cap bound the residual message alphabet.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.log_card_le_of_fibers {E : Type u_1} {V : Type u_2} {Y : Type u_3} [Fintype E] [Fintype V] [Fintype Y] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (key : (V → Bool) → Y) {K : ℕ} (hK : 0 < K) (fibers : ∀ (y : Y), {x ∈ majorityInputs edge | key x = y}.card ≤ K) :
↑(Fintype.card V) + (Real.logb 2 3 - 2) * ↑(Fintype.card E) ≤ Real.logb 2 ↑(Fintype.card Y) + Real.logb 2 ↑K

The logarithmic count for an arbitrary finite residual message alphabet.

source
theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.log_card_le_of_boolean_fibers {E : Type u_1} {V : Type u_2} {R : Type u_3} [Fintype E] [Fintype V] [Fintype R] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (key : (V → Bool) → R → Bool) {K : ℕ} (hK : 0 < K) (fibers : ∀ (y : R → Bool), {x ∈ majorityInputs edge | key x = y}.card ≤ K) :
↑(Fintype.card V) + (Real.logb 2 3 - 2) * ↑(Fintype.card E) ≤ ↑(Fintype.card R) + Real.logb 2 ↑K

A residual Boolean key spends one bit per coordinate after majority selection.