Normalized coefficient contractions

Abstract

A strict improvement of coefficient agreement gives a unique normalized formal power-series fixed point.

Theorem 1.1 (A normalized contraction has a unique fixed point).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\forall step:\mathrm{PowerSeries}\left(R\right)\to \mathrm{PowerSeries}\left(R\right),(\forall f:\mathrm{PowerSeries}\left(R\right),(\mathrm{constantCoeff}\left(f\right)=1)⟹(\mathrm{constantCoeff}\left(\mathrm{step}\left(f\right)\right)=1))⟹((\forall d:\mathbb{N},\forall f:\mathrm{PowerSeries}\left(R\right),\forall g:\mathrm{PowerSeries}\left(R\right),(1\le d)⟹((\mathrm{constantCoeff}\left(f\right)=1)⟹((\mathrm{constantCoeff}\left(g\right)=1)⟹((\mathrm{Agree}\left(d,f,g\right))⟹(\mathrm{Agree}\left((d)+(1),\mathrm{step}\left(f\right),\mathrm{step}\left(g\right)\right))))))⟹(\exists f:\mathrm{PowerSeries}\left(R\right),(\mathrm{constantCoeff}\left(f\right)=1)\wedge ((f=\mathrm{step}\left(f\right))\wedge (\forall g:\mathrm{PowerSeries}\left(R\right),(\mathrm{constantCoeff}\left(g\right)=1)⟹((g=\mathrm{step}\left(g\right))⟹(g=f))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.exists_unique_fixed (✓ std3). ∎

Source. Repository-derived.

Commentary.

The nth coefficient is read from the nth iterate. Improving agreement stabilizes these coefficients; induction proves the fixed-point identity and uniqueness.

Theorem 1.2 (Geometric zero).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\mathrm{constantCoeff}\left((\mathrm{geometric}:\mathrm{PowerSeries}\left(R\right))\right)=0$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The geometric series X times mk 1 has constant coefficient zero.

Theorem 1.3 (Geometric one).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\mathrm{coeff}\left(1,(\mathrm{geometric}:\mathrm{PowerSeries}\left(R\right))\right)=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coefficient of X in X times mk 1 is one.

Theorem 1.4 (Geometric coeff).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\forall n:\mathbb{N},(1\le n)⟹(\mathrm{coeff}\left(n,(\mathrm{geometric}:\mathrm{PowerSeries}\left(R\right))\right)=1)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_coeff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every positive coefficient of the geometric series is one.

Theorem 1.5 (Geometric mul).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],((\mathrm{geometric}:\mathrm{PowerSeries}\left(R\right)))\cdot ((1)-(X))=X$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying the geometric series by one minus X gives X.

Theorem 1.6 (Map subst pow).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\forall S:Type,[\mathrm{CommRing}\left(S\right)],\forall hom:R{\to }^{+\ast }S,\forall f:\mathrm{PowerSeries}\left(R\right),\forall k:\mathbb{N},(k\ne 0)⟹(\mathrm{map}\left(hom,\mathrm{subst}\left((X{)}^k,f\right)\right)=\mathrm{subst}\left((X{)}^k,\mathrm{map}\left(hom,f\right)\right))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.map_subst_pow (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mapping coefficients along a ring homomorphism commutes with substitution by a positive power of X.

Theorem 1.7 (Geometric subst mul).

$$\forall R:Type,[\mathrm{CommRing}\left(R\right)],\forall k:\mathbb{N},(k\ne 0)⟹((\mathrm{subst}\left((X{)}^k,(\mathrm{geometric}:\mathrm{PowerSeries}\left(R\right))\right))\cdot ((1)-((X{)}^k))=(X{)}^k)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_subst_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Substituting X to a positive power in the geometric identity preserves multiplication.

References

• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.exists_unique_fixed
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_coeff
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_mul
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_one
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_subst_mul
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.geometric_zero
• Truth anchor: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction.map_subst_pow
• Dependency: D5/S1/Recurrence/Invariants/CompositionalIterateCongruence
• Dependency: D5/S1/Recurrence/Invariants/ScaledReversionCongruence
• Dependency: D5/S1/Recurrence/Invariants/UnitReversionSquareParity