Removing frozen coordinates from a complete message

On the majority event, the designated message bits are all false. The remaining message therefore retains the full key's fiber bound on that event. No independence of the remaining messages is assumed.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_fiber_le_of_refines_on {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] (event : Finset X) (key : X → Y) (residual : X → Z) (refines : ∀ x ∈ event, ∀ y ∈ event, residual x = residual y → key x = key y) {K : ℕ} (fibers : ∀ (y : Y), {x : X | key x = y}.card ≤ K) (z : Z) : {x ∈ event | residual x = z}.card ≤ K

On a restricted event, a key determining the original key preserves its fiber bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.key_eq_false_of_majority {I : Type u_1} {V : Type u_2} [Fintype V] (key : (V → Bool) → I → Bool) (S : Finset I) (edge : ↥S → Entropy.SignedEdge V) (forced : ∀ (x : V → Bool) (i : ↥S), key x ↑i = true → (edge i).eval x = true) {x : V → Bool} (hx : x ∈ majorityInputs edge) (i : ↥S) : key x ↑i = false

A rare selected message implies its chosen two-coordinate conjunction.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.card_residual_fiber_le {I : Type u_1} {V : Type u_2} [Fintype V] (key : (V → Bool) → I → Bool) (S : Finset I) (edge : ↥S → Entropy.SignedEdge V) (forced : ∀ (x : V → Bool) (i : ↥S), key x ↑i = true → (edge i).eval x = true) {K : ℕ} (fibers : ∀ (y : I → Bool), {x : V → Bool | key x = y}.card ≤ K) (y : { i : I // i ∉ S } → Bool) : {x ∈ majorityInputs edge | (fun (i : { i : I // i ∉ S }) => key x ↑i) = y}.card ≤ K

Deleting the frozen coordinates preserves the fiber bound on the majority event.