Restricting conjunctions before counting nonlinear generators

Process the conjunction gates in program order. While the current flat is larger than the target, fix one live literal of each conjunction to its controlling value, so the gate becomes constant and the codimension grows by at most one. Every gate then stays affine on the flat. Once the target codimension is reached, the remaining conjunctions become generators: every gate is affine on the flat modulo their span. Output components that are independent modulo affine functions on the final flat therefore need one remaining generator each.

theorem Algebraic.Aggregate.Geometry.affineOn_iff_mem_flatAffineFunctions {n : ℕ} {S : AffineFlat n} {f : (Fin n → Bool) → Bool} : AffineOn S f ↔ (fun (x : Fin n → Bool) => bitValue (f x)) ∈ flatAffineFunctions S

A Boolean function is affine on a flat exactly when its prime-field values are.

theorem Algebraic.Aggregate.Geometry.flatAffineFunctions_anti {n : ℕ} {S T : AffineFlat n} (sub : T.carrier ⊆ S.carrier) : flatAffineFunctions S ≤ flatAffineFunctions T

Functions affine on a flat remain affine on every smaller flat.

theorem Algebraic.Aggregate.Geometry.const_mem_flatAffineFunctions {n : ℕ} (S : AffineFlat n) (b : ZMod 2) : (fun (x : Fin n → Bool) => b) ∈ flatAffineFunctions S

Constant prime-field functions are affine on every flat.

theorem Algebraic.Aggregate.Geometry.coordinate_mem_flatAffineFunctions {n : ℕ} (S : AffineFlat n) (i : Fin n) : (fun (x : Fin n → Bool) => bitValue (x i)) ∈ flatAffineFunctions S

Primary input bits are affine on every flat.

theorem Algebraic.Aggregate.Geometry.conjunctionCount_gate {n g : ℕ} (p : Program signature n g) (line : Line signature n g) : conjunctionCount (p.gate line) = conjunctionCount p + if Op.isConjunction line.op = true then 1 else 0

Appending a line adds one to the conjunction count exactly for conjunctions.

theorem Algebraic.Aggregate.Geometry.exists_restriction_generators {n g : ℕ} (p : Program signature n g) (target : ℕ) : ∃ (S : AffineFlat n) (d : ℕ) (T : Submodule (ZMod 2) ((Fin n → Bool) → ZMod 2)), 2 ^ d * S.carrier.card = 2 ^ n ∧ d ≤ target ∧ (d < target → T = ⊥) ∧ d + Module.finrank (ZMod 2) ↥T ≤ conjunctionCount p ∧ ∀ (i : Fin g), (fun (x : Fin n → Bool) => bitValue (p.gateFunction interpretation i x)) ∈ flatAffineFunctions S ⊔ T

The restriction process for an actual program. The flat has codimension d at most the target, and restrictions stop only at the target. Each processed conjunction raises the codimension by at most one, and each later conjunction contributes at most one dimension to T. Modulo T, every gate is affine on the flat.

theorem Algebraic.Aggregate.Geometry.output_add_input_le_of_nonaffineOnFlats {n m D : ℕ} (c : Circuit signature n m) (rigid : NonaffineOnFlats (c.eval interpretation) D) (outputs : 0 < m) (dimension : D ≤ n) : m + n ≤ conjunctionCount c.program + D

The restriction–rank inequality: output components independent modulo affine functions on every flat of 2^D points force m + n - D conjunction gates.