@[irreducible]

def Hex.powNat {R : Type u} [One R] [Mul R] (x : R) (n : Nat) : R

Natural powers by binary exponentiation, using only the executable One and Mul operations. The association order is part of this law-free computational definition; correctness consumers assume associative ring multiplication.

Equations

• Hex.powNat x n = if n = 0 then 1 else have y := Hex.powNat (x * x) (n / 2); if n % 2 = 0 then y else y * x

theorem Hex.mul_pow {S : Type u} [Lean.Grind.CommRing S] (a b : S) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n

Powers distribute over multiplication in a lightweight commutative ring.

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

Raising a power to another power multiplies the two exponents.

theorem Hex.pow_ne_zero {S : Type u} [Lean.Grind.CommRing S] [Div S] [ExactDivLaws S] (h1 : 1 ≠ 0) {a : S} (ha : a ≠ 0) (n : Nat) : a ^ n ≠ 0

Natural powers of a nonzero element stay nonzero in every nontrivial exact-division ring.

theorem Hex.powNat_eq_pow {S : Type u} [Lean.Grind.Semiring S] (x : S) (n : Nat) : powNat x n = x ^ n

The executable binary power agrees with the lightweight semiring power.

theorem Hex.powNat_ne_zero {S : Type u} [Lean.Grind.CommRing S] [Div S] [ExactDivLaws S] (h1 : 1 ≠ 0) {a : S} (ha : a ≠ 0) (n : Nat) : powNat a n ≠ 0

The executable natural power of a nonzero element stays nonzero.

def Hex.divExp {R : Type u} [Zero R] [DecidableEq R] [One R] [Mul R] [Div R] (x y : R) (n : Nat) : R

Brown's scalar update x^n / y^(n-1), with the same total zero behavior as exactDiv.

Equations

• Hex.divExp x y n = Hex.exactDiv (Hex.powNat x n) (Hex.powNat y (n - 1))

theorem Hex.DensePoly.size_scale {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {a : R} (ha : a ≠ 0) (p : DensePoly R) : (scale a p).size = p.size

A nonzero scalar does not change the normalized dense size.

theorem Hex.DensePoly.scale_ne_zero {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {a : R} (ha : a ≠ 0) {p : DensePoly R} (hp : p ≠ 0) : scale a p ≠ 0

Scaling a nonzero polynomial by a nonzero coefficient remains nonzero.

theorem Hex.DensePoly.leadingCoeff_scale {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {a : R} (ha : a ≠ 0) (p : DensePoly R) : (scale a p).leadingCoeff = a * p.leadingCoeff

The leading coefficient scales with a nonzero coefficient scalar.

noncomputable def Hex.DensePoly.divScalar {R : Type u} [Zero R] [DecidableEq R] [Div R] (p : DensePoly R) (b : R) : DensePoly R

Divide every coefficient by the same scalar.

Kernel-facing specification: one map over the coefficient list. Compiled code runs the Array.map pass divScalarImpl via divScalar_eq_impl.

Equations

• p.divScalar b = if b = 0 then 0 else Hex.DensePoly.ofList (List.map (fun (a : R) => a / b) p.toList)

def Hex.DensePoly.divScalarImpl {R : Type u} [Zero R] [DecidableEq R] [Div R] (p : DensePoly R) (b : R) : DensePoly R

Runtime array implementation of coefficientwise exact scalar division.

Equations

• p.divScalarImpl b = if b = 0 then 0 else Hex.DensePoly.ofCoeffs (Array.map (fun (a : R) => a / b) p.toArray)

theorem Hex.DensePoly.divScalar_eq_divScalarImpl {R : Type u} [Zero R] [DecidableEq R] [Div R] (p : DensePoly R) (b : R) : p.divScalar b = p.divScalarImpl b

The list specification and array implementation of scalar division agree.

theorem Hex.DensePoly.size_divScalarImpl_le {R : Type u} [Zero R] [DecidableEq R] [Div R] (p : DensePoly R) (b : R) : (p.divScalarImpl b).size ≤ p.size

Coefficientwise scalar division cannot increase the stored polynomial size.

@[csimp]

theorem Hex.DensePoly.divScalar_eq_impl : @divScalar = @divScalarImpl

Register the array pass as the compiled scalar-division implementation.

theorem Hex.DensePoly.coeff_divScalar {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (p : DensePoly R) {b : R} (hb : b ≠ 0) (n : Nat) : (p.divScalar b).coeff n = p.coeff n / b

Coefficient law for exact scalar division by a nonzero factor.

@[simp]

theorem Hex.DensePoly.divScalar_scale {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] (p : DensePoly R) {b : R} (hb : b ≠ 0) : (scale b p).divScalar b = p

Exact scalar division undoes scalar multiplication by a nonzero factor.

theorem Hex.DensePoly.scale_cancel {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] {b : R} (hb : b ≠ 0) {p q : DensePoly R} (h : scale b p = scale b q) : p = q

Scaling by a nonzero coefficient is cancellable.

instance Hex.instExactDivLawsDensePoly {R : Type u} [Lean.Grind.CommRing R] [DecidableEq R] [Div R] [ExactDivLaws R] : ExactDivLaws (DensePoly R)

Exact coefficient division lifts recursively to exact dense-polynomial division, including nonunit constants and nonmonic polynomial factors.