Audited examples for the public statement

These examples exercise the derivative convention, coefficient indexing, monicity, genuine parameter dependence, nonconstant units, and the n = 0 and d = 0 semantics of the public interface.

theorem ClassicalComplexWPT.exactOrder_monomial (n d : ℕ) : ExactOrderInLastVariable (fun (x : Ambient n) => x.2 ^ d) d

The distinguished monomial has exact order d; its d-th derivative is d!.

theorem ClassicalComplexWPT.isWeierstrassPreparation_monomial (n d : ℕ) : IsWeierstrassPreparation (fun (x : Ambient n) => x.2 ^ d) d (fun (x : Fin d) (x_1 : Base n) => 0) fun (x : Ambient n) => 1

The monomial is prepared by zero lower coefficients and the constant unit one.

theorem ClassicalComplexWPT.exactOrder_pow_add_first (d : ℕ) : ExactOrderInLastVariable (fun (x : Ambient 1) => x.2 ^ d + x.1 0) d

For every degree, w^d + z₀ has exact distinguished-variable order d.

theorem ClassicalComplexWPT.isWeierstrassPreparation_pow_add_first (d : ℕ) (hd : 0 < d) : IsWeierstrassPreparation (fun (x : Ambient 1) => x.2 ^ d + x.1 0) d (fun (i : Fin d) (z : Base 1) => if ↑i = 0 then z 0 else 0) fun (x : Ambient 1) => 1

For positive degree, w^d + z₀ has the advertised parameter-dependent prepared form.

theorem ClassicalComplexWPT.isWeierstrassPreparation_nonconstantUnit : IsWeierstrassPreparation (fun (x : Ambient 1) => (1 + x.2) * (x.2 + x.1 0)) 1 (fun (x : Fin 1) (z : Base 1) => z 0) fun (x : Ambient 1) => 1 + x.2

A nonconstant unit times a prepared degree-one polynomial is still prepared.

theorem ClassicalComplexWPT.exactOrder_nonconstantUnit : ExactOrderInLastVariable (fun (x : Ambient 1) => (1 + x.2) * (x.2 + x.1 0)) 1

Its distinguished slice has exact order one.