Exact complexity of linear targets with linear helpers

Over ZMod 2, a nonzero linear form is computable from a set of linear sources exactly when its coefficient vector lies in their span. A binary circuit must touch enough sources, even if its gates are nonlinear. If XOR can be computed in one gate, a minimum-weight representation gives a matching XOR tree. All gates are charged one, including any constant gates.

def Algebraic.ConditionalComplexity.Linear.weight {n : ℕ} (coefficients : Fin n → ZMod 2) : ℕ

Hamming weight of a coefficient vector.

Equations

• Algebraic.ConditionalComplexity.Linear.weight coefficients = {i : Fin n | coefficients i ≠ 0}.card

def Algebraic.ConditionalComplexity.Linear.forms {k n : ℕ} {K : Type u_1} (rows : Fin k → Fin n → K) [Semiring K] : Target K n k

The family of linear forms given by the rows of a coefficient matrix.

Equations

• Algebraic.ConditionalComplexity.Linear.forms rows input i = rows i ⬝ᵥ input

theorem Algebraic.ConditionalComplexity.Linear.mem_span_of_sourceSupport {n k : ℕ} {K : Type} [Field K] (target : Fin n → K) (rows : Fin k → Fin n → K) (selected : Finset (Fin k)) (determines : SourceSupport (fun (input : Fin n → K) (x : Fin 1) => target ⬝ᵥ input) (forms rows) selected) : target ∈ Submodule.span K (Set.range fun (i : ↥selected) => rows ↑i)

If selected linear forms determine another linear form, their coefficient vectors span its coefficient vector.

theorem Algebraic.ConditionalComplexity.Linear.exists_representation_of_sourceSupport {n k : ℕ} (target : Fin n → ZMod 2) (rows : Fin k → Fin n → ZMod 2) (selected : Finset (Fin k)) (determines : SourceSupport (fun (input : Fin n → ZMod 2) (x : Fin 1) => target ⬝ᵥ input) (forms rows) selected) : ∃ (coefficients : Fin k → ZMod 2), ∑ i : Fin k, coefficients i • rows i = target ∧ weight coefficients ≤ selected.card

A determining source subset yields a representation using no more nonzero coefficients than the number of selected sources.

theorem Algebraic.ConditionalComplexity.Linear.relativeGateComplexity_le_weight {σ : Signature} {n k : ℕ} (interpretation : Interpretation σ (ZMod 2)) (addition : Circuit σ 2 1) (addition_size : addition.size = 1) (addition_eval : ∀ (input : Fin 2 → ZMod 2), addition.eval interpretation input 0 = input 0 + input 1) (target : Fin n → ZMod 2) (nonzero : target ≠ 0) (rows : Fin k → Fin n → ZMod 2) (coefficients : Fin k → ZMod 2) (represents : ∑ i : Fin k, coefficients i • rows i = target) : Circuit.relativeGateComplexity interpretation (fun (input : Fin n → ZMod 2) (x : Fin 1) => target ⬝ᵥ input) (forms rows) ≤ ↑(weight coefficients - 1)

A nonzero represented linear target has an XOR implementation with one fewer gates than the number of nonzero representation coefficients.

theorem Algebraic.ConditionalComplexity.Linear.relativeGateComplexity_eq_min_weight {σ : Signature} {n k : ℕ} (interpretation : Interpretation σ (ZMod 2)) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ 2) (addition : Circuit σ 2 1) (addition_size : addition.size = 1) (addition_eval : ∀ (input : Fin 2 → ZMod 2), addition.eval interpretation input 0 = input 0 + input 1) (target : Fin n → ZMod 2) (nonzero : target ≠ 0) (rows : Fin k → Fin n → ZMod 2) : Circuit.relativeGateComplexity interpretation (fun (input : Fin n → ZMod 2) (x : Fin 1) => target ⬝ᵥ input) (forms rows) = ⨅ (coefficients : Fin k → ZMod 2), ⨅ (_ : ∑ i : Fin k, coefficients i • rows i = target), ↑(weight coefficients - 1)

Even nonlinear binary gates cannot beat the sparsest linear representation, and a one-gate XOR operation attains it.

theorem Algebraic.ConditionalComplexity.Linear.weight_append {n k : ℕ} (left : Fin n → ZMod 2) (right : Fin k → ZMod 2) : weight (Fin.append left right) = weight left + weight right

Hamming weight separates across the original-input and helper blocks.

theorem Algebraic.ConditionalComplexity.Linear.conditionalGateComplexity_eq_min_weight {σ : Signature} {n k : ℕ} (interpretation : Interpretation σ (ZMod 2)) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ 2) (addition : Circuit σ 2 1) (addition_size : addition.size = 1) (addition_eval : ∀ (input : Fin 2 → ZMod 2), addition.eval interpretation input 0 = input 0 + input 1) (target : Fin n → ZMod 2) (nonzero : target ≠ 0) (supplied : Fin k → Fin n → ZMod 2) : Circuit.conditionalGateComplexity interpretation (fun (input : Fin n → ZMod 2) (x : Fin 1) => target ⬝ᵥ input) (forms supplied) = ⨅ (coefficients : Fin k → ZMod 2), ↑(weight coefficients + weight (target + ∑ j : Fin k, coefficients j • supplied j) - 1)

Exact conditional complexity of a nonzero linear form. The infimum is over a finite nonempty set, so it is a minimum. The basis may contain any other unary or binary operations, including nonlinear ones.