Target witnesses for useful gates

The structural part of the n = 4 argument repeatedly replaces a useful gate output by the unique target-ambient direction in its one-dimensional extension. This file packages that linear-algebra step once. It is entirely independent of the later homogeneous-coordinate calculations.

theorem UnrestrictedBooleanMul.N4.exists_targetWitness_of_useful {m r : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (j : Fin r) (huse : UsefulAt C T j) : ∃ t ∈ targetAmbient m T, t ∉ circuitFlag C ↑j ∧ t ∈ circuitFlag C (↑j + 1)

A useful one-vector extension contains a target-ambient vector which was not present in the preceding state.

theorem UnrestrictedBooleanMul.N4.exists_targetWitness_eq_state_add_gate_of_useful {m r : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (j : Fin r) (huse : UsefulAt C T j) : ∃ (t : ANF m) (v : ANF m), t ∈ targetAmbient m T ∧ t ∉ circuitFlag C ↑j ∧ t ∈ circuitFlag C (↑j + 1) ∧ v ∈ circuitFlag C ↑j ∧ t = v + C.gate j

A useful gate output differs from a new target-ambient direction by a wire already present before the gate. Over F₂ the coefficient of the new gate is forced to be one.

theorem UnrestrictedBooleanMul.N4.circuitFlag_succ_eq_targetWitness {m r : ℕ} (C : Circuit m r) (T : Submodule F₂ (ANF m)) (j : Fin r) (huse : UsefulAt C T j) : ∃ t ∈ targetAmbient m T, t ∉ circuitFlag C ↑j ∧ circuitFlag C (↑j + 1) = circuitFlag C ↑j ⊔ F₂ ∙ t

The target witness generates exactly the same next state as the original gate output.