Balanced outputs avoid multiple-primary conjunctions

A permutation has balanced, distinct output coordinates. Each multiple-primary conjunction has a nondefault fibre of size at most one quarter of the cube, so it cannot be one of those outputs. Nonprojection outputs must be actual gate wires.

theorem Algebraic.Aggregate.Geometry.two_mul_card_coordinate_fibre {n : ℕ} (i : Fin n) (b : Bool) : 2 * Fintype.card { x : Fin n → Bool // x i = b } = 2 ^ n

Every primary-coordinate fibre occupies exactly half of the Boolean cube.

theorem Algebraic.Aggregate.Geometry.two_mul_card_permutation_fibre {n : ℕ} (F : (Fin n → Bool) → Fin n → Bool) (bijective : Function.Bijective F) (i : Fin n) (b : Bool) : 2 * Fintype.card { x : Fin n → Bool // F x i = b } = 2 ^ n

Every coordinate of a permutation is balanced.

theorem Algebraic.Aggregate.Geometry.multiPrimary_line_quarter {n g : ℕ} (p : Program signature n g) (line : Line signature n g) (marked : multiPrimary line = true) : ∃ (b : Bool), 4 * Fintype.card { x : Fin n → Bool // lineFunction p line x = b } ≤ 2 ^ n

A marked line forces two primary coordinates in its nondefault fibre.

theorem Algebraic.Aggregate.Geometry.multiPrimary_quarter {n g : ℕ} (p : Program signature n g) (gate : Fin g) (marked : multiPrimary (p.lines gate) = true) : ∃ (b : Bool), 4 * Fintype.card { x : Fin n → Bool // p.gateFunction interpretation gate x = b } ≤ 2 ^ n

A marked actual gate has a nondefault fibre of at most one quarter of all inputs.

theorem Algebraic.Aggregate.Geometry.input_add_multiCount_le_size {n : ℕ} (c : Circuit signature n n) (bijective : Function.Bijective (c.eval interpretation)) (nonprojection : ∀ (i j : Fin n), c.outputFunction interpretation i ≠ fun (x : Fin n → Bool) => x j) : n + multiCount c.program ≤ c.size

Distinct nonprojection outputs of a permutation occupy unmarked actual gates.