Monic normalisation only rescales by a unit: the interpretation of
Norm.monic f over ℂ is associated to the interpretation of f.
Associated complex polynomials have the same root multiplicity at every point.
Over ℂ the root multiplicity of a gcd at each point is the minimum of
the root multiplicities of its arguments.
The monic normalisation of the executable gcd DensePoly.gcd f g divides
both f and g in the executable polynomial ring.
The monic executable gcd interprets to a nonzero complex polynomial whenever its first argument does.
The executable monic gcd tracks complex root multiplicities: at every
z, the interpretation of Norm.monic (DensePoly.gcd f g) has root
multiplicity the minimum of those of f and g.
For an exact executable division the interpretations reconstruct the
dividend: interpreting dividend / divisor and multiplying by the
interpreted divisor recovers the interpreted dividend.
An exact executable quotient of a semantically nonzero dividend is semantically nonzero.
Root multiplicities subtract across the monic exact quotient: at every
z, the multiplicity of Norm.monic (dividend / divisor) is the dividend's
multiplicity minus the divisor's.
The monic normalisation of an exact quotient of a semantically nonzero dividend is semantically nonzero.
Loop invariant of Yun's algorithm tracked at one complex root z of
multiplicity r in the original input. Before emitting the component of
multiplicity k, the working polynomial w carries z simply exactly when
k ≤ r, and the repeated part carries the remaining multiplicity r - k.
- w_multiplicity : Polynomial.rootMultiplicity z (Norm.rawPolynomial levels w) = if k ≤ r then 1 else 0
Instances For
One Yun iteration preserves the invariant: replacing w by the monic
gcd with the repeated part and dividing that gcd out of the repeated part
advances the multiplicity counter from k to k + 1.
The component emitted at counter k carries z as a simple root exactly
when k is the multiplicity of z in the original input, and avoids z
otherwise.
The Yun setup establishes the invariant at counter 1: over a
characteristic-zero coefficient field, dividing the monic input by its gcd
with the derivative leaves each root exactly once, and the gcd retains the
remaining multiplicity.
A nonzero interpreted polynomial with a root has positive executable degree. Keeping this transport separate prevents the recursive Yun proof from re-elaborating the coefficient-field construction at every induction step.
The raw complex interpretation is coefficientwise mapping through the coefficient denotation homomorphism.
A semantically nonzero executable polynomial with a complex root has positive executable degree.
Entries already accumulated survive the rest of the Yun loop: the accumulator only grows.
Soundness of the Yun loop at one root: assuming the invariant, every
emitted component that vanishes at z is labelled with exactly the
multiplicity r of z in the original input.
Squarefreeness of the emitted components: assuming the invariant, every
component produced by the Yun loop carries z with multiplicity at most
one.
Completeness of the Yun loop at one root: with enough fuel, some emitted
component vanishes at z and is labelled with its multiplicity r.
The Yun loop only emits nonconstant components with positive multiplicity labels.
Multiplicity labels emitted by the Yun loop are strictly increasing and bounded by the starting counter plus the remaining fuel.
Every component emitted by the Yun loop is monic in the executable
sense: its raw leading coefficient is 1.
The multiplicity of any single root of a nonzero complex polynomial is bounded by its degree.
Every root of an emitted tower Yun component is a root of the input with the component's stored multiplicity.
Every root of a positive-degree tower polynomial occurs in an emitted Yun component at its exact multiplicity.
Every emitted Yun component has only simple roots over ℂ.
Every tower Yun component is monic in executable coordinates.
Every tower Yun component passes the executable squarefreeness test.
Distinct tower Yun components pass the executable coprimality test.
Root multiplicities scale linearly under powers of a nonzero complex polynomial.
Root multiplicities add across a product of nonzero complex polynomials.
Semantic interpretation turns the executable power Factor.polyPow into
the complex polynomial power.
The executable fold multiplying labelled component powers interprets to the product of interpreted component powers times the accumulator.
Multiplicity bookkeeping for the weighted Yun product: at every root z
of the input, the labels of the (squarefree, strictly ordered, jointly
complete) components weighted by their own multiplicities at z sum to the
input's multiplicity at z.
Every component emitted by Factor.yunRaw interprets to a monic complex
polynomial.
The powered product of all tower Yun components reconstructs the monic input exactly.
The executable Yun decomposition always passes its full internal certificate check.