def Hex.DensePoly.low {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p : DensePoly R) : DensePoly R

Coefficients strictly below k.

Equations

• Hex.DensePoly.low k p = Hex.DensePoly.ofList (List.map p.coeff (List.range k))

def Hex.DensePoly.high {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p : DensePoly R) : DensePoly R

Coefficients at and above k, shifted down by k.

Equations

• Hex.DensePoly.high k p = Hex.DensePoly.ofList (List.map (fun (i : Nat) => p.coeff (k + i)) (List.range (p.size - k)))

theorem Hex.DensePoly.coeff_low {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p : DensePoly R) (i : Nat) : (low k p).coeff i = if i < k then p.coeff i else 0

Coefficient law for the low half.

theorem Hex.DensePoly.coeff_high {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p : DensePoly R) (i : Nat) : (high k p).coeff i = if i < p.size - k then p.coeff (k + i) else 0

Coefficient law for the shifted-down high half.

theorem Hex.DensePoly.low_add_shift_high {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p : DensePoly R) : low k p + shift k (high k p) = p

Splitting at k and shifting the high half back reconstructs the input.

theorem Hex.DensePoly.shift_shift {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k l : Nat) (p : DensePoly R) : shift k (shift l p) = shift (k + l) p

Nested shifts add their offsets.

theorem Hex.DensePoly.shift_add {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p q : DensePoly R) : shift k (p + q) = shift k p + shift k q

Shifting distributes over polynomial addition.

theorem Hex.DensePoly.shift_mul {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p q : DensePoly R) : shift k p * q = shift k (p * q)

A shifted left factor shifts the product.

theorem Hex.DensePoly.mul_shift {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (p q : DensePoly R) : p * shift k q = shift k (p * q)

A shifted right factor shifts the product.

theorem Hex.DensePoly.shift_mul_shift {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k l : Nat) (p q : DensePoly R) : shift k p * shift l q = shift (k + l) (p * q)

Multiplying two shifted polynomials adds their offsets.

theorem Hex.DensePoly.karatsuba_combine {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (a₀ a₁ b₀ b₁ : DensePoly R) : have z₀ := a₀ * b₀; have z₂ := a₁ * b₁; have z₁ := (a₀ + a₁) * (b₀ + b₁) - z₀ - z₂; z₀ + shift k z₁ + shift (2 * k) z₂ = (a₀ + shift k a₁) * (b₀ + shift k b₁)

The three-product Karatsuba assembly identity.

def Hex.DensePoly.Karatsuba.Raw.add {R : Type u} [Lean.Grind.CommRing R] (a b : Array R) : Array R

Coefficientwise addition without polynomial normalization.

Equations

• Hex.DensePoly.Karatsuba.Raw.add a b = Array.ofFn fun (i : Fin (max a.size b.size)) => a.getD (↑i) 0 + b.getD (↑i) 0

def Hex.DensePoly.Karatsuba.Raw.sub {R : Type u} [Lean.Grind.CommRing R] (a b : Array R) : Array R

Coefficientwise subtraction without polynomial normalization.

Equations

• Hex.DensePoly.Karatsuba.Raw.sub a b = Array.ofFn fun (i : Fin (max a.size b.size)) => a.getD (↑i) 0 - b.getD (↑i) 0

def Hex.DensePoly.Karatsuba.Raw.low {R : Type u} [Lean.Grind.CommRing R] (k : Nat) (a : Array R) : Array R

The raw coefficient prefix strictly below k.

Equations

• Hex.DensePoly.Karatsuba.Raw.low k a = Array.ofFn fun (i : Fin (min k a.size)) => a.getD (↑i) 0

def Hex.DensePoly.Karatsuba.Raw.high {R : Type u} [Lean.Grind.CommRing R] (k : Nat) (a : Array R) : Array R

The raw coefficient suffix at k, shifted down.

Equations

• Hex.DensePoly.Karatsuba.Raw.high k a = Array.ofFn fun (i : Fin (a.size - k)) => a.getD (k + ↑i) 0

def Hex.DensePoly.Karatsuba.Raw.combine {R : Type u} [Lean.Grind.CommRing R] (k : Nat) (z₀ z₁ z₂ : Array R) : Array R

Assemble the three Karatsuba pieces in one output allocation.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.schoolbookCoeff {R : Type u} [Lean.Grind.CommRing R] (a b : Array R) (d : Nat) : R

One schoolbook convolution diagonal over raw arrays.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.schoolbook {R : Type u} [Lean.Grind.CommRing R] (a b : Array R) : Array R

Raw schoolbook multiplication with no normalization pass.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.mulAux {R : Type u} [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → Array R → Array R → Array R

Fuelled raw-array Karatsuba multiplication.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Karatsuba.Raw.mulAux cutoff 0 x✝¹ x✝ = Hex.DensePoly.Karatsuba.Raw.schoolbook x✝¹ x✝

def Hex.DensePoly.Karatsuba.Raw.squareAux {R : Type u} [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → Array R → Array R

Fuelled raw-array specialized Karatsuba squaring.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Karatsuba.Raw.squareAux cutoff 0 x✝ = Hex.DensePoly.Karatsuba.Raw.schoolbook x✝ x✝

def Hex.DensePoly.Karatsuba.Raw.addShift {R : Type u} [Lean.Grind.CommRing R] (offset : Nat) (a b : Array R) : Array R

Add a raw suffix at an offset in one output allocation.

Equations

• Hex.DensePoly.Karatsuba.Raw.addShift offset a b = Array.ofFn fun (i : Fin (max a.size (offset + b.size))) => a.getD (↑i) 0 + if offset ≤ ↑i then b.getD (↑i - offset) 0 else 0

def Hex.DensePoly.Karatsuba.Raw.addAt {R : Type u} [Lean.Grind.CommRing R] (offset : Nat) (acc b : Array R) : Array R

Accumulate only the shifted block support. The undersized-buffer branch grows the array without dropping coefficients, preserving unrestricted inputs.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.blocks {R : Type u} [Lean.Grind.CommRing R] (cutoff blockSize fuel : Nat) (long short : Array R) : Array R

Fuelled unbalanced block multiplication over raw arrays. For ordinary block dispatch, each raw product has size at most twice the short length minus one, including recursive padding. Since every visited offset is below the long length, this buffer contains every shifted block support. The growing fallback in addAt also handles unrestricted block sizes and prematurely exhausted fuel.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.schoolbookSlice {R : Type u} [Lean.Grind.CommRing R] (lo len : Nat) (a b : Array R) : Array R

A clipped raw schoolbook product.

Equations

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

def Hex.DensePoly.Karatsuba.Raw.sliceAux {R : Type u} [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → Nat → Nat → Array R → Array R → Array R

Fuelled interval-pruned Karatsuba recursion over raw arrays.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.Karatsuba.Raw.sliceAux cutoff 0 x✝³ x✝² x✝¹ x✝ = Hex.DensePoly.Karatsuba.Raw.schoolbookSlice x✝³ x✝² x✝¹ x✝

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_add {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : Array R) : ofCoeffs (add a b) = ofCoeffs a + ofCoeffs b

Raw coefficientwise addition represents polynomial addition.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_sub {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : Array R) : ofCoeffs (sub a b) = ofCoeffs a - ofCoeffs b

Raw coefficientwise subtraction represents polynomial subtraction.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_low {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (a : Array R) : ofCoeffs (low k a) = DensePoly.low k (ofCoeffs a)

A raw low split represents the polynomial low split.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_high {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (a : Array R) : ofCoeffs (high k a) = DensePoly.high k (ofCoeffs a)

A raw high split represents the polynomial shifted-down high split.

theorem Hex.DensePoly.Karatsuba.Raw.schoolbookCoeff_eq_dense {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : Array R) (d : Nat) : schoolbookCoeff a b d = (ofCoeffs a).schoolbookCoeff (ofCoeffs b) d

A raw diagonal fold represents the corresponding dense diagonal.

theorem Hex.DensePoly.Karatsuba.Raw.schoolbookCoeff_comm {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : Array R) (d : Nat) : schoolbookCoeff a b d = schoolbookCoeff b a d

Raw convolution diagonals are symmetric in their operands.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_schoolbook {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (a b : Array R) : ofCoeffs (schoolbook a b) = ofCoeffs a * ofCoeffs b

Raw schoolbook multiplication represents dense multiplication.

theorem Hex.DensePoly.Karatsuba.Raw.coeff_ofCoeffs_schoolbookSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (a b : Array R) (i : Nat) : (ofCoeffs (schoolbookSlice lo len a b)).coeff i = if i < len then (ofCoeffs a * ofCoeffs b).coeff (lo + i) else 0

A raw clipped schoolbook product has the planned slice coefficients.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_combine {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (k : Nat) (z₀ z₁ z₂ : Array R) : ofCoeffs (combine k z₀ z₁ z₂) = ofCoeffs z₀ + shift k (ofCoeffs z₁) + shift (2 * k) (ofCoeffs z₂)

Raw one-allocation assembly represents the Karatsuba shifted sum.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_addShift {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (offset : Nat) (a b : Array R) : ofCoeffs (addShift offset a b) = ofCoeffs a + shift offset (ofCoeffs b)

Raw shifted addition represents polynomial shifted addition.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_mulAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a b : Array R) : ofCoeffs (mulAux cutoff fuel a b) = ofCoeffs a * ofCoeffs b

Raw Karatsuba recursion represents dense multiplication for every fuel.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_squareAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a : Array R) : ofCoeffs (squareAux cutoff fuel a) = ofCoeffs a * ofCoeffs a

Raw specialized Karatsuba squaring represents dense squaring for every fuel.

theorem Hex.DensePoly.Karatsuba.Raw.ofCoeffs_blocks {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff blockSize fuel : Nat) (long short : Array R) : ofCoeffs (blocks cutoff blockSize fuel long short) = ofCoeffs long * ofCoeffs short

Raw block recursion represents dense multiplication for every fuel.

def Hex.DensePoly.karatsubaAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → DensePoly R → DensePoly R → DensePoly R

Fuelled three-product Karatsuba recursion. Fuel is separate from the cutoff so cutoff zero remains total; public callers provide at least the larger operand size.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.karatsubaAux cutoff 0 x✝¹ x✝ = x✝¹.mulImpl x✝

def Hex.DensePoly.karatsubaSquareAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → DensePoly R → DensePoly R

Specialized three-square Karatsuba recursion.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.karatsubaSquareAux cutoff 0 x✝ = x✝.mulImpl x✝

theorem Hex.DensePoly.karatsubaAux_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a b : DensePoly R) : karatsubaAux cutoff fuel a b = a * b

Every fuelled Karatsuba product agrees with schoolbook multiplication.

theorem Hex.DensePoly.karatsubaSquareAux_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a : DensePoly R) : karatsubaSquareAux cutoff fuel a = a * a

Every fuelled Karatsuba square agrees with ordinary squaring.

def Hex.DensePoly.karatsubaAuxImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a b : DensePoly R) : DensePoly R

Runtime Karatsuba recursion over raw coefficient arrays. The sole normalization pass is the final ofCoeffs.

Equations

• Hex.DensePoly.karatsubaAuxImpl cutoff fuel a b = Hex.DensePoly.ofCoeffs (Hex.DensePoly.Karatsuba.Raw.mulAux cutoff fuel a.toArray b.toArray)

theorem Hex.DensePoly.karatsubaAux_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a b : DensePoly R) : karatsubaAux cutoff fuel a b = karatsubaAuxImpl cutoff fuel a b

The raw-array Karatsuba runtime agrees with the proof-facing recursion.

@[csimp]

theorem Hex.DensePoly.karatsubaAux_csimp : @karatsubaAux = @karatsubaAuxImpl

Compile fuelled Karatsuba through the raw-array recursion.

def Hex.DensePoly.karatsubaSquareAuxImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a : DensePoly R) : DensePoly R

Runtime specialized Karatsuba squaring over raw coefficient arrays.

Equations

• Hex.DensePoly.karatsubaSquareAuxImpl cutoff fuel a = Hex.DensePoly.ofCoeffs (Hex.DensePoly.Karatsuba.Raw.squareAux cutoff fuel a.toArray)

theorem Hex.DensePoly.karatsubaSquareAux_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel : Nat) (a : DensePoly R) : karatsubaSquareAux cutoff fuel a = karatsubaSquareAuxImpl cutoff fuel a

The raw-array square runtime agrees with the proof-facing recursion.

@[csimp]

theorem Hex.DensePoly.karatsubaSquareAux_csimp : @karatsubaSquareAux = @karatsubaSquareAuxImpl

Compile specialized Karatsuba squaring through the raw-array recursion.

def Hex.DensePoly.mulKaratsubaBalanced {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : DensePoly R

Balanced Karatsuba multiplication with an explicit schoolbook cutoff.

Equations

• Hex.DensePoly.mulKaratsubaBalanced cutoff a b = Hex.DensePoly.karatsubaAux cutoff (max a.size b.size) a b

def Hex.DensePoly.squareKaratsubaImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a : DensePoly R) : DensePoly R

Specialized Karatsuba squaring with an explicit schoolbook cutoff.

Equations

• Hex.DensePoly.squareKaratsubaImpl cutoff a = Hex.DensePoly.karatsubaSquareAux cutoff a.size a

theorem Hex.DensePoly.mulKaratsubaBalanced_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : mulKaratsubaBalanced cutoff a b = a * b

Balanced Karatsuba multiplication agrees exactly with DensePoly.mul.

theorem Hex.DensePoly.squareKaratsubaImpl_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a : DensePoly R) : squareKaratsubaImpl cutoff a = a * a

Specialized Karatsuba squaring agrees exactly with DensePoly.mul.

def Hex.DensePoly.squareKaratsuba {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a : DensePoly R) : DensePoly R

Kernel-visible square; compiled code uses the existing Karatsuba square.

Equations

• Hex.DensePoly.squareKaratsuba cutoff a = a * a

theorem Hex.DensePoly.squareKaratsuba_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a : DensePoly R) : squareKaratsuba cutoff a = a * a

Planned squaring retains the exact reference product.

@[csimp]

theorem Hex.DensePoly.squareKaratsuba_csimp : @squareKaratsuba = @squareKaratsubaImpl

Compile the reference square through the existing Karatsuba engine.

def Hex.DensePoly.karatsubaBlocks {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff blockSize : Nat) : Nat → DensePoly R → DensePoly R → DensePoly R

Multiply a long operand by blocks of blockSize coefficients. Each block uses balanced Karatsuba; the shifted block products are accumulated without padding the short operand to the long size.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.karatsubaBlocks cutoff blockSize 0 x✝¹ x✝ = Hex.DensePoly.mulKaratsubaBalanced cutoff x✝¹ x✝

theorem Hex.DensePoly.karatsubaBlocks_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff blockSize fuel : Nat) (long short : DensePoly R) : karatsubaBlocks cutoff blockSize fuel long short = long * short

Blocked unbalanced multiplication agrees with the ordinary product for every fuel value.

def Hex.DensePoly.karatsubaBlocksImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff blockSize fuel : Nat) (long short : DensePoly R) : DensePoly R

Runtime unbalanced multiplication over raw coefficient arrays.

Equations

• Hex.DensePoly.karatsubaBlocksImpl cutoff blockSize fuel long short = Hex.DensePoly.ofCoeffs (Hex.DensePoly.Karatsuba.Raw.blocks cutoff blockSize fuel long.toArray short.toArray)

theorem Hex.DensePoly.karatsubaBlocks_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff blockSize fuel : Nat) (long short : DensePoly R) : karatsubaBlocks cutoff blockSize fuel long short = karatsubaBlocksImpl cutoff blockSize fuel long short

The raw-array block runtime agrees with the proof-facing recursion.

@[csimp]

theorem Hex.DensePoly.karatsubaBlocks_csimp : @karatsubaBlocks = @karatsubaBlocksImpl

Compile unbalanced multiplication through the raw-array block recursion.

def Hex.DensePoly.mulKaratsubaImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : DensePoly R

Full Karatsuba multiplication. Strongly skewed operands are processed in blocks near the shorter size rather than padded to the longer size.

Equations

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

theorem Hex.DensePoly.mulKaratsubaImpl_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : mulKaratsubaImpl cutoff a b = a * b

Full balanced-or-blocked Karatsuba multiplication agrees exactly with DensePoly.mul.

def Hex.DensePoly.mulKaratsuba {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : DensePoly R

Kernel-visible product; compiled code uses the existing balanced-or-blocked Karatsuba dispatch with the supplied cutoff.

Equations

• Hex.DensePoly.mulKaratsuba cutoff a b = a * b

theorem Hex.DensePoly.mulKaratsuba_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) (a b : DensePoly R) : mulKaratsuba cutoff a b = a * b

Planned multiplication retains the exact reference product.

@[csimp]

theorem Hex.DensePoly.mulKaratsuba_csimp : @mulKaratsuba = @mulKaratsubaImpl

Compile the reference product through the existing Karatsuba dispatch.

def Hex.DensePoly.coeffSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (p : DensePoly R) : DensePoly R

Extract len coefficients beginning at lo from an already-computed polynomial, shifting them down to degree zero.

Equations

• Hex.DensePoly.coeffSlice lo len p = Hex.DensePoly.ofList (List.map (fun (i : Nat) => p.coeff (lo + i)) (List.range len))

theorem Hex.DensePoly.coeff_coeffSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (lo len : Nat) (p : DensePoly R) (i : Nat) : (coeffSlice lo len p).coeff i = if i < len then p.coeff (lo + i) else 0

Coefficient law for extracting a polynomial interval.

theorem Hex.DensePoly.coeff_low_mul_low {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (a b : DensePoly R) (i : Nat) (hi : i < n) : (low n a * low n b).coeff i = (a * b).coeff i

Truncating both inputs above n preserves every product coefficient strictly below n.

def Hex.DensePoly.karatsubaSliceAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) : Nat → Nat → Nat → DensePoly R → DensePoly R → DensePoly R

Fuelled interval-pruned Karatsuba recursion. At a split, each of the three mathematical subproducts is computed once over the smallest bounding interval containing all of its shifted contributions to [lo, lo + len). Branches whose shifted output starts beyond the interval receive length zero.

Equations

• One or more equations did not get rendered due to their size.
• Hex.DensePoly.karatsubaSliceAux cutoff 0 x✝³ x✝² x✝¹ x✝ = Hex.DensePoly.schoolbookSlice x✝³ x✝² x✝¹ x✝

theorem Hex.DensePoly.coeff_karatsubaSliceAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel lo len : Nat) (a b : DensePoly R) (i : Nat) : (karatsubaSliceAux cutoff fuel lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0

Every fuelled interval recursion returns exactly the requested product coefficients.

theorem Hex.DensePoly.Karatsuba.Raw.coeff_ofCoeffs_sliceAux {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel lo len : Nat) (a b : Array R) (i : Nat) : (ofCoeffs (sliceAux cutoff fuel lo len a b)).coeff i = if i < len then (ofCoeffs a * ofCoeffs b).coeff (lo + i) else 0

Raw interval recursion returns exactly the requested dense-product coefficients for every fuel value.

def Hex.DensePoly.karatsubaSliceAuxImpl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel lo len : Nat) (a b : DensePoly R) : DensePoly R

Runtime interval-pruned Karatsuba recursion over raw coefficient arrays.

Equations

• Hex.DensePoly.karatsubaSliceAuxImpl cutoff fuel lo len a b = Hex.DensePoly.ofCoeffs (Hex.DensePoly.Karatsuba.Raw.sliceAux cutoff fuel lo len a.toArray b.toArray)

theorem Hex.DensePoly.karatsubaSliceAux_eq_impl {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff fuel lo len : Nat) (a b : DensePoly R) : karatsubaSliceAux cutoff fuel lo len a b = karatsubaSliceAuxImpl cutoff fuel lo len a b

The raw-array clipped runtime agrees with the proof-facing recursion.

@[csimp]

theorem Hex.DensePoly.karatsubaSliceAux_csimp : @karatsubaSliceAux = @karatsubaSliceAuxImpl

Compile clipped Karatsuba through the raw-array interval recursion.

def Hex.DensePoly.karatsubaSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff lo len : Nat) (a b : DensePoly R) : DensePoly R

Interval-pruned Karatsuba slicing.

Equations

• Hex.DensePoly.karatsubaSlice cutoff lo len a b = Hex.DensePoly.karatsubaSliceAux cutoff (max a.size b.size) lo len a b

theorem Hex.DensePoly.coeff_karatsubaSlice {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff lo len : Nat) (a b : DensePoly R) (i : Nat) : (karatsubaSlice cutoff lo len a b).coeff i = if i < len then (a * b).coeff (lo + i) else 0

Interval-pruned Karatsuba slicing has the exact planned-slice semantics.

def Hex.DensePoly.karatsubaPlan {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (cutoff : Nat) : MulPlan R

A lawful Karatsuba plan.

Equations

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