Golden Desubstitution Depth

Abstract

Measure golden desubstitution paths exactly and decode the resulting terminal digits.

Theorem 1.1 (Exact desubstitution path length).

$$\forall nmr\in \mathbb{N},\left(\exists xs,length(xs)=r\wedge \mathrm{IsChain}(\mathrm{desubStep}n,xs)\wedge \mathrm{getLast}(n,xs)=m\right)⟺\left(m\ne 0\vee r=0\right)\wedge \mathrm{wdigits}(n)=\mathrm{map}(k\mapsto k+r,\mathrm{wdigits}(m))$$

Proof. Machine-checked in Lean as D5/S1/Words/Powers/GoldenDesubstitutionDepth.golden_desubstitution_exact_length_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A nonzero endpoint admits exactly the number of steps recorded by the uniform Zeckendorf shift; zero is permitted only at depth zero.

Theorem 1.2 (Normal form is the closed shifted-digit decode).

$$\forall n\in \mathbb{N},\mathrm{nf}(\mathrm{desubStep},\mathrm{desubStepTermination},\mathrm{desubStepLocalConfluence},n)=\mathrm{decode}(\mathrm{map}(k\mapsto k-shift,\mathrm{wdigits}(n))$$

Proof. Machine-checked in Lean as D5/S1/Words/Powers/GoldenDesubstitutionDepth.golden_desubstitution_nf_eq_wdigits_decode (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unique terminal is obtained by shifting every occupied Fibonacci index down until the least digit reaches its floor, with zero handled separately.

References

• Truth anchor: D5/S1/Words/Powers/GoldenDesubstitutionDepth.golden_desubstitution_exact_length_iff
• Truth anchor: D5/S1/Words/Powers/GoldenDesubstitutionDepth.golden_desubstitution_nf_eq_wdigits_decode
• Dependency: D5/S0/Rewriting/NormalFormFunction
• Dependency: D5/S1/Words/Powers/GoldenDesubstitutionZeckendorf