API checks for the Leibniz identities on the spaces P_α #
The degree-one approach-zero series a has a nonzero class in P_1. Its
square exercises the two-term identity eventually_of_derivAt_mul_of_pos; the check
records that neither endpoint term is degenerate, because the class of a is nonzero and the
values ∂(a)(γ) are not eventually zero. A nonzero constant k, of degree 0, against
a exercises the one-term identity eventually_of_derivAt_mul_of_eq_zero, and the
Leibniz rule principalSubringDerivation_mul of ∂ : P̂ → Fun_{0⁻}(P̂) then reads
∂(a k) = k ∂(a), since ∂ vanishes on scalars. The zero series is the degenerate case.
The nearest wrong statement is an unconditional two-term identity in which the factor of degree
0 or a limit ordinal contributes π_α(u) π_β(v^{|γ}) with π_β(v^{|γ}) the class of the
translated truncation in P_β itself. At degree β = 0 that class vanishes termwise, which the
last check records, so the present fixture certifies the branch where the degree is a limit ordinal
but does not separate it from the unconditional identity; the two differ only when β ≥ ω is a
limit ordinal, for which there
there is no fixture in the test suite.
The degree-one class of the approach-zero series.
Equations
Instances For
The approach-zero class is nonzero in P_1.
Both grades successors: two endpoint terms #
The Leibniz identity for a · a in P_{(1+1)⁻}: near zero, the cutoff class of (a a)^{|γ}
is π_{1⁻}(a^{|γ}) π_1(a) + π_1(a) π_{1⁻}(a^{|γ}).
Neither endpoint term of approachZero_sq_leibniz is degenerate: the values ∂(a)(γ) are
not eventually zero, because ∂ of the class of a is nonzero.
A limit-grade factor: one endpoint term #
The Leibniz identity for a · k with k a constant of limit grade 0: near zero, the
cutoff class of (a k)^{|γ} in P_{(1+0)⁻} is the single term π_{1⁻}(a^{|γ}) π_0(k).
The homogeneous inclusion of the approach-zero class in P̂.
Equations
Instances For
The Leibniz rule of Δ against a scalar: Δ(a k) = k • Δ(a), the scalar term vanishing
because Δ is zero on the limit grade 0.
At grade 0 the would-be second endpoint term vanishes termwise: for γ < 0 the cutoff
class of a constant is zero, since its translated truncation at γ is the zero series.
The degenerate case #
The values ∂(0)(γ) of the zero series are zero.
The Leibniz rule at the zero element: both sides of principalSubringDerivation_mul vanish.