Addition on a support with an accumulation point #
The closed support generated by the negative reciprocal sequence has an accumulation point at zero. Addition on its square is proper and has a finite noninjective fiber. This excludes both a finite-support substitute for well-ordering and an injectivity substitute for finite fibers. The empty-support case separately exercises the degenerate domain.
The increasing negative reciprocal sequence converging to zero.
Equations
- Tests.PWOAddition.negRecip n = -(1 / (↑n + 1))
Instances For
The test support is not discrete: zero is an accumulation point.
Empty supports are permitted by the proper-map statement.
A Hahn series with coefficient one on the negative reciprocal sequence and zero elsewhere.
Equations
- Tests.PWOAddition.accumulatingSeries = { coeff := fun (x : ℝ) => if x ∈ Set.range Tests.PWOAddition.negRecip then 1 else 0, isPWO_support' := Tests.PWOAddition.accumulatingSeries._proof_1✝ }
Instances For
A genuine infinite Hahn support has positive rank at zero and value at least omega.
Zero and strictly negative monomials vanish, but a nonzero constant has value one.
Weak truncation retains the cutoff monomial; strict truncation deletes it.
A cutoff at an actual accumulation point preserves its positive rank.
The finite convolution fiber contains a limit pair absent from both raw supports.
Omitting that limit pair would falsely give value zero for this actual square.
The finite convolution error has value zero on the accumulating support fixture.
The natural-product upper bound applies to the nonzero infinite-support square.
Equal nonzero values can cancel completely; the unequal-values hypothesis is necessary.
An ordinary constant cannot cancel the accumulating part of the test series.
Value one permits an actual infinite tail bounded away from zero.
A value-one factor with infinite support preserves the accumulating-series value.
The Leibniz bound is strictly smaller than the predicted square value on an actual infinite support; this excludes a finite-support or constant-factor substitute.
The eventual qualifier is essential: negative monomials produce a value-one remainder at an earlier negative cutoff, although both original values are zero.
Zero-input API smoke test; this does not distinguish the multiplicities.
The ordinary coefficient distinguishes the square rule from the wrong coefficient-one rule.
The power estimate on an actual accumulating support, for every exponent including zero. The positive Cantor–Bendixson rank excludes a finite-support or ordinary-constant substitute.
The accumulating fixture has rank exactly one in value, not merely a positive lower bound.
The pure-power cancellation theorem proves every power value on an actual infinite support. Residual cutoffs have value one, so value-one multiplication closes the smaller-product hypothesis.
The two-factor cancellation theorem also closes on the opposite-sign infinite factors. Its residual-point hypothesis uses the independently proved pure-square value.
Unequal positive ranks, mixed signs, and a nonzero constant term are all retained.
The germ quotient is not the ordinary-coefficient quotient: this series has coefficient zero at zero and still gives a nonzero germ.
A nonzero negative monomial vanishes in the germ quotient, excluding the zero ideal.
The accumulating series gives a genuine degree-one class whose square is nonzero.
The accumulating degree-one class has nonzero derivative, excluding the zero-map substitute.
The additive derivative sends zero to zero.
Every grade-zero class has zero derivative.
The grade-zero scalar map is an actual coefficient-field equivalence.
The standard derivation and additive truncation map agree.
The accumulating series exercises both terms of the graded product rule.
Dropping one of the two square-rule terms is false for the actual accumulating series.
The literal pointwise assembly conclusion is unsatisfiable at an accumulating rank level: prescribing the constant one at every rank-zero point of the accumulating support forces a coefficient one at cutoffs arbitrarily close to zero, while the required bound at the nonpositive noncenter zero forces the support strictly below zero. The pointwise degree hypothesis of the top-rank assembly therefore cannot be dropped.
On the accumulating fixture, a degree-zero cofactor of the series itself makes every translated truncation have degree strictly below one. The zero cofactor is not a substitute, because the original series keeps degree one at cutoff zero.
Two distinct series lift one nonzero degree-one class; their difference has bottom degree. Lifting detects the class, not the series.
Without independence of the lifted classes, a nonzero polynomial with small weights can evaluate to bottom degree: the injectivity hypothesis of the uniqueness clause is not removable.
The polynomial of a series modulo bounded series, run below degree one with no generators: the machinery extracts the constant term, and only the correct constant works.