Lowest-Position Monotonicity

Abstract

The lowest nonzero signed position never decreases on a tight legal cut.

Theorem 1.1 (The literal minimum-position transition law).

$$\forall n\in \mathbb{N},\forall j\in \mathbb{N},\left(\left(\left(\mathrm{classS}\left(n\right)\wedge j<n\right)\wedge \mathrm{Palindrome}\left(\mathrm{ofFn}\left(i:\mathrm{Fin}\left(Nat.sub\left(n,j\right)\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(j+\mathrm{val}\left(i\right)\right)\right)\right)\right)\wedge \mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(j+1,2\right),\mathbb{Z}\right)\right)+1\right)\Rightarrow \left(j=0\vee \mathrm{padicValNat}\left(2,\mathrm{div}\left(n+1,2\right)\right)\le \mathrm{padicValNat}\left(2,\mathrm{div}\left(j+1,2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/TightCutLowestPosition.tight_cut_lowest_position (✓ std3). ∎

Source. Repository-derived.

Commentary.

A cut is tight when the minimum signed weight of the rounded half drops by exactly one. Complete cut realization excludes the invalid class mode. Lifting the base path to the minimum product gives a persistent flag for output nonzero digits emitted before any input nonzero digit. Its accepting potential bound zero excludes a true flag on a path with signed-weight drop one. Digit induction then yields the order of the first nonzero coefficients, and their literal dyadic valuations give the stated inequality. The zero endpoint is listed separately because its dyadic valuation is defined to be zero. div denotes natural integer quotient, and Nat.sub denotes truncated natural subtraction.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/TightCutLowestPosition.tight_cut_lowest_position
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseArithmetic
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseLowestPosition
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/CutRepresentation
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/SignedDigitValuation