Quadratic-circuit boundary

This file isolates the exact algebraic content needed from the standard quadratic-circuit flattening theorem. Everything after the definition of QuadraticFlattenable is internal: target computation is pushed through the quadratic coefficient projection, and the eight-form Hankel obstruction then rules out a flattening with eight products.

def UnrestrictedBooleanMul.N4.projectedGateSpan (C : Circuit 8 8) : Submodule F₂ TwoForm

The span of the quadratic projections of the eight gate outputs.

Equations

• UnrestrictedBooleanMul.N4.projectedGateSpan C = Submodule.span UnrestrictedBooleanMul.F₂ (Set.range fun (i : Fin 8) => UnrestrictedBooleanMul.N4.anfTwoProjection (C.gate i))

theorem UnrestrictedBooleanMul.N4.targetTwoSpace_le_projectedGateSpan (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : targetTwoSpace ≤ projectedGateSpan C

Computing all seven multiplication coordinates forces their alternating two-form target space into the span of the projected gate outputs.

def UnrestrictedBooleanMul.N4.QuadraticFlattenable (C : Circuit 8 8) : Prop

A semantic quadratic flattening certificate: the projected span of the original gates has a generating family of eight decomposable two-forms.

The classical Boyar--Find equivalence says that a circuit all of whose gates have degree at most two has such a certificate. Naming the certificate keeps that transformation boundary explicit for the axiom audit.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.flattenGenerator (C : Circuit 8 8) (i : Fin 8) : TwoForm

Retain a gate projection when it is decomposable, and otherwise return zero.

Equations

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

theorem UnrestrictedBooleanMul.N4.flattenGenerator_decomposable (C : Circuit 8 8) (i : Fin 8) : IsDecomposableTwo (flattenGenerator C i)

theorem UnrestrictedBooleanMul.N4.projection_mem_of_mem_wire (C : Circuit 8 8) (j : ℕ) (S : Submodule F₂ TwoForm) (hprev : ∀ (i : Fin 8), ↑i < j → anfTwoProjection (C.gate i) ∈ S) {p : ANF 8} (hp : p ∈ wireSpace C.gate j) : anfTwoProjection p ∈ S

theorem UnrestrictedBooleanMul.N4.gate_projection_alternative (C : Circuit 8 8) (hall : ∀ (i : Fin 8), C.gate i ∈ quadraticANFSpace 8) (i : Fin 8) : anfTwoProjection (C.gate i) ∈ Submodule.span F₂ {anfTwoProjection (C.left i), anfTwoProjection (C.right i)} ∨ IsDecomposableTwo (anfTwoProjection (C.gate i))

theorem UnrestrictedBooleanMul.N4.projected_gate_mem_flatten_span (C : Circuit 8 8) (hall : ∀ (i : Fin 8), C.gate i ∈ quadraticANFSpace 8) (i : Fin 8) : anfTwoProjection (C.gate i) ∈ decomposableTwoSpan (flattenGenerator C)

theorem UnrestrictedBooleanMul.N4.quadratic_flattenable_of_all_gates_quadratic (C : Circuit 8 8) (hall : ∀ (i : Fin 8), C.gate i ∈ quadraticANFSpace 8) : QuadraticFlattenable C

theorem UnrestrictedBooleanMul.N4.no_quadratic_flattening_of_computes (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : ¬QuadraticFlattenable C

theorem UnrestrictedBooleanMul.N4.normalized_seed_high {C : Circuit 8 8} (hNorm : NormalizedEight C) : SeedHighNonzero C

The normalized seed has a nonzero degree-at-least-three component.