Prime-Axis W-Digit Tables

Abstract

Finite prime-indexed canonical W digits encode factorization exponents.

Theorem 1.1 (Finite prime-axis table and product decode).

$$\forall z\in \mathrm{PrimeAxisTable},(\forall p,\mathrm{CanonicalRaw}(z.\mathrm{digits}(p)))\wedge \mathrm{Finite}(\mathrm{support}(z.\mathrm{digits}))\wedge (\forall p,\mathrm{axisExponent}(z,p)=\sum _{k\in \mathrm{support}(z.\mathrm{digits}(p))}z.\mathrm{digits}(p,k)w(k))\wedge \mathrm{decodePrimeAxisTable}(z)=\prod _{p\in \mathrm{support}(z.\mathrm{digits})}{p}^{\mathrm{axisExponent}(z,p)}$$

Proof. Machine-checked in Lean as D5/S1/Digit/PrimeAxisTable.prime_axis_table_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

An outer finitely supported table assigns canonical binary nonadjacent W digits to prime axes. The theorem exposes finite global support, each W-weighted exponent sum, and the corresponding finite prime-power product decode.

References

• Truth anchor: D5/S1/Digit/PrimeAxisTable.prime_axis_table_spec
• Dependency: D5/S1/Digit/Raw