Algebraic normal form for the first suffix gate

Immediately before gate five the state is Aff + R + ⟨g⟩. Idempotence reduces the product of any two wires in this state, modulo the state itself, to one of two forms: a low--low product, or a product with exactly one g-containing factor. This is the non-combinatorial normalization used in both the quartic and cubic feedback arguments.

def UnrestrictedBooleanMul.N4.IsLowLowProduct (f : ANF 8) : Prop

A product of two ANFs in the affine-plus-rational-target space.

Equations

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

def UnrestrictedBooleanMul.N4.IsSeedUsingProduct (g f : ANF 8) : Prop

A product whose first input is the seed plus a low term and whose second input is low.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.wireSpace_four_eq {C : Circuit 8 8} (h : NormalizedEight C) : circuitFlag C 4 = rationalLowSpace ⊔ F₂ ∙ C.gate 3

theorem UnrestrictedBooleanMul.N4.exists_low_add_seed_of_mem_four {C : Circuit 8 8} (h : NormalizedEight C) {w : ANF 8} (hw : w ∈ circuitFlag C 4) : ∃ (p : ANF 8) (e : F₂), p ∈ rationalLowSpace ∧ w = p + e • C.gate 3

Every wire in the first post-seed state has a low part and one Boolean coefficient of the seed.

theorem UnrestrictedBooleanMul.N4.normalize_seed_state_product {C : Circuit 8 8} (h : NormalizedEight C) {l r : ANF 8} (hl : l ∈ circuitFlag C 4) (hr : r ∈ circuitFlag C 4) : ∃ (f : ANF 8), ∃ s ∈ circuitFlag C 4, l * r = s + f ∧ (IsLowLowProduct f ∨ IsSeedUsingProduct (C.gate 3) f)

Product normalization modulo Aff + R + ⟨g⟩.

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

A new target at the fifth gate, represented modulo the fourth-gate flag by a seed child.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.usefulSeedChildData {C : Circuit 8 8} (h : NormalizedEight C) : UsefulSeedChildData C

Circuit-level gate five is reduced to the two algebraic child types.