Semantic circuit rewiring

The circuit model stores wires as ANFs and records availability by membership in a wire space. Consequently a basis replacement at one gate can leave all later factor ANFs unchanged: only their membership proofs have to be transported across the equality of wire spaces. This file implements that transport as an actual Circuit, rather than only as a flag-level statement.

def UnrestrictedBooleanMul.N4.updateGate {m r : ℕ} (C : Circuit m r) (j : Fin r) (t : ANF m) : Fin r → ANF m

Replace one gate output in a circuit output sequence.

Equations

• UnrestrictedBooleanMul.N4.updateGate C j t = Function.update C.gate j t

theorem UnrestrictedBooleanMul.N4.wireSpace_updateGate_eq_of_le {m r : ℕ} (C : Circuit m r) (j : Fin r) (t : ANF m) (k : ℕ) (hk : k ≤ ↑j) : wireSpace (updateGate C j t) k = wireSpace C.gate k

theorem UnrestrictedBooleanMul.N4.wireSpace_updateGate_eq_of_lt {m r : ℕ} (C : Circuit m r) (j : Fin r) (t : ANF m) (hstate : wireSpace C.gate (↑j + 1) = wireSpace C.gate ↑j ⊔ F₂ ∙ t) (k : ℕ) (hjk : ↑j < k) (hkr : k ≤ r) : wireSpace (updateGate C j t) k = wireSpace C.gate k

def UnrestrictedBooleanMul.N4.replaceFirstEntryCircuit {m r : ℕ} (C : Circuit m r) (j : Fin r) (u v t : ANF m) (hu : u ∈ affine m) (hv : v ∈ affine m) (ht : t = u * v) (hstate : wireSpace C.gate (↑j + 1) = wireSpace C.gate ↑j ⊔ F₂ ∙ t) : Circuit m r

Replace a first-entry gate by a direct affine product while preserving all later gate functions and the final wire space.

Equations

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

theorem UnrestrictedBooleanMul.N4.replaceFirstEntryCircuit_finalWire {m r : ℕ} (C : Circuit m r) (j : Fin r) (u v t : ANF m) (hu : u ∈ affine m) (hv : v ∈ affine m) (ht : t = u * v) (hstate : wireSpace C.gate (↑j + 1) = wireSpace C.gate ↑j ⊔ F₂ ∙ t) : (replaceFirstEntryCircuit C j u v t hu hv ht hstate).finalWire = C.finalWire

theorem UnrestrictedBooleanMul.N4.replaceFirstEntryCircuit_computes {m r o : ℕ} (C : Circuit m r) (target : Fin o → ANF m) (j : Fin r) (u v t : ANF m) (hu : u ∈ affine m) (hv : v ∈ affine m) (ht : t = u * v) (hstate : wireSpace C.gate (↑j + 1) = wireSpace C.gate ↑j ⊔ F₂ ∙ t) (hC : C.Computes target) : (replaceFirstEntryCircuit C j u v t hu hv ht hstate).Computes target

def UnrestrictedBooleanMul.N4.swapAdjacentFun {r : ℕ} {X : Type u_1} (f : Fin r → X) (a b : Fin r) : Fin r → X

Exchange two entries of a finite sequence.

Equations

• UnrestrictedBooleanMul.N4.swapAdjacentFun f a b i = if i = a then f b else if i = b then f a else f i

theorem UnrestrictedBooleanMul.N4.wireSpace_swapAdjacent_eq_of_le {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) (k : ℕ) (hk : k ≤ ↑a) : wireSpace (swapAdjacentFun C.gate a b) k = wireSpace C.gate k

theorem UnrestrictedBooleanMul.N4.wireSpace_swapAdjacent_at_right {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) : wireSpace (swapAdjacentFun C.gate a b) ↑b = wireSpace C.gate ↑a ⊔ F₂ ∙ C.gate b

theorem UnrestrictedBooleanMul.N4.wireSpace_swapAdjacent_after_pair {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) : wireSpace (swapAdjacentFun C.gate a b) (↑b + 1) = wireSpace C.gate (↑b + 1)

theorem UnrestrictedBooleanMul.N4.wireSpace_swapAdjacent_eq_of_right_lt {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) (k : ℕ) (hbk : ↑b < k) (hkr : k ≤ r) : wireSpace (swapAdjacentFun C.gate a b) k = wireSpace C.gate k

def UnrestrictedBooleanMul.N4.swapAdjacentDirectCircuit {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) (hleft : C.left b ∈ affine m) (hright : C.right b ∈ affine m) : Circuit m r

Commute a gate whose two factors are affine one position toward the front. No earlier gate can depend on it, and after the pair the wire space is unchanged.

Equations

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

theorem UnrestrictedBooleanMul.N4.swapAdjacentDirectCircuit_finalWire {m r : ℕ} (C : Circuit m r) (a b : Fin r) (hab : ↑a + 1 = ↑b) (hleft : C.left b ∈ affine m) (hright : C.right b ∈ affine m) : (swapAdjacentDirectCircuit C a b hab hleft hright).finalWire = C.finalWire

theorem UnrestrictedBooleanMul.N4.swapAdjacentDirectCircuit_computes {m r o : ℕ} (C : Circuit m r) (target : Fin o → ANF m) (a b : Fin r) (hab : ↑a + 1 = ↑b) (hleft : C.left b ∈ affine m) (hright : C.right b ∈ affine m) (hC : C.Computes target) : (swapAdjacentDirectCircuit C a b hab hleft hright).Computes target

theorem UnrestrictedBooleanMul.N4.exists_first_entry_gate {m r : ℕ} (C : Circuit m r) (t : ANF m) (hfinal : t ∈ C.finalWire) (hnotAffine : t ∉ affine m) : ∃ (j : Fin r), t ∈ circuitFlag C (↑j + 1) ∧ t ∉ circuitFlag C ↑j

A non-affine final wire has a first gate at which it enters the flag.

theorem UnrestrictedBooleanMul.N4.linearANF_mem_affine (ell : LinearForm) : linearANF ell ∈ affine 8

theorem UnrestrictedBooleanMul.N4.rationalPlaceANF_direct (theta : Fin 3) : targetANF (rationalPlaceCoeff theta) = linearANF (placeA theta) * linearANF (placeB theta)

theorem UnrestrictedBooleanMul.N4.rationalPlaceANF_not_mem_affine (theta : Fin 3) : targetANF (rationalPlaceCoeff theta) ∉ affine 8

theorem UnrestrictedBooleanMul.N4.rationalPlaceANF_mem_finalWire (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (theta : Fin 3) : targetANF (rationalPlaceCoeff theta) ∈ C.finalWire

theorem UnrestrictedBooleanMul.N4.exists_move_direct_gate_left {m r : ℕ} (C : Circuit m r) (p j : Fin r) (hpj : ↑p ≤ ↑j) (t : ANF m) (hgate : C.gate j = t) (hleft : C.left j ∈ affine m) (hright : C.right j ∈ affine m) : ∃ (D : Circuit m r), D.finalWire = C.finalWire ∧ D.gate p = t ∧ D.left p ∈ affine m ∧ D.right p ∈ affine m ∧ ∀ (k : Fin r), ↑k < ↑p → D.gate k = C.gate k

Move a direct affine-product gate left to any earlier position by adjacent legal commutations. Gates strictly before the destination are untouched.

theorem UnrestrictedBooleanMul.N4.exists_promote_rational_place (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (p : Fin 8) (theta : Fin 3) (hmissing : targetANF (rationalPlaceCoeff theta) ∉ circuitFlag C ↑p) : ∃ (D : Circuit 8 8), D.Computes (Mul 4) ∧ D.finalWire = C.finalWire ∧ D.gate p = targetANF (rationalPlaceCoeff theta) ∧ D.left p ∈ affine 8 ∧ D.right p ∈ affine 8 ∧ ∀ (k : Fin 8), ↑k < ↑p → D.gate k = C.gate k

Promote a rational target direction which is absent from a chosen prefix to a direct affine-product gate at the end of that prefix. The transformation preserves the final wire space and every earlier gate.