The native chart and its unit

The cumulative coordinates give a bijection from FinalCone to all natural three-space. Conversion to natural numbers occurs after proving nonnegativity.

Theorem 1.4 (old_zero_outside).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.old_zero_outside

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.old_zero_outside (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite Laurent expression vanishes outside FinalCone by its signed exponent balances.

Definition 1.5 (nativeChart).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.nativeChart

Formalization. D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.nativeChart (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient at (r,s,t) is the numerator coefficient at (r,s-r,t-s) when r<=s<=t, and zero otherwise.

Theorem 1.6 (old_coefficient_chart_sum).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.old_coefficient_chart_sum

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.old_coefficient_chart_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

At every decoded native index, the Laurent coefficient is the sum on its original finite fiber of the weights times the nativeChart coefficient at (n0-j-h,n1-q-l,n2).

Theorem 1.7 (native_chart_factorization).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.native_chart_factorization

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.native_chart_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under x=XYZ,y=YZ,z=Z, the literal six factors x^k y^k (x+y)^k (x+y+z)^A (y+z)^C z^D factor as X^k Y^(3k) Z^(3k+A+C+D) times (1+X)^k (1+Y+XY)^A (1+Y)^C in every commutative ring.

Definition 1.8 (chartUnitSeries).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.chartUnitSeries

Formalization. D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.chartUnitSeries (✓ std3).

Source. Repository-derived.

Commentary.

The product (1+X)^k (1+Y+XY)^a0 (1+Y)^a1 has constant coefficient one.

Definition 1.9 (chartUnit).

Lean statement: D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.chartUnit

Formalization. D5/S3/VertexAlgebra/FormalSeries/ThreeFieldFinalCone.chartUnit (✓ std3).

Source. Repository-derived.

Commentary.

This series is a unit over any commutative ring, with inverse supplied by MvPowerSeries.invOfUnit.