Independent truth-table cross-check for the n = 3 lower bound

This module validates the concrete 64-bit encodings used while developing the algebraic proof. Nothing in N3.lean or the final theorem depends on it.

def UnrestrictedBooleanMul.bitF2 (b : Bool) : F₂

Interpret a Boolean bit as an element of the two-element field.

Equations

• UnrestrictedBooleanMul.bitF2 b = if b = true then 1 else 0

def UnrestrictedBooleanMul.f2Bit (x : F₂) : Bool

Convert a field element to its Boolean bit.

Equations

• UnrestrictedBooleanMul.f2Bit x = decide (x = 1)

@[simp]

theorem UnrestrictedBooleanMul.f2Bit_zero : f2Bit 0 = false

@[simp]

theorem UnrestrictedBooleanMul.f2Bit_one : f2Bit 1 = true

@[simp]

theorem UnrestrictedBooleanMul.bitF2_f2Bit (x : F₂) : bitF2 (f2Bit x) = x

@[simp]

theorem UnrestrictedBooleanMul.bitF2_xor (a b : Bool) : bitF2 (a ^^ b) = bitF2 a + bitF2 b

@[simp]

theorem UnrestrictedBooleanMul.bitF2_and (a b : Bool) : bitF2 (a && b) = bitF2 a * bitF2 b

theorem UnrestrictedBooleanMul.bitF2_injective : Function.Injective bitF2

def UnrestrictedBooleanMul.coeffBits {n : ℕ} (c : Fin n → F₂) : BitVec n

Pack a field-valued coefficient vector with coordinate zero as the least significant bit.

Equations

• UnrestrictedBooleanMul.coeffBits c = BitVec.ofFnLE fun (i : Fin n) => UnrestrictedBooleanMul.f2Bit (c i)

theorem UnrestrictedBooleanMul.coeffBits_getLsb {n : ℕ} (c : Fin n → F₂) (i : Fin n) : (coeffBits c).getLsb i = f2Bit (c i)

@[simp]

theorem UnrestrictedBooleanMul.coeffBits_getElem {n : ℕ} (c : Fin n → F₂) (i : ℕ) (h : i < n) : (coeffBits c)[i] = f2Bit (c ⟨i, h⟩)

def UnrestrictedBooleanMul.sel (b : Bool) (x : BitVec 64) : BitVec 64

Select a truth table when the coefficient bit is set, and the zero table otherwise.

Equations

• UnrestrictedBooleanMul.sel b x = if b = true then x else 0

theorem UnrestrictedBooleanMul.bitF2_sel_getLsb (c : F₂) (x : BitVec 64) (q : Fin 64) : bitF2 ((sel (f2Bit c) x).getLsb q) = c * bitF2 (x.getLsb q)

theorem UnrestrictedBooleanMul.bitF2_sel_getElem (c : F₂) (x : BitVec 64) (q : Fin 64) : bitF2 (sel (f2Bit c) x)[q] = c * bitF2 x[q]

@[simp]

theorem UnrestrictedBooleanMul.bitF2_sel_getElemNat (c : F₂) (x : BitVec 64) (i : ℕ) (h : i < 64) : bitF2 (sel (f2Bit c) x)[i] = c * bitF2 x[i]

def UnrestrictedBooleanMul.v0 : BitVec 64

Truth-table column for input variable 0, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v0 = 12297829382473034410#64

def UnrestrictedBooleanMul.v1 : BitVec 64

Truth-table column for input variable 1, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v1 = 14757395258967641292#64

def UnrestrictedBooleanMul.v2 : BitVec 64

Truth-table column for input variable 2, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v2 = 17361641481138401520#64

def UnrestrictedBooleanMul.v3 : BitVec 64

Truth-table column for input variable 3, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v3 = 18374966859414961920#64

def UnrestrictedBooleanMul.v4 : BitVec 64

Truth-table column for input variable 4, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v4 = 18446462603027742720#64

def UnrestrictedBooleanMul.v5 : BitVec 64

Truth-table column for input variable 5, in least-significant-bit assignment order.

Equations

• UnrestrictedBooleanMul.v5 = 18446744069414584320#64

theorem UnrestrictedBooleanMul.bitF2_allOnes_getElem (q : Fin 64) : bitF2 (18446744073709551615#64)[q] = 1

@[simp]

theorem UnrestrictedBooleanMul.bitF2_allOnes_getElemNat (i : ℕ) (h : i < 64) : bitF2 (18446744073709551615#64)[i] = 1

def UnrestrictedBooleanMul.e0 : BitVec 64

Truth table for coefficient 0 of the product of two three-term polynomials.

Equations

• UnrestrictedBooleanMul.e0 = UnrestrictedBooleanMul.v0 &&& UnrestrictedBooleanMul.v3

def UnrestrictedBooleanMul.e1 : BitVec 64

Truth table for coefficient 1 of the product of two three-term polynomials.

Equations

• UnrestrictedBooleanMul.e1 = UnrestrictedBooleanMul.v0 &&& UnrestrictedBooleanMul.v4 ^^^ UnrestrictedBooleanMul.v1 &&& UnrestrictedBooleanMul.v3

def UnrestrictedBooleanMul.e2 : BitVec 64

Truth table for coefficient 2 of the product of two three-term polynomials.

Equations

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

def UnrestrictedBooleanMul.e3 : BitVec 64

Truth table for coefficient 3 of the product of two three-term polynomials.

Equations

• UnrestrictedBooleanMul.e3 = UnrestrictedBooleanMul.v1 &&& UnrestrictedBooleanMul.v5 ^^^ UnrestrictedBooleanMul.v2 &&& UnrestrictedBooleanMul.v4

def UnrestrictedBooleanMul.e4 : BitVec 64

Truth table for coefficient 4 of the product of two three-term polynomials.

Equations

• UnrestrictedBooleanMul.e4 = UnrestrictedBooleanMul.v2 &&& UnrestrictedBooleanMul.v5

def UnrestrictedBooleanMul.tableVar : Fin 6 → BitVec 64

The six input-variable truth tables, in input order.

Equations

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

def UnrestrictedBooleanMul.targetTable : Fin 5 → BitVec 64

Truth tables for the five coefficients of a three-term product.

Equations

• UnrestrictedBooleanMul.targetTable = ![UnrestrictedBooleanMul.e0, UnrestrictedBooleanMul.e1, UnrestrictedBooleanMul.e2, UnrestrictedBooleanMul.e3, UnrestrictedBooleanMul.e4]

def UnrestrictedBooleanMul.assignment (q : Fin 64) : Fin 6 → F₂

The six Boolean input values encoded by a truth-table row.

Equations

• UnrestrictedBooleanMul.assignment q i = UnrestrictedBooleanMul.bitF2 ((UnrestrictedBooleanMul.tableVar i).getLsb q)

theorem UnrestrictedBooleanMul.eval_Mul_three (i : Fin 5) (q : Fin 64) : eval (Mul 3 i) (assignment q) = bitF2 ((targetTable i).getLsb q)

def UnrestrictedBooleanMul.truthR (x : BitVec 10) : BitVec 64

Truth table of a linear combination in the rational-place basis.

Equations

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

def UnrestrictedBooleanMul.truthW (x : BitVec 12) : BitVec 64

Truth table of a linear combination in the affine-plus-target basis.

Equations

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

theorem UnrestrictedBooleanMul.rationalRep_truth (c : Fin 10 → F₂) (q : Fin 64) : eval (rationalRep c) (assignment q) = bitF2 ((truthR (coeffBits c)).getLsb q)

theorem UnrestrictedBooleanMul.ambientRep_truth (c : Fin 12 → F₂) (q : Fin 64) : eval (ambientRep c) (assignment q) = bitF2 ((truthW (coeffBits c)).getLsb q)