Singular-window separation and packing

Abstract

Singular-window separation and packing

Theorem 1.1 (Singular starts are separated).

$$\forall k\in \mathbb{N},\forall u\in \mathbb{N},\forall v\in \mathbb{N},\left(1\le k\wedge \left(u<v\wedge \left(\mathrm{count}(true,\mathrm{lowerMechanicalFactor}(\mathrm{silverSlope}(),0,P(k+1),u))\ne P(k)\wedge \mathrm{count}(true,\mathrm{lowerMechanicalFactor}(\mathrm{silverSlope}(),0,P(k+1),v))\ne P(k)\right)\right)\right)\Rightarrow P(k+2)\le v-u$$

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

Source. Repository-derived.

Commentary.

Two exceptional q-window counts place their phases in an interval of length alpha to the power k+1. A closer return contradicts the best approximation bound. Canonical coercions are denoted real and integer. Natural subtraction is truncated at zero; natMod is natural remainder.

Theorem 1.2 (Failure of period q forces a long word).

$$\forall k\in \mathbb{N},\forall n\in \mathbb{N},\forall i\in \mathbb{N},\left(1\le k\wedge \left(P(k+1)<n\wedge \neg (\mathrm{AbelianPeriod}(\mathrm{lowerMechanicalFactor}(\mathrm{silverSlope}(),0,n,i),P(k+1)))\right)\right)\Rightarrow \left(P(k+1)-1\right)\cdot P(k+2)+P(k+1)\le n$$

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

Source. Repository-derived.

Commentary.

Every residue modulo q needs a singular full window. Their separated starts give the length bound by an injection into quotient intervals. Canonical coercions are denoted real and integer. Natural subtraction is truncated at zero; natMod is natural remainder.

References

• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianSingularPacking.silver_no_q_length
• Truth anchor: D5/S1/Words/Mechanical/SilverSlopeAbelianSingularPacking.silver_singular_separation
• Dependency: D5/S1/Words/Mechanical/SilverSlopeAbelianPellArithmetic