Silver Pell arithmetic and convergent periods

Abstract

Pell approximation estimates and convergent-period constructions for the silver slope.

Theorem 1.1 (The signed Pell error).

$$\forall k\in \mathbb{N},\mathrm{real}(P(k+1))\cdot \mathrm{silverSlope}()-\mathrm{real}(P(k))={\left(-1\right)}^k\cdot \mathrm{silverSlope}({)}^{k+1}$$

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silverPell_error_formula (✓ std3). ∎

Citation. J. Peltomäki (2020). Abelian periods of factors of Sturmian words. DOI: 10.1016/j.jnt.2020.04.007. URL: https://arxiv.org/abs/1905.06138.

Commentary.

The error alternates in sign and its magnitude is the next power of the slope. The operators real and integer denote canonical numeric coercions.

Theorem 1.2 (The adjacent Pell determinant).

$$\forall k\in \mathbb{N},\mathrm{integer}(P(k+1+1))\cdot \mathrm{integer}(P(k))-\mathrm{integer}(P(k+1){)}^2={\left(-1\right)}^{k+1}$$

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silverPell_determinant (✓ std3). ∎

Citation. J. Peltomäki (2020). Abelian periods of factors of Sturmian words. DOI: 10.1016/j.jnt.2020.04.007. URL: https://arxiv.org/abs/1905.06138.

Commentary.

Consecutive denominators and numerators form a unimodular pair. The operators real and integer denote canonical numeric coercions.

Theorem 1.3 (Smaller denominators have larger error).

$$\forall k\in \mathbb{N},\forall m\in \mathbb{N},\forall z\in \mathbb{Z},\left(0<m\wedge m<P(k+1+1)\right)\Rightarrow \mathrm{silverSlope}({)}^{k+1}\le \left|\mathrm{real}(m)\cdot \mathrm{silverSlope}()-\mathrm{real}(z)\right|$$

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_best_approximation (✓ std3). ∎

Citation. J. Peltomäki (2020). Abelian periods of factors of Sturmian words. DOI: 10.1016/j.jnt.2020.04.007. URL: https://arxiv.org/abs/1905.06138.

Commentary.

Every positive denominator below q at index k+1 has error at least alpha to the power k+1. The operators real and integer denote canonical numeric coercions.

Theorem 1.4 (The noncandidate approximation gap).

$$\forall k\in \mathbb{N},\forall m\in \mathbb{N},\forall z\in \mathbb{Z},\left(P(k+1+1)\le m\wedge \left(m<P(k+2+1)\wedge \left(m\ne P(k+1+1)\wedge \left(m\ne 2\cdot P(k+1+1)\wedge m\ne P(k+1+1)+P(k+1)\right)\right)\right)\right)\Rightarrow \mathrm{silverSlope}({)}^{k+2}+\mathrm{silverSlope}({)}^{k+1}\le \left|\mathrm{real}(m)\cdot \mathrm{silverSlope}()-\mathrm{real}(z)\right|$$

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_gap_approximation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Between successive Pell denominators, the three distinguished candidates are the only exceptions to the larger error bound. The operators real and integer denote canonical numeric coercions.

Theorem 1.5 (The exact phase mass).

$$\forall k\in \mathbb{N},\left(\mathrm{real}(P(k+1+1))+\mathrm{silverSlope}()\cdot \mathrm{real}(P(k+1))\right)\cdot \mathrm{silverSlope}({)}^{k+1}=1$$

Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_phase_mass (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Pell recurrence and alpha squared plus twice alpha equals one give a constant phase mass. The operators real and integer denote canonical numeric coercions.

References

• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silverPell_determinant
• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silverPell_error_formula
• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_best_approximation
• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_gap_approximation
• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic.silver_phase_mass
• Dependency: D5/S1/Words/Mechanical/SilverSlopeAbelianPeriodDefs
• Dependency: D5/S1/Words/Mechanical/UnimodularApproximationBound