Unrestricted XOR--AND circuits

Free XORs are represented by submodule spans. At gate j, both factors must belong to the affine span enlarged by the outputs of gates with index below j. This semantic presentation is equivalent to storing coefficient masks, but makes the unrestricted nature of nonlinear feedback explicit.

def UnrestrictedBooleanMul.prefixGates {m r : ℕ} (g : Fin r → ANF m) (j : ℕ) : Set (ANF m)

Outputs of gates whose index is strictly before j.

Equations

• UnrestrictedBooleanMul.prefixGates g j = {p : UnrestrictedBooleanMul.ANF m | ∃ (i : Fin r), ↑i < j ∧ g i = p}

noncomputable def UnrestrictedBooleanMul.wireSpace {m r : ℕ} (g : Fin r → ANF m) (j : ℕ) : Submodule F₂ (ANF m)

The functions available for free immediately before gate j.

Equations

• UnrestrictedBooleanMul.wireSpace g j = UnrestrictedBooleanMul.affine m ⊔ Submodule.span UnrestrictedBooleanMul.F₂ (UnrestrictedBooleanMul.prefixGates g j)

theorem UnrestrictedBooleanMul.affine_le_wireSpace {m r j : ℕ} (g : Fin r → ANF m) : affine m ≤ wireSpace g j

structure UnrestrictedBooleanMul.Circuit (m r : ℕ) : Type

An unrestricted XOR--AND circuit with exactly r AND gates.

• gate : Fin r → ANF m

  The Boolean function produced by each AND gate.

• left : Fin r → ANF m

  The left input function of each AND gate.

• right : Fin r → ANF m

  The right input function of each AND gate.

• left_mem (j : Fin r) : self.left j ∈ wireSpace self.gate ↑j
• right_mem (j : Fin r) : self.right j ∈ wireSpace self.gate ↑j
• gate_eq (j : Fin r) : self.gate j = self.left j * self.right j

noncomputable def UnrestrictedBooleanMul.Circuit.ofAffineProducts {m r : ℕ} (left right : Fin r → ANF m) (left_affine : ∀ (i : Fin r), left i ∈ affine m) (right_affine : ∀ (i : Fin r), right i ∈ affine m) : Circuit m r

A circuit all of whose AND inputs are affine in the original inputs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UnrestrictedBooleanMul.Circuit.ofAffineProducts_gate {m r : ℕ} (left right : Fin r → ANF m) (left_affine : ∀ (i : Fin r), left i ∈ affine m) (right_affine : ∀ (i : Fin r), right i ∈ affine m) (i : Fin r) : (ofAffineProducts left right left_affine right_affine).gate i = left i * right i

noncomputable def UnrestrictedBooleanMul.Circuit.empty (m : ℕ) : Circuit m 0

The circuit with no AND gates.

Equations

• UnrestrictedBooleanMul.Circuit.empty m = UnrestrictedBooleanMul.Circuit.ofAffineProducts (fun (i : Fin 0) => i.elim0) (fun (i : Fin 0) => i.elim0) ⋯ ⋯

noncomputable def UnrestrictedBooleanMul.Circuit.finalWire {m r : ℕ} (C : Circuit m r) : Submodule F₂ (ANF m)

The final free-XOR wire space of a circuit.

Equations

• C.finalWire = UnrestrictedBooleanMul.wireSpace C.gate r

def UnrestrictedBooleanMul.Circuit.Computes {m r o : ℕ} (C : Circuit m r) (target : Fin o → ANF m) : Prop

A circuit computes a vector-valued target when every coordinate is in its final span.

Equations

• C.Computes target = ∀ (i : Fin o), target i ∈ C.finalWire

def UnrestrictedBooleanMul.HasCircuit {m o : ℕ} (target : Fin o → ANF m) (r : ℕ) : Prop

There is an unrestricted circuit with r AND gates computing target.

Equations

• UnrestrictedBooleanMul.HasCircuit target r = Nonempty { C : UnrestrictedBooleanMul.Circuit m r // C.Computes target }

noncomputable def UnrestrictedBooleanMul.multiplicativeComplexity {m o : ℕ} (target : Fin o → ANF m) : ℕ

Unrestricted Boolean multiplicative complexity (zero for an uncomputable target).

Equations

• MC(target) = if h : ∃ (r : ℕ), UnrestrictedBooleanMul.HasCircuit target r then Nat.find h else 0

def UnrestrictedBooleanMul.«termMC(_)» : Lean.ParserDescr

Unrestricted AND-gate complexity, with XOR and constants free.

Equations

• One or more equations did not get rendered due to their size.

theorem UnrestrictedBooleanMul.mc_eq_of_lower_upper {m o r : ℕ} {target : Fin o → ANF m} (upper : HasCircuit target r) (lower : ∀ (s : ℕ), HasCircuit target s → r ≤ s) : MC(target) = r

theorem UnrestrictedBooleanMul.gate_mem_wireSpace {m r : ℕ} (g : Fin r → ANF m) (i : Fin r) {j : ℕ} (hij : ↑i < j) : g i ∈ wireSpace g j

@[simp]

theorem UnrestrictedBooleanMul.gate_mem_finalWire {m r : ℕ} (C : Circuit m r) (i : Fin r) : C.gate i ∈ C.finalWire

theorem UnrestrictedBooleanMul.prefixGates_all {m r : ℕ} (g : Fin r → ANF m) : prefixGates g r = Set.range g

theorem UnrestrictedBooleanMul.Circuit.finalWire_eq {m r : ℕ} (C : Circuit m r) : C.finalWire = affine m ⊔ Submodule.span F₂ (Set.range C.gate)

theorem UnrestrictedBooleanMul.Circuit.map_finalWire_eq_span {m r : ℕ} (C : Circuit m r) {V : Type u_1} [AddCommGroup V] [Module F₂ V] (P : ANF m →ₗ[F₂] V) (killsAffine : affine m ≤ P.ker) : Submodule.map P C.finalWire = Submodule.span F₂ (Set.range fun (i : Fin r) => P (C.gate i))

Mapping a final wire space through a linear map that kills affine functions leaves exactly the span of the mapped AND-gate outputs.

theorem UnrestrictedBooleanMul.circuit_lower_bound_of_projection {m d r : ℕ} (C : Circuit m r) (target : Fin d → ANF m) (P : ANF m →ₗ[F₂] Fin d → F₂) (killsAffine : affine m ≤ P.ker) (mapsTarget : ∀ (i : Fin d), P (target i) = (Pi.basisFun F₂ (Fin d)) i) (computes : C.Computes target) : d ≤ r

Dimension lower bound obtained from any coordinate projection that kills affine functions and sends the targets to the standard basis.

noncomputable def UnrestrictedBooleanMul.targetDimension {m r : ℕ} (C : Circuit m r) (target : Submodule F₂ (ANF m)) (j : ℕ) : ℕ

Target dimension modulo the free affine functions.

Equations

• One or more equations did not get rendered due to their size.