Circuit flags and the defect ledger

The definitions in this file isolate the two components of a circuit flag: the target dimension and the complementary defect dimension. The main identity is the reusable form of the manuscript's ledger

number of nonredundant gates = target rank + defect rank.

noncomputable def UnrestrictedBooleanMul.N4.targetAmbient (m : ℕ) (T : Submodule F₂ (ANF m)) : Submodule F₂ (ANF m)

The target ambient space Aff + T.

Equations

• UnrestrictedBooleanMul.N4.targetAmbient m T = UnrestrictedBooleanMul.affine m ⊔ T

noncomputable def UnrestrictedBooleanMul.N4.flagTargetRank {m : ℕ} (V T : Submodule F₂ (ANF m)) : ℕ

Target dimension of a wire space, measured modulo affine functions.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.flagDefectRank {m : ℕ} (V T : Submodule F₂ (ANF m)) : ℕ

Defect dimension: directions in the wire space outside Aff + T.

Equations

• UnrestrictedBooleanMul.N4.flagDefectRank V T = Module.finrank UnrestrictedBooleanMul.F₂ ↥V - Module.finrank UnrestrictedBooleanMul.F₂ ↥(V ⊓ UnrestrictedBooleanMul.N4.targetAmbient m T)

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

The wire-space flag associated with a semantic circuit.

Equations

• UnrestrictedBooleanMul.N4.circuitFlag C j = UnrestrictedBooleanMul.wireSpace C.gate j

def UnrestrictedBooleanMul.N4.NonredundantAt {m r : ℕ} (C : Circuit m r) (j : Fin r) : Prop

A gate is nonredundant when its output is not already in the preceding wire space. Minimal circuits have this property at every gate.

Equations

• UnrestrictedBooleanMul.N4.NonredundantAt C j = (C.gate j ∉ UnrestrictedBooleanMul.N4.circuitFlag C ↑j)

def UnrestrictedBooleanMul.N4.UsefulAt {m r : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (j : Fin r) : Prop

A gate is useful when adjoining it raises the target rank.

Equations

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

theorem UnrestrictedBooleanMul.N4.prefixGates_mono {m r j k : ℕ} {g : Fin r → ANF m} (hjk : j ≤ k) : prefixGates g j ⊆ prefixGates g k

theorem UnrestrictedBooleanMul.N4.wireSpace_mono {m r j k : ℕ} {g : Fin r → ANF m} (hjk : j ≤ k) : wireSpace g j ≤ wireSpace g k

@[simp]

theorem UnrestrictedBooleanMul.N4.prefixGates_zero {m r : ℕ} (g : Fin r → ANF m) : prefixGates g 0 = ∅

@[simp]

theorem UnrestrictedBooleanMul.N4.wireSpace_zero {m r : ℕ} (g : Fin r → ANF m) : wireSpace g 0 = affine m

theorem UnrestrictedBooleanMul.N4.prefixGates_succ {m r j : ℕ} (g : Fin r → ANF m) (hj : j < r) : prefixGates g (j + 1) = prefixGates g j ∪ {g ⟨j, hj⟩}

theorem UnrestrictedBooleanMul.N4.wireSpace_succ {m r j : ℕ} (g : Fin r → ANF m) (hj : j < r) : wireSpace g (j + 1) = wireSpace g j ⊔ F₂ ∙ g ⟨j, hj⟩

Each step of the circuit flag adjoins exactly the span of the new gate output (possibly redundantly).

theorem UnrestrictedBooleanMul.N4.finrank_inf_extension_le_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (A W : Submodule K V) (x : V) : Module.finrank K ↥((A ⊔ K ∙ x) ⊓ W) ≤ Module.finrank K ↥(A ⊓ W) + 1

Intersecting a one-vector extension with any fixed ambient subspace can raise dimension by at most one. This is the linear-algebra core of “one gate buys at most one target dimension.”

theorem UnrestrictedBooleanMul.N4.flagTargetRank_step_le_one {m r : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (j : Fin r) : flagTargetRank (circuitFlag C (↑j + 1)) T ≤ flagTargetRank (circuitFlag C ↑j) T + 1

theorem UnrestrictedBooleanMul.N4.flag_rank_ledger {m : ℕ} {V T : Submodule F₂ (ANF m)} (hAff : affine m ≤ V) : Module.finrank F₂ ↥V - Module.finrank F₂ ↥(affine m) = flagTargetRank V T + flagDefectRank V T

The exact short-exact-sequence ledger for any wire space containing the affine inputs.

theorem UnrestrictedBooleanMul.N4.circuitFlag_finrank {m r j : ℕ} (C : Circuit m r) (hj : j ≤ r) (hnr : ∀ (i : Fin r), ↑i < j → NonredundantAt C i) : Module.finrank F₂ ↥(circuitFlag C j) = Module.finrank F₂ ↥(affine m) + j

A nonredundant prefix of j AND gates has quotient dimension exactly j modulo affine functions.

theorem UnrestrictedBooleanMul.N4.circuit_flag_defect_count {m r j : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (hj : j ≤ r) (hnr : ∀ (i : Fin r), ↑i < j → NonredundantAt C i) : j = flagTargetRank (circuitFlag C j) T + flagDefectRank (circuitFlag C j) T

The manuscript identity j = t(V_j) + e(V_j) for a nonredundant circuit prefix.