Boundary-Pivot Transport

Abstract

Boundary pivots make the signed endpoint corrections of actual descent edges eventually periodic.

The BKS block mechanism supplies bounded edge corrections but does not by itself identify one finite family for every actual block. This owner follows the actual complementary letters at both endpoints through consecutive descent edges. Extremal choices make the next state deterministic, while retaining the left and right pivots as one paired state preserves their joint realization.

Definition 1.1 (A letter image contains an outside letter).

$$\mathrm{imageMeetsComplement}\left(g,Delta,a\right)⟺\exists t\in \mathrm{Fin}\left(Q\right),\neg (\mathrm{uniformLetter}\left(g,a,t\right)\in Delta)$$

Formalization. D5/S1/Recurrence/Raney/BoundaryPivotTransport.imageMeetsComplement (✓ std3).

Source. Repository-derived.

Acknowledgement. Yann Bugeaud, Dalia Krieger, and Jeffrey Shallit (2009). Morphic and Automatic Words: Maximal Blocks and Diophantine Approximation. URL: https://arxiv.org/abs/0808.2544v2.

Commentary.

For a Q-uniform morphism g, imageMeetsComplement(g,Delta,a) means that some offset in Fin(Q) has g(a)[offset] outside Delta. The existential offset is literal and is later extremized separately at the two boundaries.

Theorem 1.2 (Two actual edges transport both boundary pivots).

$$\mathrm{IsBksDescentStep}\left(Q,grand,parent\right)\wedge \mathrm{IsBksDescentStep}\left(Q,parent,child\right)\Rightarrow \mathrm{existsExtremalPivotsWithSignedEquations}\left(Q,grand,parent,child\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Raney/BoundaryPivotTransport.actual_boundary_pivot_transport_at_power (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Yann Bugeaud, Dalia Krieger, and Jeffrey Shallit (2009). Morphic and Automatic Words: Maximal Blocks and Diophantine Approximation. URL: https://arxiv.org/abs/0808.2544v2.

Commentary.

Fix q>0 and Q=P^q together with the Q-uniform fixed-word and support-stability facts. Given actual edges grandparent->parent and parent->child, the left boundary is represented by the outside exit at parent.first-1 and the right boundary by the outside exit at parent.last+1. On the left choose the rightmost image entry whose own image meets the complement; on the right choose the leftmost. The theorem returns exit, entry, and next-exit offsets in Fin(Q), their letters and extremality conditions, and the exact signed equations grand.first-Qparent.first=Qentry+nextExit+1-Q*(exit+1) and (grand.last+1)-Q*(parent.last+1)=Qentry+nextExit-Qexit.

Definition 1.3 (The paired outside-letter state).

$$\mathrm{actualBksPivotState}\left(Q,w,(i,j)\right)=(w\left(\mathrm{div}\left(i-1,Q\right)\right),w\left(\mathrm{div}\left(j+1,Q\right)\right))$$

Formalization. D5/S1/Recurrence/Raney/BoundaryPivotTransport.actualBksPivotState (✓ std3).

Source. Repository-derived.

Acknowledgement. Yann Bugeaud, Dalia Krieger, and Jeffrey Shallit (2009). Morphic and Automatic Words: Maximal Blocks and Diophantine Approximation. URL: https://arxiv.org/abs/0808.2544v2.

Commentary.

For endpoints (i,j), the state is the pair of word letters at quotient indices (i-1)/Q and (j+1)/Q. Natural subtraction gives the boundary-safe value at i=0, although descent edges themselves are late. Keeping the pair together is essential: separate left and right optima would not certify a common block.

Theorem 1.4 (Paired states determine the next state and correction).

$$\mathrm{twoEdgeWindows}\left(Q,blocks,i,j\right)\Rightarrow (((\mathrm{state}\left(i\right)=\mathrm{state}\left(j\right))\Rightarrow (\mathrm{state}\left(i+1\right)=\mathrm{state}\left(j+1\right)))\wedge ((\mathrm{state}\left(i\right)=\mathrm{state}\left(j\right)\wedge \mathrm{state}\left(i+1\right)=\mathrm{state}\left(j+1\right))\Rightarrow (\mathrm{first}\left(\mathrm{blocks}\left(i+2\right)\right)-Q\cdot \mathrm{first}\left(\mathrm{blocks}\left(i+1\right)\right)=\mathrm{first}\left(\mathrm{blocks}\left(j+2\right)\right)-Q\cdot \mathrm{first}\left(\mathrm{blocks}\left(j+1\right)\right)\wedge \mathrm{last}\left(\mathrm{blocks}\left(i+2\right)\right)+1-Q\cdot \left(\mathrm{last}\left(\mathrm{blocks}\left(i+1\right)\right)+1\right)=\mathrm{last}\left(\mathrm{blocks}\left(j+2\right)\right)+1-Q\cdot \left(\mathrm{last}\left(\mathrm{blocks}\left(j+1\right)\right)+1\right))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Raney/BoundaryPivotTransport.actual_bks_pivot_state_dynamics_at_power (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Yann Bugeaud, Dalia Krieger, and Jeffrey Shallit (2009). Morphic and Automatic Words: Maximal Blocks and Diophantine Approximation. URL: https://arxiv.org/abs/0808.2544v2.

Commentary.

For one fixed q and a sequence of blocks, state(k) is the paired pivot state of block(k+1), and validAt(k) requires the actual descent edges block(k+2)->block(k+1) and block(k+1)->block(k). Two valid windows with equal current states have equal following states. If their current and following states agree, their upper-edge signed displacements block(k+2).first-Q*block(k+1).first and the corresponding last+1 displacement are equal. The proof uses the extremal offsets returned by actual_boundary_pivot_transport_at_power, not an unrealized product of marginal choices.

Theorem 1.5 (Signed endpoint displacements are eventually periodic).

$$\exists q\in \mathbb{N},0<q\wedge \forall Delta\in FinsetA,\forall blocks\in \mathrm{Seq}\left(\mathrm{Prod}\left(\mathbb{N},\mathbb{N}\right)\right),(\forall k\in \mathbb{N},\mathrm{IsBksDescentStep}\left(P^q,\mathrm{blocks}\left(k+1\right),\mathrm{blocks}\left(k\right)\right))\Rightarrow (\exists N0\in \mathbb{N},\exists t\in \mathbb{N},0<t\wedge \forall k\in \mathbb{N},(N0\le k)\Rightarrow (\mathrm{first}\left(\mathrm{blocks}\left(k+t+1\right)\right)-Q\cdot \mathrm{first}\left(\mathrm{blocks}\left(k+t\right)\right)=\mathrm{first}\left(\mathrm{blocks}\left(k+1\right)\right)-Q\cdot \mathrm{first}\left(\mathrm{blocks}\left(k\right)\right)\wedge \mathrm{last}\left(\mathrm{blocks}\left(k+t+1\right)\right)+1-Q\cdot \left(\mathrm{last}\left(\mathrm{blocks}\left(k+t\right)\right)+1\right)=\mathrm{last}\left(\mathrm{blocks}\left(k+1\right)\right)+1-Q\cdot \left(\mathrm{last}\left(\mathrm{blocks}\left(k\right)\right)+1\right)))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Raney/BoundaryPivotTransport.exists_eventually_periodic_actual_bks_signed_displacements (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Yann Bugeaud, Dalia Krieger, and Jeffrey Shallit (2009). Morphic and Automatic Words: Maximal Blocks and Diophantine Approximation. URL: https://arxiv.org/abs/0808.2544v2.

Commentary.

For every infinite sequence of actual descent edges at the selected power Q, there are N and a positive period t such that for all k>=N both corrections repeat after t: the left correction is block(k+1).first-Q*block(k).first, and the right correction uses last+1 in the same way. Finite paired states force a repeated state; deterministic transition propagates it, and equal adjacent state pairs give equal corrections. The conclusion is about signed Int displacements, so boundary borrowing is preserved.

References

• Truth anchor: D5/S1/Recurrence/Raney/BoundaryPivotTransport.actualBksPivotState
• Truth anchor: D5/S1/Recurrence/Raney/BoundaryPivotTransport.actual_bks_pivot_state_dynamics_at_power
• Truth anchor: D5/S1/Recurrence/Raney/BoundaryPivotTransport.actual_boundary_pivot_transport_at_power
• Truth anchor: D5/S1/Recurrence/Raney/BoundaryPivotTransport.exists_eventually_periodic_actual_bks_signed_displacements
• Truth anchor: D5/S1/Recurrence/Raney/BoundaryPivotTransport.imageMeetsComplement
• Dependency: D5/S1/Recurrence/Raney/MaximalBlockDescent