N3Certificate for unrestricted Boolean polynomial multiplication

@[reducible, inline]

abbrev UnrestrictedBooleanMul.N3Certificate.F2 : Type

The two-element coefficient field used by the scalar certificates.

Equations

• UnrestrictedBooleanMul.N3Certificate.F2 = ZMod 2

theorem UnrestrictedBooleanMul.N3Certificate.mul_self_f2 (x : F2) : x * x = x

theorem UnrestrictedBooleanMul.N3Certificate.pow_two_f2 (x : F2) : x ^ 2 = x

theorem UnrestrictedBooleanMul.N3Certificate.two_eq_zero_f2 : 2 = 0

theorem UnrestrictedBooleanMul.N3Certificate.three_eq_one_f2 : 3 = 1

theorem UnrestrictedBooleanMul.N3Certificate.four_eq_zero_f2 : 4 = 0

theorem UnrestrictedBooleanMul.N3Certificate.six_eq_zero_f2 : 6 = 0

theorem UnrestrictedBooleanMul.N3Certificate.eight_eq_zero_f2 : 8 = 0

def UnrestrictedBooleanMul.N3Certificate.ab (a b : Fin 10 → F2) (i j : Fin 10) : F2

A bilinear coordinate product from two rational-basis coefficient vectors.

Equations

• UnrestrictedBooleanMul.N3Certificate.ab a b i j = a i * b j

def UnrestrictedBooleanMul.N3Certificate.c3 (a b : Fin 10 → F2) : F2

The product coefficient at the squarefree monomial {0, 1, 4}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.c20 (a b : Fin 10 → F2) : F2

The product coefficient at the squarefree monomial {0, 4, 5}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.c25 (a b : Fin 10 → F2) : F2

The product coefficient at the squarefree monomial {0, 1}.

Equations

• UnrestrictedBooleanMul.N3Certificate.c25 a b = UnrestrictedBooleanMul.N3Certificate.ab a b 1 2 + UnrestrictedBooleanMul.N3Certificate.ab a b 2 1

def UnrestrictedBooleanMul.N3Certificate.c30 (a b : Fin 10 → F2) : F2

The product coefficient at the squarefree monomial {4, 5}.

Equations

• UnrestrictedBooleanMul.N3Certificate.c30 a b = UnrestrictedBooleanMul.N3Certificate.ab a b 5 6 + UnrestrictedBooleanMul.N3Certificate.ab a b 6 5

def UnrestrictedBooleanMul.N3Certificate.c31 (a b : Fin 10 → F2) : F2

Sum of product coefficients at {0, 4} and {1, 3}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.c32 (a b : Fin 10 → F2) : F2

Sum of product coefficients at {0, 5} and {1, 4}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.c34 (a b : Fin 10 → F2) : F2

Sum of product coefficients at {1, 5} and {2, 4}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.g0 (a b : Fin 10 → F2) : F2

The first target-coordinate obstruction, detected at {0, 4} and {0, 5}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.g1 (a b : Fin 10 → F2) : F2

The second target-coordinate obstruction, detected at {0, 5} and {1, 5}.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q00 (a b : Fin 10 → F2) : F2

Multiplier of c3 in the scalar certificate for g0.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q01 (a b : Fin 10 → F2) : F2

Multiplier of c25 in the scalar certificate for g0.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q02 (a b : Fin 10 → F2) : F2

Multiplier of c31 in the scalar certificate for g0.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q03 (a b : Fin 10 → F2) : F2

Multiplier of c32 in the scalar certificate for g0.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q10 (a b : Fin 10 → F2) : F2

Multiplier of c20 in the scalar certificate for g1.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q11 (a b : Fin 10 → F2) : F2

Multiplier of c30 in the scalar certificate for g1.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q12 (a b : Fin 10 → F2) : F2

Multiplier of c32 in the scalar certificate for g1.

Equations

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

def UnrestrictedBooleanMul.N3Certificate.q13 (a b : Fin 10 → F2) : F2

Multiplier of c34 in the scalar certificate for g1.

Equations

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

theorem UnrestrictedBooleanMul.N3Certificate.identity0 (a b : Fin 10 → F2) : g0 a b = q00 a b * c3 a b + q01 a b * c25 a b + q02 a b * c31 a b + q03 a b * c32 a b

theorem UnrestrictedBooleanMul.N3Certificate.identity1 (a b : Fin 10 → F2) : g1 a b = q10 a b * c20 a b + q11 a b * c30 a b + q12 a b * c32 a b + q13 a b * c34 a b

theorem UnrestrictedBooleanMul.N3Certificate.cert0 (a b : Fin 10 → F2) (h3 : c3 a b = 0) (h25 : c25 a b = 0) (h31 : c31 a b = 0) (h32 : c32 a b = 0) : g0 a b = 0

theorem UnrestrictedBooleanMul.N3Certificate.cert1 (a b : Fin 10 → F2) (h20 : c20 a b = 0) (h30 : c30 a b = 0) (h32 : c32 a b = 0) (h34 : c34 a b = 0) : g1 a b = 0