Exact counting for disjoint conjunction majority inputs

Split the original cube into all selected endpoints and the unused coordinates. Each selected pair independently allows exactly three of its four assignments.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Internal.local_card {E : Type u_1} [Fintype E] (left right : E → Bool) : Fintype.card { x : E × Bool → Bool // ∀ (e : E), (x (e, false) == left e && x (e, true) == right e) = false } = 3 ^ Fintype.card E

Independent signed pairs have exactly three majority assignments each.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Internal.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)

The majority set of disjoint signed conjunctions has its exact product cardinality.