08. Bounded additive cycle¶
← 07. Short train · Table of contents · 09. Factor-repeat rigidity →
Lean:
EuclidsPath/Engine/BK.lean(exists_additive_cycle).
Where we are¶
In chapter 07 we squeezed the length of a valid train: even along an infinite affine line the number of genuinely reachable centres is short (cubic_squeeze). The +1 fuel is inexhaustible, but the engine's valid move is cramped.
Now we turn the clamp into the additive plane: instead of the length of a single move, we ask how many distinct K-fold combinations of divisors can fit into a bounded window before two of them inevitably coincide in sum. The answer — a pure pigeonhole, the boxes principle (see the glossary) — gives us the first structural prohibition on unchecked accumulation of repeats.
Setting: an additive cycle on K-multisets¶
Fix a finite set of divisors (or centres) 𝒜 ⊆ [1, T], that is, every a ∈ 𝒜 satisfies 1 ≤ a ≤ T. The parameter K ≥ 1 is the order of the combination — the "length" of the additive word that the engine assembles from elements of 𝒜.
Definition 8.1 (K-multiset). A K-multiset over
𝒜is a multiset of cardinalityKall of whose elements lie in𝒜. The set of all such objects is written in Lean/Mathlib as𝒜.sym K(the symmetric K-power). Order in a multiset does not matter and repeats are allowed — this is precisely an "unordered choice ofKelements from𝒜with replacement".
To each K-multiset s ∈ 𝒜.sym K we assign its additive weight — the sum of its elements:
Definition 8.2 (nontrivial additive cycle). By a nontrivial additive (Euclidean) cycle we mean a pair of distinct K-multisets
s ≠ tfrom𝒜.sym Kwith equal weight:\[ s \neq t, \qquad \Sigma(s) \;=\; \Sigma(t). \tag{8.2} \]"Nontriviality" here is exactly
s ≠ t: the trivial equalityΣ(s) = Σ(s)costs nothing; what is substantive is that two different ways of adding upKdivisors give one and the same total.
The name "cycle" is not accidental. The equality Σ(s) = Σ(t) with s ≠ t is the relation \(\sum_{x\in s} x - \sum_{y\in t} y = 0\), that is, a nontrivial integer linear dependence (with coefficients ±1) among the elements of 𝒜. Such a closed additive loop is precisely a "cycle" in the additive structure generated by the carrier.
Theorem: mass forces a cycle¶
The chapter's main result is the contrapositive of Lemma B_K (§VI, Lemma 6.1.1). The direct lemma asserts: if 𝒜 ⊆ [1,T] has no nontrivial equality of K-sums, then the set is forced to be small, \(|𝒜| \ll_K T^{1/K}\). We, however, need precisely the contrapositive — the form that feeds Fan-Cycle further down the chain: as soon as there is enough combinatorial mass, a cycle is bound to exist.
Theorem 8.3 (
exists_additive_cycle). Let \(\mathcal{A} \subseteq \mathbb{N}\) be a finite set, \(K, T \in \mathbb{N}\), \(1 \le K\), and suppose\[ 1 \le a \le T \quad \text{for all } a \in \mathcal{A}, \qquad K \cdot T \;<\; |\,\mathcal{A}.\mathrm{sym}\ K\,|. \tag{8.3} \]Then there exist \(s, t \in \mathcal{A}.\mathrm{sym}\ K\) such that \(s \neq t\) and \(\Sigma(s) = \Sigma(t)\) (8.2) — a nontrivial additive Euclidean cycle.
The condition K · T < |𝒜.sym K| is the mass threshold: the number of distinct K-multisets exceeds the number K·T of possible values of the sum. The whole proof is pigeonhole — no analysis, no distribution of primes, no sieve. This makes the result an atomic law of the engine, not a heuristic.
Why this is true: walking through the proof¶
The proof in BK.lean is arranged in three steps, and each honestly plays its part.
Step 1 — the image of the weight is pinned inside the window [K, K·T]. Let s ∈ 𝒜.sym K. By definition s is a multiset of cardinality exactly K (in Lean this is s.2 : (s : Multiset ℕ).card = K), all of whose elements lie in 𝒜 and are therefore squeezed between 1 and T. Hence two bounds:
The lower bound is Multiset.card_nsmul_le_sum (a sum of K terms, each ≥ 1, is at least K); the upper is Multiset.sum_le_card_nsmul (each term ≤ T, hence the sum is ≤ K·T). In the code this is packaged as
that is, the weight map Σ : 𝒜.sym K → ℕ really does land in the integer interval Finset.Icc K (K*T).
Step 2 — the window of values is tight. The interval Finset.Icc K (K*T) contains exactly K·T − K + 1 integer points (Nat.card_Icc). With 1 ≤ K this is at most K·T. The hypothesis K·T < |𝒜.sym K| then gives
In Lean this is the single arithmetic line, closed by omega:
There are strictly fewer values of the sum than there are K-multisets.
Step 3 — pigeonhole. The map Σ carries the larger set (all K-multisets) into the smaller one (the window of sums). By Dirichlet's principle it cannot be injective: two distinct preimages get glued into one image. Formally this is Finset.exists_ne_map_eq_of_card_lt_of_maps_to, which yields exactly the pair we need:
hne : s ≠ t and heq : Σ(s) = Σ(t) — this is the nontrivial additive cycle. The proof is complete.
Note. The three steps match the three ingredients of any pigeonhole argument: (1) send the objects into boxes (
hmaps— the weight lands in the window), (2) count that the boxes are few (hcard_lt), (3) extract the collision (Finset.exists_ne_map_eq_of_card_lt_of_maps_to). None of the steps uses any property of prime numbers — any𝒜 ⊆ [1,T]will do. This is precisely why it is a law of the mechanism, not a property of a particular arithmetic.
What it means: a bound on the order of repeats¶
The substantive consequence is a bound on how long the carrier can grow "cycle-free". Let us restate the direct Lemma B_K as a counting estimate.
Proposition 8.4 (cycle-freeness threshold). If \(\mathcal{A} \subseteq [1,T]\) contains no nontrivial additive cycle of order \(K\) (in the sense of Definition 8.2), then the weight map \(\Sigma\) (8.1) is injective on \(\mathcal{A}.\mathrm{sym}\ K\), whence
\[ |\mathcal{A}.\mathrm{sym}\ K| \;\le\; |\mathrm{Icc}(K,\,K{\cdot}T)| \;=\; K{\cdot}T - K + 1 \;\le\; K{\cdot}T. \tag{8.6} \]Since \(|\mathcal{A}.\mathrm{sym}\ K|\) grows like \(\binom{|\mathcal{A}| + K - 1}{K} \asymp |\mathcal{A}|^K / K!\), from (8.6) we get \(|\mathcal{A}|^K \lesssim K{\cdot}T\), hence \(|\mathcal{A}| \ll_K T^{1/K}\). This is exactly the \(|\mathcal{A}| \ll_K T^{1/K}\) of §VI. (Contrapositively: if \(|\mathcal{A}|^K \gg K \cdot T\), then by Theorem 8.3 a cycle exists.)
Conclusion. An additive cycle can be avoided only by keeping the carrier radically sparse — no more than on the order of T^{1/K} elements in the window [1,T]. Euclid's engine, on the contrary, is forced to accumulate divisors on the centres along its move; as soon as enough of them pile up relative to the available window of values, a repeat of sums is inevitable. Through the contrapositive this translates into a structural prohibition: the order of repeats is bounded — one cannot endlessly clone a divisor configuration while keeping all additive weights distinct.
Coupled with the impossibility of the perpetual engine — the infinite strictly descending chain, the programme's central forbidden object (chapter 01, no_infinite_descent) — this feeds the prohibition of perpetual clean recycling: if the reuse of divisors could go on without forming an additive loop, the carrier would grow while remaining cycle-free, contradicting the T^{1/K} threshold. The cycle guaranteed by Theorem 8.3 (exists_additive_cycle) is the point where "clean" fuel recycling closes onto itself and therefore cannot last forever.
Note (the boundary of the result). The theorem gives the existence of a cycle, but not its geometry: it does not say which divisors enter it, and it does not tie the cycle to differences of centres. That tie — that a repeat of the divisor
ℓpins downℓ ∣ (n₂ − n₁)— is established only in the next chapter. Here we record honestly: Theorem 8.3 (exists_additive_cycle) is a combinatorial threshold, NOT a structural rigidity; the two must not be conflated.
Bridge to what comes next¶
We have obtained that a mass of divisors forces an additive cycle, and, through the contrapositive, that the order of repeats is bounded by the window T^{1/K}. But the bare existence of coinciding sums does not yet say that a repeated divisor entails periodicity of hits along the move.
In chapter 09 (factor_repeat_rigidity, cross_side_fuel) we will give the repeat its rigidity: if a prime ℓ appears as a divisor at two centres, it divides their difference, ℓ ∣ (n₂ − n₁). The bounded cycle of this chapter and the rigidity of the next, together with the short train (chapter 07), will close the covering into something finite and short — turning the additive prohibition into a geometric one.
← 07. Short train · Table of contents · 09. Factor-repeat rigidity →