@[irreducible]

def Hex.SparsePoly.pow1 {R : Type u} [Mul R] (x : R) : Nat → R

x^g for g ≥ 1 by binary powering, using only multiplication: gap powers never need an identity element (pow1 x 0 is x, unused).

Equations

• Hex.SparsePoly.pow1 x 0 = x
• Hex.SparsePoly.pow1 x 1 = x
• Hex.SparsePoly.pow1 x g.succ.succ = if (g + 2) % 2 = 1 then Hex.SparsePoly.pow1 (x * x) ((g + 2) / 2) * x else Hex.SparsePoly.pow1 (x * x) ((g + 2) / 2)

def Hex.SparsePoly.mulPow {R : Type u} [Mul R] (a x : R) : Nat → R

a * x^g, using only multiplication: g = 0 is the identity application and multiplies nothing.

Equations

• Hex.SparsePoly.mulPow a x 0 = a
• Hex.SparsePoly.mulPow a x g.succ = a * Hex.SparsePoly.pow1 x (g + 1)

def Hex.SparsePoly.evalShifted {R : Type u} [Zero R] [Add R] [Mul R] (x : R) : List (Nat × R) → Nat → R

Gap-Horner worker: the value of an ascending term list at x, relative to a base exponent, with each bracket closed by one gap power. evalShifted x l b is Σ cᵢ · x^(eᵢ − b) bracketed as (c₀ + (c₁ + …) · x^(e₁−e₀)) · x^(e₀−b).

Equations

• Hex.SparsePoly.evalShifted x [] x✝ = 0
• Hex.SparsePoly.evalShifted x ((e, c) :: rest) x✝ = Hex.SparsePoly.mulPow (c + Hex.SparsePoly.evalShifted x rest e) x (e - x✝)

def Hex.SparsePoly.eval {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (s : SparsePoly R) (x : R) : R

Evaluate at x by Horner over the exponent gaps: writing m for the term count and n for the degree, m additions and O(m · log(n/m + 1)) multiplications, against DensePoly's O(n).

Equations

• s.eval x = Hex.SparsePoly.evalShifted x s.terms.toList 0

theorem Hex.SparsePoly.sq_pow {S : Type u} [Lean.Grind.Semiring S] (x : S) (n : Nat) : (x * x) ^ n = x ^ (2 * n)

Powers of the square are even powers.

theorem Hex.SparsePoly.pow1_eq {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (x : S) (g : Nat) (hg : 1 ≤ g) : pow1 x g = x ^ g

The positive binary powering computes the semiring power.

theorem Hex.SparsePoly.pow_add' {S : Type u} [Lean.Grind.Semiring S] (x : S) (a b : Nat) : x ^ a * x ^ b = x ^ (a + b)

Powers at added exponents multiply.

theorem Hex.SparsePoly.mulPow_eq {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (a x : S) (g : Nat) : mulPow a x g = a * x ^ g

The gap multiplier computes multiplication by the power.

theorem Hex.SparsePoly.evalShifted_eq {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] {l : List (Nat × S)} (hs : List.Pairwise (fun (a b : Nat × S) => a.fst < b.fst) l) (x : S) (base : Nat) (hbase : ∀ (t : Nat × S), t ∈ l → base ≤ t.fst) : evalShifted x l base = List.foldr (fun (t : Nat × S) (acc : S) => t.snd * x ^ (t.fst - base) + acc) 0 l

The gap-Horner worker computes the exponent-shifted term sum.

theorem Hex.SparsePoly.eval_toDense {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) (x : S) : s.eval x = s.toDense.eval x

Gap Horner agrees with dense Horner. Lean.Grind.Semiring and not CommRing: both run in the same orientation and the gap form only skips the zero coefficients, so no coefficient is commuted past a power of x.

def Hex.SparsePoly.derivative {R : Type u} [Zero R] [DecidableEq R] [NatCast R] [Mul R] (s : SparsePoly R) : SparsePoly R

The formal derivative: c · x^e maps to (e : R) · c · x^(e−1), the e = 0 term is dropped, and — the invariant hazard — a coefficient (e : R) * c that vanishes (every exponent divisible by p over ZMod64 p) drops its term rather than storing a zero.

Equations

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

theorem Hex.SparsePoly.coeffList_filter_ne_zero {R : Type u} [Zero R] {l : List (Nat × R)} {e : Nat} (he : e ≠ 0) : coeffList (List.filter (fun (t : Nat × R) => decide (t.fst ≠ 0)) l) e = coeffList l e

Removing the constant term changes no other coefficient.

theorem Hex.SparsePoly.coeff_derivative {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) (f : Nat) : s.derivative.coeff f = ↑(f + 1) * s.coeff (f + 1)

Coefficient law for the derivative.

def Hex.SparsePoly.substPow {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) (k : Nat) : SparsePoly R

Substitute x^k for x: multiply every exponent by k. For k ≥ 1 the map is strictly monotone, so the terms, their order, and their coefficients are unchanged and the cost is O(t). For k = 0 every term lands on exponent 0, so the result is the combined constant, which can vanish; that case is a canonicalisation to perform, not an input to reject.

Equations

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

theorem Hex.SparsePoly.coeff_substPow_mul {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) {k : Nat} (hk : k ≠ 0) (e : Nat) : (s.substPow k).coeff (k * e) = s.coeff e

Coefficient law for the sparse substitution, positive case: the coefficient moves from e to k · e untouched.

theorem Hex.SparsePoly.coeff_substPow_of_ne {R : Type u} [Zero R] [DecidableEq R] [Add R] (s : SparsePoly R) {k : Nat} (hk : k ≠ 0) {f : Nat} (hf : ∀ (e : Nat), f ≠ k * e) : (s.substPow k).coeff f = 0

Off the multiples of k, the substituted polynomial vanishes.

def Hex.SparsePoly.substScaleStep {R : Type u} [Mul R] (a : R) (prev : Nat) (pw : Option R) (e : Nat) : Option R

One step of the substScale walk: the power of a for the next exponent, from the power at the previous one (none encodes a^0, so no identity element is needed).

Equations

• Hex.SparsePoly.substScaleStep a prev none e = if e - prev = 0 then none else some (Hex.SparsePoly.pow1 a (e - prev))
• Hex.SparsePoly.substScaleStep a prev (some p) e = if e - prev = 0 then some p else some (p * Hex.SparsePoly.pow1 a (e - prev))

def Hex.SparsePoly.substScaleGo {R : Type u} [Zero R] [DecidableEq R] [Mul R] (a : R) : Nat → Option R → List (Nat × R) → List (Nat × R)

Walk the ascending terms scaling each coefficient by the accumulated power of a, dropping the products that vanish: the worker for substScale.

Equations

• One or more equations did not get rendered due to their size.
• Hex.SparsePoly.substScaleGo a x✝¹ x✝ [] = []

theorem Hex.SparsePoly.exp_mem_substScaleGo {R : Type u} [Zero R] [DecidableEq R] [Mul R] {a : R} {l : List (Nat × R)} {prev : Nat} {pw : Option R} {u : Nat × R} (hu : u ∈ substScaleGo a prev pw l) : ∃ (v : Nat × R), v ∈ l ∧ u.fst = v.fst

Every exponent the walk emits is a stored one.

theorem Hex.SparsePoly.substScaleGo_canonical {R : Type u} [Zero R] [DecidableEq R] [Mul R] {a : R} {l : List (Nat × R)} (hs : List.Pairwise (fun (x y : Nat × R) => x.fst < y.fst) l) (prev : Nat) (pw : Option R) : List.Pairwise (fun (x y : Nat × R) => x.fst < y.fst) (substScaleGo a prev pw l) ∧ ∀ (t : Nat × R), t ∈ substScaleGo a prev pw l → t.snd ≠ 0

The walk emits a canonical list.

def Hex.SparsePoly.substScale {R : Type u} [Zero R] [DecidableEq R] [Mul R] (s : SparsePoly R) (a : R) : SparsePoly R

Scale the argument: c · x^e maps to (c · a^e) · x^e, with the powers of a computed from the exponent gaps as eval computes its powers of x. Exponents are unchanged; coefficients can vanish when a is a zero divisor or zero, so the zero filter applies.

Equations

• s.substScale a = Hex.SparsePoly.ofCanonicalList (Hex.SparsePoly.substScaleGo a 0 none s.terms.toList) ⋯ ⋯

@[irreducible]

def Hex.SparsePoly.polyPow1 {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (p : SparsePoly R) : Nat → SparsePoly R

p^g for g ≥ 1 by binary powering over mul, with no identity needed: the gap powers of compose are always positive.

Equations

• p.polyPow1 0 = p
• p.polyPow1 1 = p
• p.polyPow1 g.succ.succ = if (g + 2) % 2 = 1 then (p * p).polyPow1 ((g + 2) / 2) * p else (p * p).polyPow1 ((g + 2) / 2)

def Hex.SparsePoly.composeStep {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (t : SparsePoly R) (st : SparsePoly R × Nat × Option (SparsePoly R)) (term : Nat × R) : SparsePoly R × Nat × Option (SparsePoly R)

Substitute t for x in s: Σ cₑ · t^e in increasing exponent, with the powers of t obtained by binary powering from the exponent gaps. The cost is the sum of the multiplication costs over this schedule, not a function of the output size. A caller wanting f(x^k) must use substPow, never this.

Equations

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

def Hex.SparsePoly.compose {R : Type u} [Zero R] [DecidableEq R] [Add R] [Mul R] (s t : SparsePoly R) : SparsePoly R

Substitute t for the variable of s: one fold of composeStep over the terms, carrying the running power of t across each exponent gap.

Equations

• s.compose t = (Array.foldl t.composeStep (0, 0, none) s.terms).fst

theorem Hex.SparsePoly.derivative_toDense {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s : SparsePoly S) : s.derivative.toDense = s.toDense.derivative

The derivative transports through the dense conversion.

theorem Hex.SparsePoly.derivative_add {S : Type u} [Lean.Grind.Semiring S] [DecidableEq S] (s t : SparsePoly S) : (s + t).derivative = s.derivative + t.derivative

The derivative is additive.

theorem Hex.SparsePoly.derivative_mul {C : Type u} [Lean.Grind.CommRing C] [DecidableEq C] (s t : SparsePoly C) : (s * t).derivative = s.derivative * t + s * t.derivative

The product rule, by transport through the dense derivative.

theorem Hex.SparsePoly.poly_pow_add {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (p : SparsePoly K) (a b : Nat) : p ^ (a + b) = p ^ a * p ^ b

Powers at added exponents multiply, on the polynomials themselves.

theorem Hex.SparsePoly.poly_sq_pow {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (p : SparsePoly K) (n : Nat) : (p * p) ^ n = p ^ (2 * n)

Powers of the square are even powers, on the polynomials themselves.

theorem Hex.SparsePoly.polyPow1_eq {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (p : SparsePoly K) (g : Nat) (hg : 1 ≤ g) : p.polyPow1 g = p ^ g

The positive binary powering over mul computes the power.

theorem Hex.SparsePoly.eval_add {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s t : SparsePoly K) (x : K) : (s + t).eval x = s.eval x + t.eval x

Evaluation is additive, by transport.

theorem Hex.SparsePoly.eval_mul {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s t : SparsePoly K) (x : K) : (s * t).eval x = s.eval x * t.eval x

Evaluation is multiplicative, by transport.

@[simp]

theorem Hex.SparsePoly.eval_monomial {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (e : Nat) (c x : K) : (monomial e c).eval x = c * x ^ e

Evaluating a monomial multiplies its coefficient by the power.

@[simp]

theorem Hex.SparsePoly.eval_C {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (c x : K) : (C c).eval x = c

Constants evaluate to their value.

@[simp]

theorem Hex.SparsePoly.eval_one {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (x : K) : eval 1 x = 1

One evaluates to 1.

@[simp]

theorem Hex.SparsePoly.eval_zero {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (x : K) : eval 0 x = 0

Zero evaluates to 0.

theorem Hex.SparsePoly.eval_pow {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (n : Nat) (x : K) : (s ^ n).eval x = s.eval x ^ n

Evaluation respects powers.

def Hex.SparsePoly.tpVal {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] : Option (SparsePoly K) → SparsePoly K

The value the compose walk carries for t^prev (none encodes t^0 so that no identity element is needed at the [Add R] [Mul R] signature).

Equations

• Hex.SparsePoly.tpVal none = 1
• Hex.SparsePoly.tpVal (some p) = p

theorem Hex.SparsePoly.compose_eq_foldl {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s t : SparsePoly K) : s.compose t = List.foldl (fun (a : SparsePoly K) (u : Nat × K) => a + C u.snd * t ^ u.fst) 0 s.terms.toList

compose as the plain power-sum fold over the stored terms: the characterisation everything below transports through.

theorem Hex.SparsePoly.toDense_composePower {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (t : SparsePoly K) (n : Nat) : (t ^ n).toDense = t.toDense.composePower n

Powers transport to the dense iterated product.

theorem Hex.SparsePoly.compose_toDense {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s t : SparsePoly K) : (s.compose t).toDense = s.toDense.compose t.toDense

The substitution transports: composing then converting is converting then composing.

theorem Hex.SparsePoly.monomial_pow {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (k : Nat) (c : K) (e : Nat) : monomial k c ^ e = monomial (k * e) (c ^ e)

Powers of a monomial are monomials.

theorem Hex.SparsePoly.C_mul_monomial {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (c : K) (m : Nat) (d : K) : C c * monomial m d = monomial m (c * d)

Constants scale monomials by scaling their coefficient.

theorem Hex.SparsePoly.substPow_eq_compose {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (k : Nat) : s.substPow k = s.compose (monomial k 1)

The fast path and the general path agree: what lets the cyclotomic adapter use substPow and reason with compose.

theorem Hex.SparsePoly.eval_compose {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s t : SparsePoly K) (x : K) : (s.compose t).eval x = s.eval (t.eval x)

Substitution then evaluation is evaluation at the evaluation.

theorem Hex.SparsePoly.eval_substPow {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (k : Nat) (x : K) : (s.substPow k).eval x = s.eval (x ^ k)

Evaluating the exponent substitution is evaluating at the power.

theorem Hex.SparsePoly.substPow_toDense {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (k : Nat) : (s.substPow k).toDense = s.toDense.compose (DensePoly.monomial k 1)

The exponent substitution transports to dense composition with the unit monomial.

theorem Hex.SparsePoly.coeff_substScale {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (a : K) (e : Nat) : (s.substScale a).coeff e = s.coeff e * a ^ e

Coefficient law for substScale: each coefficient is scaled by the power of the argument at its exponent.

theorem Hex.SparsePoly.substScale_eq_compose {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (a : K) : s.substScale a = s.compose (monomial 1 a)

Argument scaling is composition with the degree-one monomial a · x: the sparse fast path and the general path agree.

theorem Hex.SparsePoly.substScale_toDense {K : Type u} [Lean.Grind.CommRing K] [DecidableEq K] (s : SparsePoly K) (a : K) : (s.substScale a).toDense = s.toDense.compose (DensePoly.monomial 1 a)

The scaling substitution transports to dense composition with the degree-one monomial.