Direct sum of the three rational-place cubic spaces

The manuscript uses

I₀ ⊕ I₁ ⊕ I∞, where Iθ = L ∧ rθ.

The eighteen packed rows below form a left inverse on the six quotient coordinates of each summand. Their correctness is checked only on the 3 × 8 coordinate vectors and extended to arbitrary linear forms by linearity. This compact certificate replaces repeated coordinate chases in the quartic and annihilator arguments.

def UnrestrictedBooleanMul.N4.upperTriple : Fin 56 → Fin 8 × Fin 8 × Fin 8

The 56 strictly increasing triples of eight coordinate indices.

Equations

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

def UnrestrictedBooleanMul.N4.cubicDirectRecoverTable : Fin 18 → ℕ

Packed covectors recovering six quotient coordinates at each rational place.

Equations

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

def UnrestrictedBooleanMul.N4.threeFormCoordinate (i j k : Fin 8) : ThreeForm →ₗ[F₂] F₂

Extract one coordinate from a three-form coordinate array.

Equations

• UnrestrictedBooleanMul.N4.threeFormCoordinate i j k = { toFun := fun (h : UnrestrictedBooleanMul.N4.ThreeForm) => h i j k, map_add' := ⋯, map_smul' := ⋯ }

def UnrestrictedBooleanMul.N4.cubicDirectRecover (r : Fin 18) : ThreeForm →ₗ[F₂] F₂

The linear functional encoded by one row of the cubic recovery table.

Equations

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

def UnrestrictedBooleanMul.N4.cubicPlaceLinear (theta : Fin 3) : LinearForm →ₗ[F₂] ThreeForm

Wedge a linear form with the two-form of one rational place.

Equations

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

def UnrestrictedBooleanMul.N4.rationalCubicDirectSum (M : Fin 3 → LinearForm) : ThreeForm

Sum of the cubic contributions at the three rational places.

Equations

• UnrestrictedBooleanMul.N4.rationalCubicDirectSum M = ∑ theta : Fin 3, (UnrestrictedBooleanMul.N4.cubicPlaceLinear theta) (M theta)

def UnrestrictedBooleanMul.N4.cubicDirectQuotient (M : Fin 3 → LinearForm) : Fin 18 → F₂

Six quotient coordinates for each of P₀, P₁, and P∞.

Equations

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

def UnrestrictedBooleanMul.N4.singleCubicInput (theta : Fin 3) (j : Fin 8) : Fin 3 → LinearForm

A coordinate vector at one rational place, with zero inputs at the other places.

Equations

• UnrestrictedBooleanMul.N4.singleCubicInput theta j phi = if phi = theta then UnrestrictedBooleanMul.N4.coordinateLinear j else 0

theorem UnrestrictedBooleanMul.N4.cubicDirectRecover_basis_check (r : Fin 18) (theta : Fin 3) (j : Fin 8) : (cubicDirectRecover r) (vectorWedgeTwo (coordinateLinear j) (rationalPlaceTwo theta)) = cubicDirectQuotient (singleCubicInput theta j) r

theorem UnrestrictedBooleanMul.N4.cubicDirectRecover_sum (M : Fin 3 → LinearForm) (r : Fin 18) : (cubicDirectRecover r) (rationalCubicDirectSum M) = cubicDirectQuotient M r

theorem UnrestrictedBooleanMul.N4.neg_eq_self_f2 (x : F₂) : -x = x

theorem UnrestrictedBooleanMul.N4.rationalCubicDirectSum_kernel (M : Fin 3 → LinearForm) (h : rationalCubicDirectSum M = 0) (theta : Fin 3) : ∃ (a : F₂) (b : F₂), M theta = a • placeA theta + b • placeB theta

The three rational-place cubic spaces are a direct sum modulo their two-dimensional support kernels.