Aperiodicity of the projected gap sequence for irrational slopes

This file formalizes the aperiodicity proposition of the companion paper "Period lengths of one-dimensional rational cut-and-project sequences", Section "The Irrational Case". For positive irrational slope a and window parameter ω > 0, the projected gap sequence on the accepted lattice points has no finite period.

The proof has three steps:

1. The physical projection tildeP(x,y) = x + a*y is injective on ℤ².
2. A finite period of the gap sequence lifts to a non-zero translation v ∈ ℤ² that preserves the accepted set A.
3. Such a translation must induce a non-zero internal shift τ that preserves W ∩ s(ℤ²); Kronecker density on ℝ rules this out, forcing v = 0 and contradicting Step 2.

Section A. Notation and accepted set

def CutAndProject.Irrational.tildeP (a : ℝ) : ℤ × ℤ → ℝ

Physical (signed-position) projection used in the irrational case: tildeP(x,y) = x + a*y.

Equations

• CutAndProject.Irrational.tildeP a z = ↑z.1 + a * ↑z.2

def CutAndProject.Irrational.sInternal (a : ℝ) : ℤ × ℤ → ℝ

Internal coordinate: s(x,y) = y - a*x.

Equations

• CutAndProject.Irrational.sInternal a z = ↑z.2 - a * ↑z.1

def CutAndProject.Irrational.W (a ω : ℝ) : Set ℝ

Internal window W = [-a*ω, ω].

Equations

• CutAndProject.Irrational.W a ω = Set.Icc (-(a * ω)) ω

def CutAndProject.Irrational.acceptedSet (a ω : ℝ) : Set (ℤ × ℤ)

Accepted lattice points: those whose internal coordinate lies in W.

Equations

• CutAndProject.Irrational.acceptedSet a ω = {z : ℤ × ℤ | CutAndProject.Irrational.sInternal a z ∈ CutAndProject.Irrational.W a ω}

Section B. Step 1: tildeP is injective on ℤ²

theorem CutAndProject.Irrational.tildeP_injective (a : ℝ) (ha : Irrational a) : Function.Injective (tildeP a)

Section C. Kronecker density of ℤ + a·ℤ

theorem CutAndProject.Irrational.dense_internal_image (a : ℝ) (ha : Irrational a) : Dense (Set.range (sInternal a))

For irrational a, the set {n - a*m : m, n ∈ ℤ} is dense in ℝ.

Section D. Local finiteness of the projected accepted set

theorem CutAndProject.Irrational.accepted_preimage_finite (a ω : ℝ) (hω : 0 < ω) (b₁ b₂ : ℝ) : {z : ℤ × ℤ | z ∈ acceptedSet a ω ∧ tildeP a z ∈ Set.Icc b₁ b₂}.Finite

The preimage in ℤ² of any bounded interval, intersected with the accepted set, is finite.

Proof sketch. For (x, y) in the set we have s := y - a*x ∈ [-a*ω, ω] and p := x + a*y ∈ [b₁, b₂]. Inverting the linear system gives x = (p - a*s)/(1+a²) and y = (a*p + s)/(1+a²), so both x and y are bounded by an explicit real constant. Since x, y : ℤ lie in a bounded subset of ℝ, they lie in a finite box.

Section E. Bi-infinite unboundedness

theorem CutAndProject.Irrational.tildeP_image_unbounded_above (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (M : ℝ) : ∃ z ∈ acceptedSet a ω, M < tildeP a z

The unboundedness-above main theorem.

theorem CutAndProject.Irrational.tildeP_image_unbounded_below (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (M : ℝ) : ∃ z ∈ acceptedSet a ω, tildeP a z < M

The unboundedness-below main theorem.

Section F. ℤ-enumeration of the projected accepted set

API lemmas for unfolding the Section A definitions.

@[simp]

theorem CutAndProject.Irrational.tildeP_apply (a : ℝ) (m n : ℤ) : tildeP a (m, n) = ↑m + a * ↑n

@[simp]

theorem CutAndProject.Irrational.sInternal_apply (a : ℝ) (m n : ℤ) : sInternal a (m, n) = ↑n - a * ↑m

@[simp]

theorem CutAndProject.Irrational.mem_W_iff (a ω x : ℝ) : x ∈ W a ω ↔ -(a * ω) ≤ x ∧ x ≤ ω

@[simp]

theorem CutAndProject.Irrational.mem_acceptedSet_iff (a ω : ℝ) (z : ℤ × ℤ) : z ∈ acceptedSet a ω ↔ sInternal a z ∈ W a ω

def CutAndProject.Irrational.projectedSet (a ω : ℝ) : Set ℝ

The image of the accepted set under the projection.

Equations

• CutAndProject.Irrational.projectedSet a ω = CutAndProject.Irrational.tildeP a '' CutAndProject.Irrational.acceptedSet a ω

noncomputable def CutAndProject.Irrational.enumerate (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) : ℤ ≃o ↑(projectedSet a ω)

Bi-infinite enumeration of the projected accepted set. The forward map enumerate i is the i-th projected lattice point.

Equations

• CutAndProject.Irrational.enumerate a ω ha ha_pos hω = orderIsoIntOfLinearSuccPredArch.symm

Section G. Gap sequence and periodicity

noncomputable def CutAndProject.Irrational.ell (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (i : ℤ) : ℝ

The i-th projected point (= ℓ_i in the paper).

Equations

• CutAndProject.Irrational.ell a ω ha ha_pos hω i = ↑((CutAndProject.Irrational.enumerate a ω ha ha_pos hω) i)

noncomputable def CutAndProject.Irrational.gap (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (i : ℤ) : ℝ

The i-th gap g_i := ℓ_{i+1} - ℓ_i.

Equations

• CutAndProject.Irrational.gap a ω ha ha_pos hω i = CutAndProject.Irrational.ell a ω ha ha_pos hω (i + 1) - CutAndProject.Irrational.ell a ω ha ha_pos hω i

def CutAndProject.Irrational.IsGapPeriod (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (lam : ℕ) : Prop

The gap sequence has period λ.

Equations

• One or more equations did not get rendered due to their size.

theorem CutAndProject.Irrational.ell_strictMono (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) : StrictMono (ell a ω ha ha_pos hω)

The enumeration is strictly monotone, so ℓ is strictly increasing.

theorem CutAndProject.Irrational.gap_pos (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (i : ℤ) : 0 < gap a ω ha ha_pos hω i

Each gap is strictly positive.

Section H. Step 2: a finite period lifts to a lattice translation

theorem CutAndProject.Irrational.period_lifts_to_lattice_translation (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (lam : ℕ) (hp : IsGapPeriod a ω ha ha_pos hω lam) : ∃ (v : ℤ × ℤ), v ≠ 0 ∧ 0 < tildeP a v ∧ ∀ z ∈ acceptedSet a ω, z + v ∈ acceptedSet a ω

Step 2 of Proposition 1. If the gap sequence has finite period λ, there is a non-zero lattice translation v with tildeP v > 0 that preserves acceptedSet.

Section I. Step 3: a non-trivial lattice translation cannot

preserve the accepted set 

theorem CutAndProject.Irrational.lattice_translation_must_be_zero (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) (v : ℤ × ℤ) (hv_inv : ∀ z ∈ acceptedSet a ω, z + v ∈ acceptedSet a ω) : v = 0

Step 3 of Proposition 1. If v ∈ ℤ² preserves acceptedSet under addition, then v = 0.

Section J. Main theorem: aperiodicity for irrational slope

theorem CutAndProject.Irrational.prop_irrational (a ω : ℝ) (ha : Irrational a) (ha_pos : 0 < a) (hω : 0 < ω) : ¬∃ (lam : ℕ), IsGapPeriod a ω ha ha_pos hω lam

Aperiodicity (paper: prop:irrational, Section "The Irrational Case"). For a ∈ ℝ_{>0} ∖ ℚ and ω > 0, the projected gap sequence has no finite period.

theorem CutAndProject.Irrational.tildeP_injOn_acceptedSet (a ω : ℝ) (ha : Irrational a) : Set.InjOn (tildeP a) (acceptedSet a ω)

Companion injectivity claim (prop:irrational). Because tildeP is injective on ℤ² (Step 1, tildeP_injective), it is in particular injective when restricted to acceptedSet. This formalizes the paper's remark that "the multiset and set conventions coincide" in the irrational case: the projected accepted points have no duplicates.