Literal counts on a large conjunction majority fiber

Within the product of three-state majority pairs, forcing d distinct signed coordinates retains at most (2/3)^d of all inputs. This applies to any remaining conjunction, without an independence assumption about its output.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.three_pow_mul_card_le_of_forces {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) (S : Finset V) (bits : V → Bool) (P : (V → Bool) → Prop) [DecidablePred P] (forces : ∀ (x : V → Bool), P x → ∀ v ∈ S, x v = bits v) : 3 ^ S.card * {x : ↥(majorityInputs edge) | P ↑x}.card ≤ 2 ^ S.card * (majorityInputs edge).card

Fixing selected coordinates inside the majority event incurs a two-thirds cost per bit.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.three_pow_mul_card_evalLiterals_le {E : Type u_1} {V : Type u_2} [Fintype E] [Fintype V] [DecidableEq V] (edge : E → Entropy.SignedEdge V) (disjoint : Function.Injective (endpoint edge)) {L : Finset (V × Bool)} {d : ℕ} (many : d ≤ (Joint.literalVars L).card) : 3 ^ d * {x : ↥(majorityInputs edge) | Joint.evalLiterals L ↑x = true}.card ≤ 2 ^ d * (majorityInputs edge).card

Any d distinct literals in a conjunction retain at most a (2/3)^d fraction.