Expansion Engine

Abstract

Multiplying by the frontier base is an integer map on coordinate pairs, which is the algebraic engine of any expansion argument at that base.

Every element of the ring generated by the base is a coordinate pair against one and the base. Because the base squares to itself plus three, multiplying by it sends the pair to three times the second coordinate, paired with the sum of the two. Subtracting a digit changes only the first coordinate, so a greedy step stays integral.

Theorem 1.1 (The frontier expansion engine).

$$\left(\left(\forall p\in R,q\in R,betaThirteen\cdot \left(p+q\cdot betaThirteen\right)=3\cdot q+\left(p+q\right)\cdot betaThirteen\right)\wedge \left(2<betaThirteen\wedge betaThirteen<3\right)\right)\wedge \left(\left(0<betaThirteen-2\wedge betaThirteen-2<1\right)\wedge \left(0<3-betaThirteen\wedge 3-betaThirteen<1\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Tower/NonPisotFrontier/ExpansionEngine.frontier_expansion_engine (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two window facts pin the first two greedy digits of one at two and zero. The expansion itself, and the growth of the gap alphabet that the source reports, are not proved here.

References

• Truth anchor: D5/S0/Tower/NonPisotFrontier/ExpansionEngine.frontier_expansion_engine
• Dependency: D5/S0/Tower/NonPisotFrontier/BetaThirteen