Cubic first-feedback slice exclusion

This file formalizes the Q/L comparison in the manuscript's exclusion of a seed-using first feedback. The seed has already been normalized to M (z + E₀) modulo Aff + R. On an active (x,y) slice both seed factors are affine in the six complementary variables, so the quadratic equation is independent of the corner. The three active corners then force two independent target differences into a space of dimension at most one, or into one of the two disjoint support planes.

The proof is exterior-linear and does not enumerate circuits or Boolean functions.

noncomputable def UnrestrictedBooleanMul.N4.sliceLinearFactorModel (ell : LinearForm) (x y : F₂) : ANF 8

Restrict a linear factor to fixed values of the two anchor inputs.

Equations

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

noncomputable def UnrestrictedBooleanMul.N4.sliceCubicSeedFullModel (anchorLinear companionLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : ANF 8

The sliced cubic seed, including its affine and rational-target correction.

Equations

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

theorem UnrestrictedBooleanMul.N4.eval_sliceLinearFactorModel (ell : LinearForm) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceLinearFactorModel ell x y) (sliceAssignment x y z) = eval (linearANF ell) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.eval_sliceCubicSeedFullModel_eq_normalized (anchorLinear companionLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) (z : Fin 6 → F₂) : eval (sliceCubicSeedFullModel anchorLinear companionLinear correctionConst correctionLinear correctionCoeff x y) (sliceAssignment x y z) = eval (linearANF anchorLinear * (linearANF companionLinear + rationalANF (rationalSingleton 0)) + representedLowFactor correctionConst correctionLinear correctionCoeff) (sliceAssignment x y z)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceLinearFactorModel (ell : LinearForm) (x y : F₂) : AnchorsIndependent (sliceLinearFactorModel ell x y)

theorem UnrestrictedBooleanMul.N4.anchorsIndependent_sliceCubicSeedFullModel (anchorLinear companionLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : AnchorsIndependent (sliceCubicSeedFullModel anchorLinear companionLinear correctionConst correctionLinear correctionCoeff x y)

@[simp]

theorem UnrestrictedBooleanMul.N4.anfTwoProjection_sliceCubicSeedFullModel (anchorLinear companionLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfTwoProjection (sliceCubicSeedFullModel anchorLinear companionLinear correctionConst correctionLinear correctionCoeff x y) = vectorWedge (sliceComplementLinear anchorLinear) (sliceComplementLinear companionLinear) + correctionCoeff 1 • sliceQuadraticA + correctionCoeff 2 • sliceInfinityQuadratic

@[simp]

theorem UnrestrictedBooleanMul.N4.anfLinearProjection_sliceCubicSeedFullModel (anchorLinear companionLinear : LinearForm) (correctionConst : F₂) (correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂) (x y : F₂) : anfLinearProjection (sliceCubicSeedFullModel anchorLinear companionLinear correctionConst correctionLinear correctionCoeff x y) = sliceProductLinear (sliceAnchorValue anchorLinear x y) (sliceAnchorValue companionLinear x y + x * y) (sliceComplementLinear anchorLinear) (sliceComplementLinear companionLinear) (sliceComplementLinear correctionLinear) (correctionCoeff 1) x y

def UnrestrictedBooleanMul.N4.InLinearPair (m n w : LinearForm) : Prop

The third linear form belongs to the span of the first two.

Equations

• UnrestrictedBooleanMul.N4.InLinearPair m n w = ∃ (a : UnrestrictedBooleanMul.F₂) (b : UnrestrictedBooleanMul.F₂), w = a • m + b • n

theorem UnrestrictedBooleanMul.N4.vectorWedge_linear_combinations (a b c d : F₂) (m n : LinearForm) : vectorWedge (a • m + b • n) (c • m + d • n) = (a * d + b * c) • vectorWedge m n

theorem UnrestrictedBooleanMul.N4.vectorWedge_eq_zero_of_pair {m n u v : LinearForm} (hmn : vectorWedge m n = 0) (hu : InLinearPair m n u) (hv : InLinearPair m n v) : vectorWedge u v = 0

theorem UnrestrictedBooleanMul.N4.vectorWedge_sliceU_sliceV_ne_zero : vectorWedge sliceU sliceV ≠ 0

theorem UnrestrictedBooleanMul.N4.sliceQuadraticB_ne_zero : sliceQuadraticB ≠ 0

theorem UnrestrictedBooleanMul.N4.no_cubic_seed_three_active_slices {delta rho sigma lambdaOne lambdaInfinity : F₂} {m n base targetBase : LinearForm} (hcorners : ExactlyThreeActiveCorners delta rho sigma) (hquad : vectorWedge m n + lambdaOne • sliceQuadraticA + lambdaInfinity • sliceInfinityQuadratic = 0) (mu nu : F₂ → F₂ → F₂) (hlinear : ∀ (x y : F₂), feedbackCorner delta rho sigma x y = 1 → sliceProductLinear (mu x y) (nu x y) m n base lambdaOne x y = targetBase + y • sliceU + x • sliceV) : False

Algebraic Q/L exclusion for the three active corners.

theorem UnrestrictedBooleanMul.N4.no_cubic_seed_three_active_slice_functions {delta rho sigma : F₂} {anchorLinear companionLinear correctionLinear targetLinear : LinearForm} {correctionConst targetConst eps : F₂} {correctionCoeff : Fin 3 → F₂} (hcorners : ExactlyThreeActiveCorners delta rho sigma) (hslice : ∀ (x y : F₂), feedbackCorner delta rho sigma x y = 1 → ∀ (z : Fin 6 → F₂), eval (sliceCubicSeedFullModel anchorLinear companionLinear correctionConst correctionLinear correctionCoeff x y) (sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z)) : False

Semantic wrapper for the algebraic Q/L exclusion. It converts an equality of the three active six-variable slice functions into their quadratic and linear homogeneous equations; no truth-table enumeration is used.

theorem UnrestrictedBooleanMul.N4.no_zeroAnchored_cubic_feedback_target {g correction factor target : ANF 8} {targetConst eps delta rho sigma : F₂} {targetLinear : LinearForm} (hseed : ZeroAnchoredCubicSeedForm g) (hcorrection : correction ∈ rationalLowSpace) (htargetEq : target = (g + correction) * factor) (htargetRep : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps)) (hfactorRep : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0)) (hright : target * factor = target) : False

A zero-place feedback cannot use the canonical cubic seed M (z + E₀). The only finite data are the three active anchor corners; all six-variable reasoning is transferred through homogeneous projections.

theorem UnrestrictedBooleanMul.N4.seedUsingCubicClassifiedForm_impossible {g : ANF 8} (hseed : CubicSeedAnchoredForm g) (hfeedback : SeedUsingCubicClassifiedForm g) : False

The complete cubic classification is incompatible with either idempotence identity. The classified place is transported to zero, with the seed and feedback kept at that same indexed place.

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

A new target at the fifth gate represented, modulo the preceding flag, by a low-low product.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.firstUsefulChild_isLowLow {C : Circuit 8 8} (h : NormalizedEight C) : FirstLowLowData C

Circuit-facing endpoint of the first-feedback exclusion: the first useful post-seed gate is necessarily low--low.