The four-term target and its ambient dimension

This file supplies concrete coordinate projections for the nine affine and seven target directions. They make the flag ledger numerically usable while keeping all proofs in ordinary linear algebra over F₂.

noncomputable def UnrestrictedBooleanMul.N4.targetANFLinear : TargetCoeff →ₗ[F₂] ANF 8

The linear map from target coefficient vectors to product ANFs.

Equations

• UnrestrictedBooleanMul.N4.targetANFLinear = { toFun := UnrestrictedBooleanMul.N4.targetANF, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem UnrestrictedBooleanMul.N4.targetANFLinear_apply (c : TargetCoeff) : targetANFLinear c = targetANF c

def UnrestrictedBooleanMul.N4.fourTargetAnchor : Fin 7 → Monomial 8

Seven quadratic monomials, one private to each coordinate of Mul 4.

Equations

• UnrestrictedBooleanMul.N4.fourTargetAnchor = ![{ vars := {0, 4} }, { vars := {0, 5} }, { vars := {0, 6} }, { vars := {0, 7} }, { vars := {1, 7} }, { vars := {2, 7} }, { vars := {3, 7} }]

def UnrestrictedBooleanMul.N4.fourTargetProjection : ANF 8 →ₗ[F₂] Fin 7 → F₂

Extract seven anchor coefficients recovering a four-term product target.

Equations

• UnrestrictedBooleanMul.N4.fourTargetProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.N4.fourTargetAnchor

theorem UnrestrictedBooleanMul.N4.fourTargetAnchor_degree (i : Fin 7) : (fourTargetAnchor i).vars.card = 2

theorem UnrestrictedBooleanMul.N4.fourTargetProjection_kills_affine : affine 8 ≤ fourTargetProjection.ker

theorem UnrestrictedBooleanMul.N4.fourTargetProjection_Mul (i : Fin 7) : fourTargetProjection (Mul 4 i) = (Pi.basisFun F₂ (Fin 7)) i

theorem UnrestrictedBooleanMul.N4.fourTargetProjection_targetANF (c : TargetCoeff) : fourTargetProjection (targetANF c) = c

theorem UnrestrictedBooleanMul.N4.targetANF_injective : Function.Injective targetANF

theorem UnrestrictedBooleanMul.N4.targetANF_mem_mulTarget (c : TargetCoeff) : targetANF c ∈ mulTarget 4

theorem UnrestrictedBooleanMul.N4.mulFour_linearIndependent : LinearIndependent F₂ (Mul 4)

theorem UnrestrictedBooleanMul.N4.mulTarget_four_finrank : Module.finrank F₂ ↥(mulTarget 4) = 7

noncomputable def UnrestrictedBooleanMul.N4.affineFourBasis : Fin 9 → ANF 8

A concrete basis for the affine input space on eight variables.

Equations

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

def UnrestrictedBooleanMul.N4.affineFourAnchor : Fin 9 → Monomial 8

The constant and eight singleton monomials anchoring affine coordinates.

Equations

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

def UnrestrictedBooleanMul.N4.affineFourProjection : ANF 8 →ₗ[F₂] Fin 9 → F₂

Extract the constant and eight linear coefficients of an ANF.

Equations

• UnrestrictedBooleanMul.N4.affineFourProjection = UnrestrictedBooleanMul.coefficientProjection UnrestrictedBooleanMul.N4.affineFourAnchor

theorem UnrestrictedBooleanMul.N4.affineFourProjection_basis (i : Fin 9) : affineFourProjection (affineFourBasis i) = (Pi.basisFun F₂ (Fin 9)) i

theorem UnrestrictedBooleanMul.N4.affineFourBasis_linearIndependent : LinearIndependent F₂ affineFourBasis

theorem UnrestrictedBooleanMul.N4.affine_eight_eq_span : affine 8 = Submodule.span F₂ (Set.range affineFourBasis)

theorem UnrestrictedBooleanMul.N4.affine_eight_finrank : Module.finrank F₂ ↥(affine 8) = 9

theorem UnrestrictedBooleanMul.N4.affine_disjoint_mulTarget_four : Disjoint (affine 8) (mulTarget 4)

The affine and target spaces meet trivially. The proof projects to the seven private quadratic coefficients, so it is both symbolic and inexpensive.

theorem UnrestrictedBooleanMul.N4.targetAmbient_four_finrank : Module.finrank F₂ ↥(targetAmbient 8 (mulTarget 4)) = 16

theorem UnrestrictedBooleanMul.N4.final_target_rank_four (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : flagTargetRank C.finalWire (mulTarget 4) = 7

theorem UnrestrictedBooleanMul.N4.finalWire_finrank_le_affine_add {m r : ℕ} (C : Circuit m r) : Module.finrank F₂ ↥C.finalWire ≤ Module.finrank F₂ ↥(affine m) + r

A circuit with r gates has final dimension at most affine dimension plus r, whether or not some gate is redundant.

theorem UnrestrictedBooleanMul.N4.eight_gate_defect_le_one (C : Circuit 8 8) (hC : C.Computes (Mul 4)) : flagDefectRank C.finalWire (mulTarget 4) ≤ 1

The defect budget of any hypothetical eight-gate circuit for Mul 4 is at most one; no nonredundancy assumption is needed.

theorem UnrestrictedBooleanMul.N4.eight_gate_defect_is_one (C : Circuit 8 8) (hC : C.Computes (Mul 4)) (hnr : ∀ (i : Fin 8), NonredundantAt C i) : flagDefectRank C.finalWire (mulTarget 4) = 1