Semantic recovery of cubic ANF coefficients

Quadratic semantic recovery is already provided by pairPolarMap. The quartic slice proof also needs the three-variable polarization identity. The only finite certificate here is the fixed subset identity on three indices; it contains no circuit data.

noncomputable def UnrestrictedBooleanMul.N4.triplePolarMap (i j k : Fin 8) : ANF 8 →ₗ[F₂] F₂

The third finite difference at zero in three coordinate directions.

Equations

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

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

Extract the coefficient supported on the specified three variables.

Equations

• UnrestrictedBooleanMul.N4.tripleCoeffMap i j k = { toFun := fun (p : UnrestrictedBooleanMul.ANF 8) => p.coeff { vars := {i, j, k} }, map_add' := ⋯, map_smul' := ⋯ }

theorem UnrestrictedBooleanMul.N4.subset_triple_polar_identity (s : Finset (Fin 8)) (i j k : Fin 8) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : ((((((((if s ⊆ ∅ then 1 else 0) + if s ⊆ {i} then 1 else 0) + if s ⊆ {j} then 1 else 0) + if s ⊆ {k} then 1 else 0) + if s ⊆ {i, j} then 1 else 0) + if s ⊆ {i, k} then 1 else 0) + if s ⊆ {j, k} then 1 else 0) + if s ⊆ {i, j, k} then 1 else 0) = if s = {i, j, k} then 1 else 0

Möbius polarization on a three-element Boolean cube.

theorem UnrestrictedBooleanMul.N4.triplePolarMap_eq_tripleCoeffMap (i j k : Fin 8) (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : triplePolarMap i j k = tripleCoeffMap i j k

theorem UnrestrictedBooleanMul.N4.anfThreeProjection_congr_of_eval_eq {p q : ANF 8} (h : ∀ (x : Fin 8 → F₂), eval p x = eval q x) : anfThreeProjection p = anfThreeProjection q

Equality of Boolean functions determines their homogeneous cubic projection.