def Hex.GaussDyadic.nsmul (n : Nat) (w : GaussDyadic) : GaussDyadic

A natural multiple of a Gaussian dyadic.

Equations

• Hex.GaussDyadic.nsmul n w = (Hex.GaussDyadic.ofInt ↑n).mul w

def Hex.GaussDyadic.pow (z : GaussDyadic) : Nat → GaussDyadic

A natural power of a Gaussian dyadic.

Equations

• z.pow 0 = Hex.GaussDyadic.ofInt 1
• z.pow n.succ = (z.pow n).mul z

@[simp]

theorem Hex.GaussDyadic.add_zero (z : GaussDyadic) : z.add (0, 0) = z

Zero is a right identity for Gaussian-dyadic addition.

@[simp]

theorem Hex.GaussDyadic.zero_add (z : GaussDyadic) : add (0, 0) z = z

Zero is a left identity for Gaussian-dyadic addition.

theorem Hex.GaussDyadic.add_assoc (x y z : GaussDyadic) : (x.add y).add z = x.add (y.add z)

Gaussian-dyadic addition is associative.

theorem Hex.GaussDyadic.add_comm (x y : GaussDyadic) : x.add y = y.add x

Gaussian-dyadic addition is commutative.

theorem Hex.GaussDyadic.add_cross (x y z w : GaussDyadic) : (x.add y).add (z.add w) = (x.add z).add (y.add w)

Reassociate two Gaussian-dyadic sums after exchanging their middle terms.

@[simp]

theorem Hex.GaussDyadic.mul_zero (z : GaussDyadic) : z.mul (0, 0) = (0, 0)

Zero is right-absorbing for Gaussian-dyadic multiplication.

@[simp]

theorem Hex.GaussDyadic.zero_mul (z : GaussDyadic) : mul (0, 0) z = (0, 0)

Zero is left-absorbing for Gaussian-dyadic multiplication.

@[simp]

theorem Hex.GaussDyadic.mul_one (z : GaussDyadic) : z.mul (ofInt 1) = z

One is a right identity for Gaussian-dyadic multiplication.

@[simp]

theorem Hex.GaussDyadic.one_mul (z : GaussDyadic) : (ofInt 1).mul z = z

One is a left identity for Gaussian-dyadic multiplication.

theorem Hex.GaussDyadic.mul_add (x y z : GaussDyadic) : x.mul (y.add z) = (x.mul y).add (x.mul z)

Gaussian-dyadic multiplication distributes over addition on the left.

theorem Hex.GaussDyadic.add_mul (x y z : GaussDyadic) : (x.add y).mul z = (x.mul z).add (y.mul z)

Gaussian-dyadic multiplication distributes over addition on the right.

theorem Hex.GaussDyadic.mul_assoc (x y z : GaussDyadic) : (x.mul y).mul z = x.mul (y.mul z)

Gaussian-dyadic multiplication is associative.

theorem Hex.GaussDyadic.mul_comm (x y : GaussDyadic) : x.mul y = y.mul x

Gaussian-dyadic multiplication is commutative.

@[simp]

theorem Hex.GaussDyadic.pow_zero (z : GaussDyadic) : z.pow 0 = ofInt 1

The zeroth Gaussian-dyadic power is one.

@[simp]

theorem Hex.GaussDyadic.pow_succ (z : GaussDyadic) (n : Nat) : z.pow (n + 1) = (z.pow n).mul z

Characterization of a successor Gaussian-dyadic power.

theorem Hex.GaussDyadic.nsmul_add (m n : Nat) (z : GaussDyadic) : nsmul (m + n) z = (nsmul m z).add (nsmul n z)

Adding natural scalars before scaling agrees with adding the scaled values.

@[simp]

theorem Hex.GaussDyadic.nsmul_one (z : GaussDyadic) : nsmul 1 z = z

Scaling a Gaussian dyadic by one leaves it unchanged.

theorem Hex.GaussDyadic.mul_nsmul (x y : GaussDyadic) (n : Nat) : x.mul (nsmul n y) = nsmul n (x.mul y)

A natural scalar can move across Gaussian-dyadic multiplication.

theorem Hex.GaussDyadic.mul_term (z a : GaussDyadic) (n r : Nat) : z.mul (nsmul n (a.mul (z.pow r))) = nsmul n (a.mul (z.pow (r + 1)))

Multiplication by z advances the power in a naturally scaled monomial.

def Hex.gaussSum (n : Nat) (f : Nat → GaussDyadic) : GaussDyadic

Sum f 0 + ⋯ + f (n-1) using named Gaussian-dyadic addition.

Equations

• Hex.gaussSum n f = List.foldl (fun (s : Hex.GaussDyadic) (i : Nat) => s.add (f i)) (0, 0) (List.range n)

@[simp]

theorem Hex.gaussSum_zero (f : Nat → GaussDyadic) : gaussSum 0 f = (0, 0)

The empty Gaussian-dyadic sum is zero.

theorem Hex.gaussSum_succ (n : Nat) (f : Nat → GaussDyadic) : gaussSum (n + 1) f = (gaussSum n f).add (f n)

Split the last term from a Gaussian-dyadic sum.

theorem Hex.mul_gaussSum (z : GaussDyadic) (n : Nat) (f : Nat → GaussDyadic) : z.mul (gaussSum n f) = gaussSum n fun (i : Nat) => z.mul (f i)

Left multiplication distributes over a Gaussian-dyadic sum.

theorem Hex.gaussSum_head (n : Nat) (f : Nat → GaussDyadic) : gaussSum (n + 1) f = (f 0).add (gaussSum n fun (i : Nat) => f (i + 1))

Split the first term from a nonempty Gaussian-dyadic sum.

def Hex.Taylor.init (p : ZPoly) : Array GaussDyadic

Initial coefficient array for Taylor expansion.

Equations

• Hex.Taylor.init p = (List.map (fun (i : Nat) => Hex.GaussDyadic.ofInt (Hex.DensePoly.coeff p i)) (List.range (Hex.DensePoly.size p))).toArray

def Hex.Taylor.pass (n : Nat) (z : GaussDyadic) (a : Array GaussDyadic) (k : Nat) : Array GaussDyadic

One in-place synthetic-division pass.

The Taylor implementation calls this with n = p.size; the separate argument keeps the inner fold independent of the polynomial representation.

Equations

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

def Hex.taylorCoeff (p : ZPoly) (z : GaussDyadic) (k : Nat) : GaussDyadic

Closed-form coefficient of X^k in the Taylor shift. The range index r represents the source coefficient at j = k + r.

Equations

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

def Hex.taylor (p : ZPoly) (z : GaussDyadic) : Array GaussDyadic

Exact Taylor coefficients of p at the Gaussian-dyadic point z: returns #[c₀, …, c_n] with p(X + z) = Σ cₖ Xᵏ, where cₖ = Σ_{j ≥ k} binomial(j, k) · aⱼ · z^{j−k} exactly. The result has size p.size (empty for the zero polynomial, a single cast coefficient for a nonzero constant). Computed by repeated synthetic division, using only exact Gaussian-dyadic additions and multiplications.

Equations

• Hex.taylor p z = List.foldl (Hex.Taylor.pass (Hex.DensePoly.size p) z) (Hex.Taylor.init p) (List.range (Hex.DensePoly.size p))

structure Hex.TaylorShift (p : ZPoly) (center : GaussDyadic) : Type

Exact Taylor coefficients indexed by the polynomial and centre they represent. The equality is proof-only; compiled values contain just the coefficient array. Equality is characterized by the subsingleton instance below, so no constructor injectivity rule is generated.

• coeffs : Array GaussDyadic

  The cached exact coefficient array.

• valid : self.coeffs = taylor p center

  The cache contains the exact Taylor shift at its indexed centre.

instance Hex.TaylorShift.instSubsingleton {p : ZPoly} {center : GaussDyadic} : Subsingleton (TaylorShift p center)

At fixed polynomial and centre the coefficient equality determines the cached shift uniquely.

def Hex.TaylorShift.compute (p : ZPoly) (center : GaussDyadic) : TaylorShift p center

Compute the exact Taylor shift at center.

Equations

• Hex.TaylorShift.compute p center = { coeffs := Hex.taylor p center, valid := ⋯ }

def Hex.TaylorShift.cast {p : ZPoly} {center center' : GaussDyadic} (shift : TaylorShift p center) (h : center = center') : TaylorShift p center'

Re-index a cached shift along an exact centre equality. This changes only proof indices; the compiled coefficient array is reused.

Equations

• shift.cast h = h ▸ shift

theorem Hex.taylor_size (p : ZPoly) (z : GaussDyadic) : (taylor p z).size = DensePoly.size p

The Taylor expansion has one coefficient per stored coefficient of p: the synthetic-division passes only overwrite entries of the initial length-p.size array, never resize it.

theorem Hex.taylor_getD (p : ZPoly) (z : GaussDyadic) (k : Nat) : (taylor p z).getD k (0, 0) = if k < DensePoly.size p then taylorCoeff p z k else (0, 0)

Characterization of a Taylor coefficient as the finite binomial sum Σ_r binom(k+r,k) · a_(k+r) · z^r.

theorem Hex.taylor_getD_of_lt (p : ZPoly) (z : GaussDyadic) (k : Nat) (hk : k < DensePoly.size p) : (taylor p z).getD k (0, 0) = taylorCoeff p z k

In-bounds form of taylor_getD, convenient for companion proofs.