hex

35.1.Β HexTruncatedSeries: fixed-precision seriesπŸ”—

35.1.1.Β IntroductionπŸ”—

HexTruncatedSeries provides executable power series whose precision is fixed in the type. A value of precision n stores exactly the coefficients below degree n; every operation discards higher terms. This makes the precision contract explicit while keeping the representation suitable for bounded multiplication and Newton iteration.

The computational library is Mathlib-free and depends only on HexBasic. It supplies arithmetic, precision changes, inverse, square root, exponential, logarithm, composition, and reversion. HexTruncatedSeriesMathlib, described in the correspondence section, identifies the representation with Mathlib power series modulo X ^ n.

35.1.2.Β Representation and arithmeticπŸ”—

πŸ”—structure
Hex.TSeries.{u} (R : Type u) (n : β„•) : Type u
Hex.TSeries.{u} (R : Type u) (n : β„•) :
  Type u

A power series over R truncated at precision n, represented by its coefficients in ascending degree order.

Constructor

Hex.TSeries.mk.{u}

Fields

coeffs : Vector R n

The coefficients of x^0 through x^(n-1).

πŸ”—def
Hex.TSeries.coeff.{u} {R : Type u} {n : β„•} [Zero R]
  (a : Hex.TSeries R n) (i : β„•) : R
Hex.TSeries.coeff.{u} {R : Type u} {n : β„•}
  [Zero R] (a : Hex.TSeries R n) (i : β„•) :
  R

The coefficient of x^i, read as zero when i is beyond the precision.

Coefficient access is total: an index outside the represented precision reads as zero. Tabulation and extensionality are the main constructor and equality principle.

πŸ”—def
Hex.TSeries.ofFn.{u} {R : Type u} {n : β„•} (f : β„• β†’ R) : Hex.TSeries R n
Hex.TSeries.ofFn.{u} {R : Type u} {n : β„•}
  (f : β„• β†’ R) : Hex.TSeries R n

Tabulate a truncated series from a total coefficient function.

πŸ”—theorem
Hex.TSeries.ext.{u} {R : Type u} {n : β„•} [Zero R]
  {a b : Hex.TSeries R n} (h : βˆ€ i < n, a.coeff i = b.coeff i) : a = b
Hex.TSeries.ext.{u} {R : Type u} {n : β„•}
  [Zero R] {a b : Hex.TSeries R n}
  (h : βˆ€ i < n, a.coeff i = b.coeff i) :
  a = b

Two truncated series are equal when all represented coefficients agree.

The usual notation is available for addition, subtraction, multiplication, and powers. Constants and the indeterminate have explicit constructors, and mulUpTo computes only the requested prefix.

πŸ”—def
Hex.TSeries.C.{u} {R : Type u} {n : β„•} [Zero R] (c : R) :
  Hex.TSeries R n
Hex.TSeries.C.{u} {R : Type u} {n : β„•}
  [Zero R] (c : R) : Hex.TSeries R n

The constant truncated series.

πŸ”—def
Hex.TSeries.X.{u} {R : Type u} {n : β„•} [Zero R] [One R] :
  Hex.TSeries R n
Hex.TSeries.X.{u} {R : Type u} {n : β„•}
  [Zero R] [One R] : Hex.TSeries R n

The indeterminate x, which is zero at precisions zero and one.

πŸ”—def
Hex.TSeries.mulUpTo.{u} {R : Type u} {n : β„•} [Zero R] [Add R] [Mul R]
  (m : β„•) (a b : Hex.TSeries R n) : Hex.TSeries R n
Hex.TSeries.mulUpTo.{u} {R : Type u}
  {n : β„•} [Zero R] [Add R] [Mul R] (m : β„•)
  (a b : Hex.TSeries R n) :
  Hex.TSeries R n

Multiply only through degree m - 1, zeroing the remaining stored coefficients.

This finite geometric series demonstrates that multiplication is always interpreted modulo the precision.

open Hex Hex.TSeries def geometric : TSeries Int 6 := ofFn fun _ => 1 #guard (geometric * (1 - X)).coeff 0 == 1 #guard (geometric * (1 - X)).coeff 4 == 0

35.1.3.Β Precision-changing operationsπŸ”—

Truncation and zero extension change the precision in the type. Multiplying or dividing by a power of X shifts coefficients; division is partial because discarded low coefficients must be zero. valuation? reports the first represented nonzero coefficient and returns none for the zero truncated series.

πŸ”—def
Hex.TSeries.truncate.{u} {R : Type u} {n : β„•} [Zero R]
  (a : Hex.TSeries R n) (m : β„•) (_h : m ≀ n) : Hex.TSeries R m
Hex.TSeries.truncate.{u} {R : Type u}
  {n : β„•} [Zero R] (a : Hex.TSeries R n)
  (m : β„•) (_h : m ≀ n) : Hex.TSeries R m

Discard coefficients at index m and above.

πŸ”—def
Hex.TSeries.extend.{u} {R : Type u} {n : β„•} [Zero R]
  (a : Hex.TSeries R n) (m : β„•) (_h : n ≀ m) : Hex.TSeries R m
Hex.TSeries.extend.{u} {R : Type u}
  {n : β„•} [Zero R] (a : Hex.TSeries R n)
  (m : β„•) (_h : n ≀ m) : Hex.TSeries R m

Pad a series with zero coefficients to a larger precision.

πŸ”—def
Hex.TSeries.divXPow?.{u} {R : Type u} {n : β„•} [Zero R] [DecidableEq R]
  (a : Hex.TSeries R n) (k : β„•) : Option (Hex.TSeries R (n - k))
Hex.TSeries.divXPow?.{u} {R : Type u}
  {n : β„•} [Zero R] [DecidableEq R]
  (a : Hex.TSeries R n) (k : β„•) :
  Option (Hex.TSeries R (n - k))

Divide by x^k when every discarded low coefficient is zero.

πŸ”—def
Hex.TSeries.valuation?.{u} {R : Type u} {n : β„•} [Zero R] [DecidableEq R]
  (a : Hex.TSeries R n) : Option β„•
Hex.TSeries.valuation?.{u} {R : Type u}
  {n : β„•} [Zero R] [DecidableEq R]
  (a : Hex.TSeries R n) : Option β„•

The first represented nonzero coefficient, if one exists.

open Hex Hex.TSeries def shifted : TSeries Int 6 := ofFn fun i => if i = 2 then 7 else 0 #guard shifted.valuation? == some 2 #guard (shifted.divXPow? 2).map (fun q => q.coeff 0) == some 7

Differentiation loses one coefficient of precision. Integration adds a zero constant coefficient and requires only the finitely many natural inverses needed at the chosen precision.

πŸ”—def
Hex.TSeries.deriv.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) : Hex.TSeries R (n - 1)
Hex.TSeries.deriv.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) :
  Hex.TSeries R (n - 1)

The formal derivative, losing one coefficient of precision.

πŸ”—def
Hex.TSeries.integrate.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R n] (a : Hex.TSeries R n) :
  Hex.TSeries R (n + 1)
Hex.TSeries.integrate.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R n]
  (a : Hex.TSeries R n) :
  Hex.TSeries R (n + 1)

Formal integration with zero constant coefficient.

πŸ”—type class
Hex.TSeries.NatInverses.{u} (R : Type u) [Lean.Grind.CommRing R]
  (m : β„•) : Type u
Hex.TSeries.NatInverses.{u} (R : Type u)
  [Lean.Grind.CommRing R] (m : β„•) : Type u

Inverses of the natural numbers 1 through m in R.

Instance Constructor

Hex.TSeries.NatInverses.mk.{u}

Methods

invNat : β„• β†’ R

A total lookup whose values are constrained on 1, ..., m.

invNat_eq : βˆ€ (k : β„•), 1 ≀ k β†’ k ≀ m β†’ ↑k * Hex.TSeries.NatInverses.invNat m k = 1

The lookup inverts every required natural number.

35.1.4.Β Newton operationsπŸ”—

The main algorithms accept algebraic witnesses rather than searching the coefficient ring. Optional wrappers use UnitOps when executable unit detection is available. Bounded variants expose the prefixes used by Newton doubling, and their agreement theorems connect those implementations to the full operations.

πŸ”—type class
Hex.TSeries.UnitOps.{u} (R : Type u) : Type u
Hex.TSeries.UnitOps.{u} (R : Type u) :
  Type u

An executable partial inverse operation on a coefficient ring.

Instance Constructor

Hex.TSeries.UnitOps.mk.{u}

Methods

inv? : R β†’ Option R

Return a multiplicative inverse when one is available.

πŸ”—def
Hex.TSeries.invOfUnit.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R) : Hex.TSeries R n
Hex.TSeries.invOfUnit.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R) :
  Hex.TSeries R n

The inverse of a, given an inverse of its constant coefficient.

πŸ”—def
Hex.TSeries.inv?.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.UnitOps R] (a : Hex.TSeries R n) :
  Option (Hex.TSeries R n)
Hex.TSeries.inv?.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.UnitOps R]
  (a : Hex.TSeries R n) :
  Option (Hex.TSeries R n)

Look up a constant-coefficient inverse and invert the series.

πŸ”—theorem
Hex.TSeries.invOfUnit_mul.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R] (a : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1) : a * a.invOfUnit u = 1
Hex.TSeries.invOfUnit_mul.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (u : R)
  (hu : a.coeff 0 * u = 1) :
  a * a.invOfUnit u = 1

Newton inversion satisfies the defining multiplicative equation.

Square-root lifting takes a chosen constant root r and an inverse of 2 * r; it proves both the square equation and uniqueness above that root.

πŸ”—def
Hex.TSeries.sqrtOfRoot.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R) : Hex.TSeries R n
Hex.TSeries.sqrtOfRoot.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R) :
  Hex.TSeries R n

The square root of a above r, given a witness inverting 2*r.

πŸ”—theorem
Hex.TSeries.sqrtOfRoot_sq.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R] (a : Hex.TSeries R n) (r v : R)
  (hr : r * r = a.coeff 0) (hv : (1 + 1) * r * v = 1) :
  a.sqrtOfRoot r v * a.sqrtOfRoot r v = a
Hex.TSeries.sqrtOfRoot_sq.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (a : Hex.TSeries R n) (r v : R)
  (hr : r * r = a.coeff 0)
  (hv : (1 + 1) * r * v = 1) :
  a.sqrtOfRoot r v * a.sqrtOfRoot r v = a

Newton lifting squares to the input under the stated root and unit hypotheses.

πŸ”—theorem
Hex.TSeries.sqrt_unique.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (s t : Hex.TSeries R n) (r v : R) (hv : (1 + 1) * r * v = 1)
  (hs : s * s = t * t) (hsr : s.coeff 0 = r) (htr : t.coeff 0 = r) :
  s = t
Hex.TSeries.sqrt_unique.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (s t : Hex.TSeries R n) (r v : R)
  (hv : (1 + 1) * r * v = 1)
  (hs : s * s = t * t)
  (hsr : s.coeff 0 = r)
  (htr : t.coeff 0 = r) : s = t

A square root is unique once its constant root has been fixed and 2*r is a unit.

Formal exponential and logarithm use NatInverses R (n - 1), so the core API states exactly which scalar divisions are required rather than assuming characteristic zero.

πŸ”—def
Hex.TSeries.exp.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n) :
  Hex.TSeries R n
Hex.TSeries.exp.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n) : Hex.TSeries R n

Formal exponential with constant coefficient one.

πŸ”—def
Hex.TSeries.log.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n) :
  Hex.TSeries R n
Hex.TSeries.log.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n) : Hex.TSeries R n

Formal logarithm with zero constant coefficient.

πŸ”—theorem
Hex.TSeries.log_exp.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n)
  (h : a.coeff 0 = 0) : a.exp.log = a
Hex.TSeries.log_exp.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n)
  (h : a.coeff 0 = 0) : a.exp.log = a

Logarithm is a left inverse to exponential on zero-constant series.

πŸ”—theorem
Hex.TSeries.exp_log.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (a : Hex.TSeries R n)
  (h : (a - 1).coeff 0 = 0) : a.log.exp = a
Hex.TSeries.exp_log.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (a : Hex.TSeries R n)
  (h : (a - 1).coeff 0 = 0) :
  a.log.exp = a

Exponential is a left inverse to logarithm on one-constant series.

35.1.5.Β Composition and reversionπŸ”—

Composition uses a Brent--Kung implementation and requires a zero constant coefficient for its algebraic laws. Reversion lifts an inverse of the linear coefficient by Newton iteration. A direct Lagrange implementation provides an independent route when the required natural inverses exist.

πŸ”—def
Hex.TSeries.comp.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) : Hex.TSeries R n
Hex.TSeries.comp.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) :
  Hex.TSeries R n

Substitute b into a, using Brent--Kung composition.

πŸ”—theorem
Hex.TSeries.comp_spec.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n) (h : b.coeff 0 = 0) :
  a.comp b =
    List.foldl (fun acc k => acc + Hex.TSeries.C (a.coeff k) * b.pow k)
      0 (List.range n)
Hex.TSeries.comp_spec.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (a b : Hex.TSeries R n)
  (h : b.coeff 0 = 0) :
  a.comp b =
    List.foldl
      (fun acc k =>
        acc +
          Hex.TSeries.C (a.coeff k) *
            b.pow k)
      0 (List.range n)

Composition is the finite truncated sum of coefficient-scaled powers.

πŸ”—def
Hex.TSeries.revOfUnit.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R) : Hex.TSeries R n
Hex.TSeries.revOfUnit.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R) :
  Hex.TSeries R n

The compositional inverse of b, given an inverse of its linear coefficient.

πŸ”—theorem
Hex.TSeries.revOfUnit_comp.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R] (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0) (hv : b.coeff 1 * v = 1) :
  b.comp (b.revOfUnit v) = Hex.TSeries.X ∧
    (b.revOfUnit v).comp b = Hex.TSeries.X
Hex.TSeries.revOfUnit_comp.{u}
  {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) :
  b.comp (b.revOfUnit v) = Hex.TSeries.X ∧
    (b.revOfUnit v).comp b = Hex.TSeries.X

Newton reversion is both a left and right compositional inverse.

πŸ”—def
Hex.TSeries.revLagrange.{u} {R : Type u} {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)] (b : Hex.TSeries R n) (v : R) :
  Hex.TSeries R n
Hex.TSeries.revLagrange.{u} {R : Type u}
  {n : β„•} [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (b : Hex.TSeries R n) (v : R) :
  Hex.TSeries R n

Direct Lagrange inversion. This deliberately performs the explicit division by k and therefore carries NatInverses R (n-1). Consecutive powers are carried through the fold, so the schoolbook route performs n full multiplications and costs O(nΒ³) rather than recomputing each power by square-and-multiply. When b.coeff 0 = 0, b = X * shiftQuotient b exactly; the unavailable top coefficient of the quotient is harmless because truncated multiplication is lower triangular.

πŸ”—theorem
Hex.TSeries.revLagrange_eq.{u} {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R] [Hex.TSeries.NatInverses R (n - 1)]
  (b : Hex.TSeries R n) (v : R) (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) : b.revLagrange v = b.revOfUnit v
Hex.TSeries.revLagrange_eq.{u}
  {R : Type u} {n : β„•}
  [Lean.Grind.CommRing R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (b : Hex.TSeries R n) (v : R)
  (h0 : b.coeff 0 = 0)
  (hv : b.coeff 1 * v = 1) :
  b.revLagrange v = b.revOfUnit v

Direct Lagrange inversion agrees with Newton reversion whenever its explicit natural-number divisions are available.

Here x - xΒ² has invertible linear coefficient. Both reversion algorithms produce the same series, and substitution recovers x at precision six.

open Hex Hex.TSeries def reversible : TSeries Rat 6 := X - X ^ 2 #guard comp reversible (revOfUnit reversible 1) == X #guard revLagrange reversible 1 == revOfUnit reversible 1

35.1.6.Β The Mathlib correspondenceπŸ”—

Everything above is executable and Mathlib-free. The companion installs Mathlib's CommRing API using those same operations and defines coefficient truncation from PowerSeries R as a surjective ring homomorphism.

πŸ”—def
HexTruncatedSeriesMathlib.ofPowerSeries.{u} {R : Type u} {n : β„•}
  [CommRing R] (f : PowerSeries R) : Hex.TSeries R n
HexTruncatedSeriesMathlib.ofPowerSeries.{u}
  {R : Type u} {n : β„•} [CommRing R]
  (f : PowerSeries R) : Hex.TSeries R n

Truncate a Mathlib power series to the first n coefficients.

πŸ”—def
HexTruncatedSeriesMathlib.ofPowerSeriesHom.{u} {R : Type u} {n : β„•}
  [CommRing R] : PowerSeries R β†’+* Hex.TSeries R n
HexTruncatedSeriesMathlib.ofPowerSeriesHom.{u}
  {R : Type u} {n : β„•} [CommRing R] :
  PowerSeries R β†’+* Hex.TSeries R n

Truncation from power series is a ring homomorphism.

Its kernel is the ideal generated by X ^ n, giving the headline quotient equivalence.

πŸ”—theorem
HexTruncatedSeriesMathlib.ker_ofPowerSeriesHom.{u} {R : Type u} {n : β„•}
  [CommRing R] :
  RingHom.ker HexTruncatedSeriesMathlib.ofPowerSeriesHom =
    Ideal.span {PowerSeries.X ^ n}
HexTruncatedSeriesMathlib.ker_ofPowerSeriesHom.{u}
  {R : Type u} {n : β„•} [CommRing R] :
  RingHom.ker
      HexTruncatedSeriesMathlib.ofPowerSeriesHom =
    Ideal.span {PowerSeries.X ^ n}

The kernel of coefficient truncation is the principal ideal (X^n).

πŸ”—def
HexTruncatedSeriesMathlib.quotEquiv.{u} {R : Type u} {n : β„•}
  [CommRing R] :
  PowerSeries R β§Έ Ideal.span {PowerSeries.X ^ n} ≃+* Hex.TSeries R n
HexTruncatedSeriesMathlib.quotEquiv.{u}
  {R : Type u} {n : β„•} [CommRing R] :
  PowerSeries R β§Έ
      Ideal.span {PowerSeries.X ^ n} ≃+*
    Hex.TSeries R n

Fixed-precision series are power series modulo X^n.

The correspondence covers powers, precision changes, differentiation, inverse, substitution, reversion, exponential, and logarithm. Square roots have a direct existence-and-uniqueness theorem because Mathlib has no matching power-series square-root operation with a supplied root.

πŸ”—theorem
HexTruncatedSeriesMathlib.deriv_ofPowerSeries.{u} {R : Type u} {n : β„•}
  [CommRing R] (f : PowerSeries R) :
  (HexTruncatedSeriesMathlib.ofPowerSeries f).deriv =
    HexTruncatedSeriesMathlib.ofPowerSeries
      ((PowerSeries.derivative R) f)
HexTruncatedSeriesMathlib.deriv_ofPowerSeries.{u}
  {R : Type u} {n : β„•} [CommRing R]
  (f : PowerSeries R) :
  (HexTruncatedSeriesMathlib.ofPowerSeries
        f).deriv =
    HexTruncatedSeriesMathlib.ofPowerSeries
      ((PowerSeries.derivative R) f)

Executable differentiation commutes with truncation, at the precision lost by differentiation.

πŸ”—theorem
HexTruncatedSeriesMathlib.ofPowerSeries_invOfUnit.{u} {R : Type u}
  {n : β„•} [CommRing R] (f : PowerSeries R) (u : RΛ£)
  (hu : PowerSeries.constantCoeff f = ↑u) :
  HexTruncatedSeriesMathlib.ofPowerSeries (f.invOfUnit u) =
    (HexTruncatedSeriesMathlib.ofPowerSeries f).invOfUnit ↑u⁻¹
HexTruncatedSeriesMathlib.ofPowerSeries_invOfUnit.{u}
  {R : Type u} {n : β„•} [CommRing R]
  (f : PowerSeries R) (u : RΛ£)
  (hu :
    PowerSeries.constantCoeff f = ↑u) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      (f.invOfUnit u) =
    (HexTruncatedSeriesMathlib.ofPowerSeries
          f).invOfUnit
      ↑u⁻¹

Truncation carries Mathlib's unit-certified inverse to executable Newton inversion.

πŸ”—theorem
HexTruncatedSeriesMathlib.ofPowerSeries_subst.{u} {R : Type u} {n : β„•}
  [CommRing R] (f g : PowerSeries R)
  (hg : PowerSeries.constantCoeff g = 0) :
  HexTruncatedSeriesMathlib.ofPowerSeries (PowerSeries.subst g f) =
    (HexTruncatedSeriesMathlib.ofPowerSeries f).comp
      (HexTruncatedSeriesMathlib.ofPowerSeries g)
HexTruncatedSeriesMathlib.ofPowerSeries_subst.{u}
  {R : Type u} {n : β„•} [CommRing R]
  (f g : PowerSeries R)
  (hg : PowerSeries.constantCoeff g = 0) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      (PowerSeries.subst g f) =
    (HexTruncatedSeriesMathlib.ofPowerSeries
          f).comp
      (HexTruncatedSeriesMathlib.ofPowerSeries
        g)

Truncation carries Mathlib substitution by a zero-constant series to executable composition.

πŸ”—theorem
HexTruncatedSeriesMathlib.ofPowerSeries_substInvOfIsUnit.{u}
  {R : Type u} {n : β„•} [CommRing R] (g : PowerSeries R)
  (h0 : PowerSeries.constantCoeff g = 0)
  (hu : IsUnit ((PowerSeries.coeff 1) g)) :
  HexTruncatedSeriesMathlib.ofPowerSeries (g.substInvOfIsUnit hu) =
    (HexTruncatedSeriesMathlib.ofPowerSeries g).revOfUnit ↑hu.unit⁻¹
HexTruncatedSeriesMathlib.ofPowerSeries_substInvOfIsUnit.{u}
  {R : Type u} {n : β„•} [CommRing R]
  (g : PowerSeries R)
  (h0 : PowerSeries.constantCoeff g = 0)
  (hu :
    IsUnit ((PowerSeries.coeff 1) g)) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      (g.substInvOfIsUnit hu) =
    (HexTruncatedSeriesMathlib.ofPowerSeries
          g).revOfUnit
      ↑hu.unit⁻¹

Truncation carries Mathlib's compositional inverse to executable Newton reversion.

πŸ”—theorem
HexTruncatedSeriesMathlib.ofPowerSeries_exp.{u} {R : Type u} {n : β„•}
  [CommRing R] [Algebra β„š R] [Hex.TSeries.NatInverses R (n - 1)]
  (f : PowerSeries R) (h : PowerSeries.constantCoeff f = 0) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      (PowerSeries.subst f (PowerSeries.exp R)) =
    (HexTruncatedSeriesMathlib.ofPowerSeries f).exp
HexTruncatedSeriesMathlib.ofPowerSeries_exp.{u}
  {R : Type u} {n : β„•} [CommRing R]
  [Algebra β„š R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (f : PowerSeries R)
  (h : PowerSeries.constantCoeff f = 0) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      (PowerSeries.subst f
        (PowerSeries.exp R)) =
    (HexTruncatedSeriesMathlib.ofPowerSeries
        f).exp

Truncation carries Mathlib's formal exponential to the executable truncated exponential.

πŸ”—theorem
HexTruncatedSeriesMathlib.ofPowerSeries_logOf.{u} {R : Type u} {n : β„•}
  [CommRing R] [Algebra β„š R] [Hex.TSeries.NatInverses R (n - 1)]
  (f : PowerSeries R) (h : PowerSeries.constantCoeff f = 1) :
  HexTruncatedSeriesMathlib.ofPowerSeries f.logOf =
    (HexTruncatedSeriesMathlib.ofPowerSeries f).log
HexTruncatedSeriesMathlib.ofPowerSeries_logOf.{u}
  {R : Type u} {n : β„•} [CommRing R]
  [Algebra β„š R]
  [Hex.TSeries.NatInverses R (n - 1)]
  (f : PowerSeries R)
  (h : PowerSeries.constantCoeff f = 1) :
  HexTruncatedSeriesMathlib.ofPowerSeries
      f.logOf =
    (HexTruncatedSeriesMathlib.ofPowerSeries
        f).log

Truncation carries Mathlib's formal logarithm to the executable truncated logarithm.

πŸ”—theorem
HexTruncatedSeriesMathlib.exists_unique_sq.{u} {R : Type u} [CommRing R]
  (f : PowerSeries R) (r : R) (hr : r * r = PowerSeries.constantCoeff f)
  (hu : IsUnit (2 * r)) :
  βˆƒ! s, s * s = f ∧ PowerSeries.constantCoeff s = r
HexTruncatedSeriesMathlib.exists_unique_sq.{u}
  {R : Type u} [CommRing R]
  (f : PowerSeries R) (r : R)
  (hr :
    r * r = PowerSeries.constantCoeff f)
  (hu : IsUnit (2 * r)) :
  βˆƒ! s,
    s * s = f ∧
      PowerSeries.constantCoeff s = r

A unit derivative at a chosen constant root gives exactly one square-root lift in the full power-series ring.

35.1.7.Β Cross-referencesπŸ”—

  • HexBasic supplies the kernel-reducible vector and fold helpers used by the fixed-length representation and convolution.

  • HexTruncatedSeriesMathlib is the proof boundary: it imports Mathlib, while HexTruncatedSeries and executable consumers do not.

  • Polynomial reversal and fast polynomial division belong above this library in the dependency graph; the truncated-series API deliberately names no polynomial representation.