theorem Hex.DensePoly.Interpret.map_zero {E : Type u} {F : Type v} [Zero E] [Zero F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) : f Zero.zero = Zero.zero

def Hex.DensePoly.Interpret.map {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : DensePoly F

Map each stored coefficient, retaining normalization by zero reflection. The proof argument preserves stored length without a trailing-zero scan.

Equations

• Hex.DensePoly.Interpret.map f hz p = { coeffs := (List.map f p.toArray.toList).toArray, normalized := ⋯ }

def Hex.DensePoly.Interpret.mapImpl {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : DensePoly F

Runtime coefficient map, preserving the array implementation. The reference map supplies kernel reduction; its compiled replacement avoids lists.

Equations

• Hex.DensePoly.Interpret.mapImpl f hz p = { coeffs := Array.map f p.toArray, normalized := ⋯ }

theorem Hex.DensePoly.Interpret.map_eq_mapImpl {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : map f hz p = mapImpl f hz p

The kernel specification and the runtime array map return the same polynomial.

@[csimp]

theorem Hex.DensePoly.Interpret.map_eq_impl : @map = @mapImpl

Compiled clients use the original array map, with no intermediate lists.

@[simp]

theorem Hex.DensePoly.Interpret.map_size {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).size = p.size

@[simp]

theorem Hex.DensePoly.Interpret.map_array {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).toArray = Array.map f p.toArray

theorem Hex.DensePoly.Interpret.map_ofCoeffs {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (a : Array E) : map f hz (ofCoeffs a) = ofCoeffs (Array.map f a)

@[simp]

theorem Hex.DensePoly.Interpret.map_zero_poly {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) : map f hz 0 = 0

@[simp]

theorem Hex.DensePoly.Interpret.map_coeff {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) (i : Nat) : (map f hz p).coeff i = f (p.coeff i)

@[simp]

theorem Hex.DensePoly.Interpret.map_list {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).toList = List.map f p.toList

theorem Hex.DensePoly.Interpret.map_eq_zero {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : map f hz p = 0 ↔ p = 0

Interpretation preserves the zero polynomial and reflects it.

theorem Hex.DensePoly.Interpret.map_add {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Add E] [Add F] (ha : ∀ (a b : E), f (a + b) = f a + f b) (p q : DensePoly E) : map f hz (p + q) = map f hz p + map f hz q

Addition transfers using only preservation of scalar addition.

theorem Hex.DensePoly.Interpret.map_sub {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Sub F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (p q : DensePoly E) : map f hz (p - q) = map f hz p - map f hz q

Subtraction transfers without structural ring laws on either carrier.

theorem Hex.DensePoly.Interpret.map_neg {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Sub F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (p : DensePoly E) : map f hz (-p) = -map f hz p

Polynomial negation uses the executable subtraction operation.

theorem Hex.DensePoly.Interpret.map_scale {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Mul E] [Mul F] (hm : ∀ (a b : E), f (a * b) = f a * f b) (c : E) (p : DensePoly E) : map f hz (scale c p) = scale (f c) (map f hz p)

Scaling transfers even when nonzero representations are not canonical.

theorem Hex.DensePoly.Interpret.map_mul {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Add E] [Mul E] [Add F] [Mul F] (ha : ∀ (a b : E), f (a + b) = f a + f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p q : DensePoly E) : map f hz (p * q) = map f hz p * map f hz q

Schoolbook multiplication transfers in its actual accumulation order.

theorem Hex.DensePoly.Interpret.map_eval {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Add E] [Mul E] [Add F] [Mul F] (ha : ∀ (a b : E), f (a + b) = f a + f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p : DensePoly E) (x : E) : f (p.eval x) = (map f hz p).eval (f x)

Horner evaluation commutes with interpretation, including the zero case.

theorem Hex.DensePoly.Interpret.map_derivative {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [NatCast E] [Mul E] [NatCast F] [Mul F] (hn : ∀ (n : Nat), f ↑n = ↑n) (hm : ∀ (a b : E), f (a * b) = f a * f b) (p : DensePoly E) : map f hz p.derivative = (map f hz p).derivative

Natural-cast preservation is required for the actual derivative.

@[simp]

theorem Hex.DensePoly.Interpret.map_isZero {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).isZero = p.isZero

@[simp]

theorem Hex.DensePoly.Interpret.map_degree {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).natDegree = p.natDegree

theorem Hex.DensePoly.Interpret.map_leading {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) (p : DensePoly E) : (map f hz p).leadingCoeff = f p.leadingCoeff

theorem Hex.DensePoly.Interpret.map_divModMonic {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] (h1 : f 1 = 1) (p q : DensePoly E) (hq : q.Monic) : have hq' := ⋯; have r := p.divModMonic q hq; (map f hz r.fst, map f hz r.snd) = (map f hz p).divModMonic (map f hz q) hq'

The shared monic division needs no coefficient inverse. Its actual two outputs commute with zero-reflecting coefficient interpretation.

theorem Hex.DensePoly.Interpret.map_divMod {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : DensePoly E) : have r := p.divMod q; (map f hz r.fst, map f hz r.snd) = (map f hz p).divMod (map f hz q)

The actual existing division algorithm commutes with a zero-reflecting interpretation. The map is not required to be injective.

theorem Hex.DensePoly.Interpret.map_div {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : DensePoly E) : map f hz (p / q) = map f hz p / map f hz q

Transfer of the quotient selected by polynomial division notation.

theorem Hex.DensePoly.Interpret.map_mod {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : DensePoly E) : map f hz (p % q) = map f hz p % map f hz q

Transfer of the remainder selected by polynomial modulus notation.

theorem Hex.DensePoly.Interpret.map_gcd {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (p q : DensePoly E) : map f hz (p.gcd q) = (map f hz p).gcd (map f hz q)

Transfer of the actual gcd, including its structural fuel.

theorem Hex.DensePoly.Interpret.map_one {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [One E] [One F] (h1 : f 1 = 1) : map f hz 1 = 1

The literal scalar one is preserved when the scalar map preserves one.

theorem Hex.DensePoly.Interpret.map_xgcdAux {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (ha : ∀ (a b : E), f (a + b) = f a + f b) (r₀ s₀ t₀ r₁ s₁ t₁ : DensePoly E) (fuel : Nat) : have r := r₀.xgcdAux s₀ t₀ r₁ s₁ t₁ fuel; { gcd := map f hz r.gcd, left := map f hz r.left, right := map f hz r.right } = (map f hz r₀).xgcdAux (map f hz s₀) (map f hz t₀) (map f hz r₁) (map f hz s₁) (map f hz t₁) fuel

The extended Euclidean loop transports all three outputs and accumulators.

theorem Hex.DensePoly.Interpret.map_xgcd {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (ha : ∀ (a b : E), f (a + b) = f a + f b) (h1 : f 1 = 1) (p q : DensePoly E) : have r := p.xgcd q; { gcd := map f hz r.gcd, left := map f hz r.left, right := map f hz r.right } = (map f hz p).xgcd (map f hz q)

Interpretation of the actual extended gcd, with its size-derived bound.

theorem Hex.DensePoly.Interpret.map_xgcdLeftAux {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (ha : ∀ (a b : E), f (a + b) = f a + f b) (r₀ s₀ r₁ s₁ : DensePoly E) (fuel : Nat) : have r := r₀.xgcdLeftAux s₀ r₁ s₁ fuel; { gcd := map f hz r.gcd, left := map f hz r.left } = (map f hz r₀).xgcdLeftAux (map f hz s₀) (map f hz r₁) (map f hz s₁) fuel

One-sided extended gcd transports the accumulator used by inverse clients.

theorem Hex.DensePoly.Interpret.map_xgcdLeft {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Sub E] [Mul E] [Sub F] [Mul F] (hs : ∀ (a b : E), f (a - b) = f a - f b) (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] [Div E] [Div F] (hd : ∀ (a b : E), f (a / b) = f a / f b) (ha : ∀ (a b : E), f (a + b) = f a + f b) (h1 : f 1 = 1) (p q : DensePoly E) : have r := p.xgcdLeft q; { gcd := map f hz r.gcd, left := map f hz r.left } = (map f hz p).xgcdLeft (map f hz q)

One-sided extended gcd uses the same interpreted size-derived bound.

theorem Hex.DensePoly.Interpret.map_natPow {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Zero F] [DecidableEq F] (f : E → F) (hz : ∀ (x : E), f x = Zero.zero ↔ x = Zero.zero) [Mul E] [Mul F] (hm : ∀ (a b : E), f (a * b) = f a * f b) [One E] [Add E] [One F] [Add F] (ha : ∀ (a b : E), f (a + b) = f a + f b) (h1 : f 1 = 1) (p : DensePoly E) (n : Nat) : map f hz (p.natPow n) = (map f hz p).natPow n

Binary polynomial exponentiation transfers without ring laws on the carrier.

theorem Hex.DensePoly.Interpret.map_monicize {E : Type u} {F : Type v} [Zero E] [DecidableEq E] [Inv E] [Mul E] [Zero F] [DecidableEq F] [Inv F] [Mul F] (f : E → F) (hz : ∀ (x : E), f x = 0 ↔ x = 0) (hm : ∀ (a b : E), f (a * b) = f a * f b) (hi : ∀ (a : E), f a⁻¹ = (f a)⁻¹) (p : DensePoly E) : map f hz p.monicize = (map f hz p).monicize

Monicization transfers semantically; the leading representative need not be literal one.