Period lengths of rational cut-and-project gap sequences #
For coprime α, β : ℕ and a window parameter ω ≥ 0, the accepted lattice
points (x, y) ∈ ℤ² with y ∈ [(α/β)(x-ω), (α/β)x + ω] project onto the
line f(x) = (α/β)x; sorting the projections yields a periodic sequence of
consecutive gaps. Writing N = ⌊ωα⌋ + ⌊ωβ⌋ + 1 and D = α² + β², this file
proves the closed-form minimal periods for the residue model of that
construction: the paper's strip-to-residue reduction — enumerate N
consecutive residue classes modulo D under the multiplier m = -α·β⁻¹ and
sort the hits — is taken here as the definition of the gap sequence
(differenceSequenceUnit), not derived from the lattice points. For it,
counting with multiplicity the period is N if D ∤ N and N / D if
D ∣ N (main_theorem_geometric_concrete), while discarding multiplicities
it is N if N < D and 1 otherwise (set_main_theorem_geometric_concrete).
The geometric data is threaded through the GeometricProjection typeclass,
whose concrete instance GeometricProjectionConcrete discharges its four
hypotheses; the identification of the residue model with the sorted lattice
projections is not formalised here. The irrational-slope case
(LeanPool.CutAndProject.Irrational) is built from the lattice directly.
The geometric multiplier m = -α · β⁻¹, as a unit of ZMod (α ^ 2 + β ^ 2).
Equations
- CutAndProject.multiplier α β h = -1 * CutAndProject.alphaUnit α β h * (CutAndProject.betaUnit α β h)⁻¹
Instances For
countHits D r0 N x counts the number of times the residue x (modulo D) is hit
by the arithmetic progression r0, r0+1, ..., r0+N-1 of length N.
The residue distribution theorem (residue_distribution, Lemma 4.3 in the
paper) describes the multiset of multiplicities.
Equations
- CutAndProject.countHits D r0 N x = {i ∈ Finset.range N | ↑r0 + ↑i = x}.card
Instances For
countHitsUnit D u r0 N x is the unit-aware variant of countHits:
it counts how many i ∈ Finset.range N satisfy (u : ZMod D) * (r0 + i) = x.
This corresponds to the geometric residue map r ↦ m * r (mod D) from the
paper, where m = -α · β⁻¹ ∈ (ZMod D)ˣ is the multiplier introduced via
multiplier. For u = 1 it reduces to countHits (count_hits_unit_one);
in general it reduces to countHits after applying u⁻¹ to the target
residue (count_hits_unit_eq_count_hits).
Equations
- CutAndProject.countHitsUnit D u r0 N x = {i ∈ Finset.range N | ↑u * (↑r0 + ↑i) = x}.card
Instances For
Transfer lemma: counting hits of the multiplier-twisted progression
u * (r0 + i) against the target x equals counting hits of the plain
progression r0 + i against u⁻¹ * x. Multiplication by a unit is a
bijection of ZMod D, so the two counts agree pointwise.
Specialisation of count_hits_unit_eq_count_hits to u = 1:
the unit-aware count with trivial multiplier reduces to countHits.
Unit-aware analogue of residue_distribution (Lemma 4.3): the multiset of
multiplicities of countHitsUnit D u r0 N agrees with that of
countHits D r0 N. Multiplication by u : (ZMod D)ˣ is a bijection of
ZMod D, so the cardinalities of the level sets {x | count = k} are
preserved.
Unit-aware analogue of uniform_residue_distribution: in the degenerate
case D ∣ N, every residue class is hit exactly N / D times under the
multiplier-twisted progression u * (r0 + i).
The cyclic interval of length s based at x0: the image of {0, …, s - 1} under `i ↦ x0
- i
inZMod D`.
Equations
- CutAndProject.cyclicInterval D s x0 = Finset.image (fun (i : ℕ) => x0 + ↑i) (Finset.range s)
Instances For
Unit-aware analogue of heavy_set_is_cyclic_interval: under the unit-twisted
count countHitsUnit D u r0 N, the heavy residues are precisely those x
for which u⁻¹ * x lies in the cyclic interval describing the heavy residues
of the untwisted countHits D r0 N. Equivalently, the unit-twisted heavy
set is the image of the untwisted heavy cyclic interval under multiplication
by u.
Proof: direct corollary of the transfer lemma count_hits_unit_eq_count_hits
and heavy_set_is_cyclic_interval.
Lemma (Minimality): A cyclic interval of length s with 0 < s < D
cannot be invariant under any non-zero translation τ.
HasPeriodLength s L states that L is the least positive period of the sequence s.
Equations
- CutAndProject.HasPeriodLength s L = (CutAndProject.IsPeriod s L ∧ ∀ L' > 0, CutAndProject.IsPeriod s L' → L ≤ L')
Instances For
Abstract interface for the combinatorial residue model obtained by reducing
the cut-and-project geometry to the distribution of N consecutive residue
classes modulo D = α² + β². The four axioms are periodic-combinatorial
in nature; the geometric construction is not formalised from first
principles. Concrete instances are built from the geometric data via
GeometricProjectionConcrete.
Instances
Running total of countHits over Finset.range (x + 1): the number of projected points
with index in [0, x].
Equations
Instances For
The k-th sorted index: the least x whose cumulative hit count exceeds k.
Equations
- CutAndProject.V α β ω k = if h : ∃ (x : ℕ), k < CutAndProject.cumulativeHits α β ω x then Nat.find h else 0
Instances For
The i-th value of the sorted multiset of projected residues, extended D-periodically to
all of ℤ.
Equations
Instances For
The concrete difference sequence of the normalized residue model (u = 1).
differenceSequenceUnit with u = multiplier α β h is the residue-model
counterpart of the geometric gap sequence in the paper (the identification is
the paper's strip-to-residue reduction, stated as a definition here, not
proved); the two have the same period length but differ as sequences in
general.
Equations
- CutAndProject.differenceSequence α β ω i = CutAndProject.sortedMultiset α β ω (i + 1) - CutAndProject.sortedMultiset α β ω i
Instances For
Unit-aware concrete construction. cumulativeHitsUnit α β ω u x is the
total number of hits in the integer range [0, x] of the multiplier-twisted
arithmetic progression u * (r0 + i) for i ∈ [0, N). With u = 1 it
reduces to cumulativeHits (cumulative_hits_unit_one); with
u = multiplier α β h it realises the geometric residue map
c_{r0+i} ≡ -αβ⁻¹·(r0 + i) (mod D), i ∈ [0, N), from the paper.
Equations
Instances For
Unit-twisted analogue of V, built from cumulativeHitsUnit.
Equations
- CutAndProject.VUnit α β ω u k = if h : ∃ (x : ℕ), k < CutAndProject.cumulativeHitsUnit α β ω u x then Nat.find h else 0
Instances For
Unit-aware concrete difference sequence. With u = multiplier α β h_coprime
this is the residue-model counterpart of the geometric gap sequence in the
paper (the strip-to-residue identification is definitional, not proved).
Equations
- CutAndProject.differenceSequenceUnit α β ω u i = CutAndProject.sortedMultisetUnit α β ω u (i + 1) - CutAndProject.sortedMultisetUnit α β ω u i
Instances For
u = 1 specialisation: the unit-aware cumulative count agrees with cumulativeHits.
Helper: If the difference sequence has period L, the sortedMultiset shift by L is constant (independent of i).
Proof idea: Define f(i) = sortedMultiset(i+L) - sortedMultiset(i). Then f(i+1) - f(i) = differenceSequence(i+L) - differenceSequence(i) = 0 by periodicity. So f is constant = f(0).
Helper: N * shift = L * D. From sortedMultiset(i+N) = sortedMultiset(i) + D and sortedMultiset(i+L) = sortedMultiset(i) + σ, applied NL times both ways.
Unit-aware analogue of sorted_shift_constant. Structural — identical
to the untwisted proof with differenceSequenceUnit/sortedMultisetUnit
substituted.
The concrete residue-model instance built from the difference sequence:
discharges the four hypotheses of GeometricProjection for coprime α, β
and window parameter ω ≥ 0. Supplied explicitly at each use site (the
coprimality and nonnegativity hypotheses cannot be found by synthesis).
Theorem 3.1: Period length formula.
Set-valued period (Phase A: countHits dichotomy) #
The two lemmas count_hits_lt_D (already proved above) and count_hits_ge_D
(below) furnish the structural dichotomy underlying the set-valued period
theorem: under N < D the multiplicity function takes values in {0,1}
(so the gap multiset coincides with the gap set), while under N ≥ D every
residue class is hit (so the underlying set is all of ℤ and the set-valued
period collapses to 1).
Set-valued period (Phase B: dichotomy theorem, abstract form) #
Together with count_hits_lt_D and count_hits_ge_D (Phase A), this section
gives the abstract version of the set-valued period theorem:
λ_set = N if N < D, else 1. The dichotomy is reduced to two hypotheses
on the candidate set sequence — pointwise agreement with the multiset gap
sequence (when N < D), respectively constancy at 1 (when N ≥ D) —
which a concrete construction would discharge.
A sequence that is identically 1 has minimal period 1.
Set-valued period theorem (abstract form).
If set_seq : ℤ → ℤ agrees pointwise with differenceSequence whenever
N < D, and is constantly 1 whenever N ≥ D, then its minimal period is
N in the first case and 1 in the second.
The two hypotheses are exactly what the structural dichotomy
(count_hits_lt_D / count_hits_ge_D) lets a concrete enumeration of the
underlying point set verify.
Set-valued period (Phase C: concrete construction) #
Concrete enumeration of the underlying set
{ z ∈ ℤ | countHits D r0 N (z mod D) ≥ 1 },
mirroring the multiset's V / sortedMultiset machinery but with
multiplicities flattened to {0,1} via the indicator. The resulting
setDifferenceSequence discharges the abstract hypotheses h_lt
and h_ge of set_main_theorem.
Set indicator: 1 if residue (y : ZMod D) is hit at least once,
else 0. Flattens multiplicities of the multiset to {0,1}.
Equations
Instances For
Cumulative count of hit residues over [0, x]. Set analogue of
cumulativeHits.
Equations
- CutAndProject.setCumulativeHits α β ω x = (Finset.range (x + 1)).sum (CutAndProject.setIndicator α β ω)
Instances For
Set-convention analogue of V: the least x whose set-cumulative hit count exceeds k.
Equations
- CutAndProject.setV α β ω k = if h : ∃ (x : ℕ), k < CutAndProject.setCumulativeHits α β ω x then Nat.find h else 0
Instances For
Number of distinct residues hit, i.e. |set ∩ [0, D)|.
Equations
Instances For
Bi-infinite enumeration of the underlying set, lifted via setSize.
Equations
- CutAndProject.setSorted α β ω i = ↑(CutAndProject.setV α β ω (i % ↑(CutAndProject.setSize α β ω)).toNat) + i / ↑(CutAndProject.setSize α β ω) * ↑(α ^ 2 + β ^ 2)
Instances For
Concrete set-valued gap sequence.
Equations
- CutAndProject.setDifferenceSequence α β ω i = CutAndProject.setSorted α β ω (i + 1) - CutAndProject.setSorted α β ω i
Instances For
Phase C, branch N < D: agreement with differenceSequence #
The set size is positive in either branch of the dichotomy: it equals N
when N < D (and N ≥ 1 from N_pos_concrete), and equals D when
N ≥ D (and D ≥ 1 from NeZero). Hence the modulo arithmetic in
setSorted is well-defined as a period-block enumeration.
Phase C, concrete instantiation of both period theorems #
For symmetry between the two branches: each wrapper internally discharges
the [GeometricProjection ...] instance via GeometricProjectionConcrete,
so neither requires its caller to provide it.
Concrete multiset-valued period theorem. Wrapper around main_theorem
(line 1903) that internalises the GeometricProjectionConcrete instance,
so callers only need h_coprime and h_ω.
Unit-aware analogue of sigma_of_period_concrete.
Unit-aware analogue of period_degenerate_concrete. In the degenerate
case the unit-twisted sequence equals the untwisted one
(difference_sequence_unit_eq_difference_sequence_of_dvd), so the period
result transfers directly from period_degenerate_concrete.
Unit-aware concrete main theorem. Combines the period-N and degenerate
cases plus the minimality argument from heavy_set_unit_is_cyclic_interval.
For u = multiplier α β h_coprime, this is the geometric main theorem
(main_theorem_geometric_concrete below).
Geometric concrete main theorem. Specialises main_theorem_unit_concrete
to the geometric multiplier u = multiplier α β h_coprime, so the period
result holds for the residue-model enumeration carrying the geometric
residues c_{r0+r} ≡ -αβ⁻¹ · (r0 + r) (mod D) (paper §9.3, Layer 2; the
reduction from the lattice strip is not formalised — see the module
docstring).
The geometric residue of the integer point indexed by r, as defined in
equation eq:residue of the paper:
cR ≡ -α · β⁻¹ · r (mod D).
This formalises the residue-class formula used by Section 3 of the paper
(strip-to-residue reduction). The function below is just multiplier · r
in ZMod D; the bridge lemma c_r_eq_multiplier_mul_r makes the equation
to the paper explicit, and count_hits_unit_multiplier_eq_c_r_count
shows that the unit-twisted hit-counter used in
differenceSequenceUnit α β ω (multiplier α β h_coprime) precisely
counts integer indices i ∈ [0, N) with c_{r0 + i} ≡ x (mod D).
Equations
- CutAndProject.cR α β h_coprime r = ↑(CutAndProject.multiplier α β h_coprime) * ↑r
Instances For
Bridge lemma to the paper's cR formula. The Lean multiplier equals
-α · β⁻¹ as a unit in ZMod D, so cR α β h r = -α · β⁻¹ · r (mod D)
matches equation eq:residue of the paper verbatim.
Bridge from the paper's residue map to the unit-twisted hit counter.
countHitsUnit (α^2+β^2) (multiplier α β h_coprime) r0 N x is exactly
the cardinality of {i ∈ [0, N) : c_{r0+i} ≡ x (mod D)}, where
c_{r0+i} is the geometric residue from the paper. This makes the
formalisation of main_theorem_geometric_concrete an honest statement
about the geometric cR enumeration.
Concrete set-valued period theorem. The setDifferenceSequence defined
above realises the abstract set_main_theorem, closing the asymmetry
between the multiset side (main_theorem, line 1903 — instantiated via
GeometricProjectionConcrete) and the set side.
Unit-twisted set-convention analogue of cumulativeHits.
Equations
- CutAndProject.setCumulativeHitsUnit α β ω u x = (Finset.range (x + 1)).sum (CutAndProject.setIndicatorUnit α β ω u)
Instances For
Unit-twisted set-convention analogue of setSorted.
Equations
- CutAndProject.setSortedUnit α β ω u i = ↑(CutAndProject.setVUnit α β ω u (i % ↑(CutAndProject.setSizeUnit α β ω u)).toNat) + i / ↑(CutAndProject.setSizeUnit α β ω u) * ↑(α ^ 2 + β ^ 2)
Instances For
Unit-aware concrete set-valued gap sequence. With
u = multiplier α β h_coprime this is the residue-model counterpart of the
geometric set enumeration (identification definitional, not proved).
Equations
- CutAndProject.setDifferenceSequenceUnit α β ω u i = CutAndProject.setSortedUnit α β ω u (i + 1) - CutAndProject.setSortedUnit α β ω u i
Instances For
Unit-aware Phase C, branch N < D: agreement with differenceSequenceUnit #
Discharge of h_lt for the unit case: under N < D, the unit
set sequence agrees pointwise with differenceSequenceUnit.
Unit-aware abstract set-valued period theorem. Parallel to
set_main_theorem but uses main_theorem_unit_concrete (the unit-aware
multiset main theorem) for the N < D branch.
Geometric concrete set-valued main theorem. Specialises
set_main_theorem_unit to u = multiplier α β h_coprime and discharges
the dichotomy axioms via the unit-aware Phase C lemmas.