Cycle.lean — FrcCore

1import FrcCore.Series23/-!4# FrcCore.Cycle — the cycle of `n` sites and the shift of its index (the base theme; 38-s13, 12 October 2026)56A function on the cycle of `n` sites is a function `Nat → Shell p` read at `i mod n` (`cyc`); it returns after `n` steps7(`cyc_add_n`). A sum over the cycle is invariant under the shift of its index (`sum_shift`), because `j ↦ (j + s) mod n`8permutes `[0, n)` (`shift_inj`, proved on the core's own division algorithm `FRC.Nat.mod_spec`, without the prelude's9`omega`). Moved here from the gravity theme's `Theme/Shift.lean` (21-gravity, 10 October 2026) on 12 October (38-s13,10task T02; the author's decision D4), so that every theme may read the cycle; every name is unchanged (`FRC.Cycle`), and11the shift theorem stays in `Theme/Shift.lean`. No axioms.12-/1314namespace FRC.Cycle1516open FRC.Shell1718variable {p : Nat} [Pos p]1920/-- A function on the cycle, read at `i mod n`. -/21def cyc (n : Nat) (f : Nat → Shell p) (i : Nat) : Shell p := f (i % n)2223theorem cyc_mod (n : Nat) (hn : 0 < n) (f : Nat → Shell p) (i : Nat) : cyc n f (i % n) = cyc n f i := by24  show f (i % n % n) = f (i % n); rw [FRC.Nat.mod_mod i n hn]2526theorem cyc_add_mod (n : Nat) (hn : 0 < n) (f : Nat → Shell p) (i s : Nat) :27    cyc n f (i % n + s) = cyc n f (i + s) := by28  show f ((i % n + s) % n) = f ((i + s) % n); rw [FRC.Nat.mod_add_mod i s n hn]2930/-- 21:X3, 00:E5, 00:E10, 38:B4 — the drive returns after `n` steps: a function on the cycle read `n` sites on is itself, so a permutation of31the cycle has finite order and what it moves comes back. -/32theorem cyc_add_n (n : Nat) (hn : 0 < n) (f : Nat → Shell p) (i : Nat) : cyc n f (i + n) = cyc n f i := by33  show f ((i + n) % n) = f (i % n)34  rw [FRC.Nat.add_mod i n n hn, FRC.Nat.mod_self n hn, Nat.add_zero, FRC.Nat.mod_mod i n hn]3536/-! ## The shift permutes the cycle -/3738theorem shift_lt (n : Nat) (hn : 0 < n) (s j : Nat) (_ : j < n) : (j + s) % n < n := FRC.Nat.mod_lt' _ hn3940/-- If `i + s` and `j + s` share a residue mod `n` with quotients `q₁ < q₂`, then `j ≥ i + n`, impossible for `j < n`. -/41theorem no_lower_quot {n i j s q₁ q₂ r : Nat} (hj : j < n) (h1 : i + s = n * q₁ + r) (h2 : j + s = n * q₂ + r)42    (hq : q₁ < q₂) : False := by43  have h3 : n * (q₁ + 1) ≤ n * q₂ := Nat.mul_le_mul_left n (Nat.succ_le_of_lt hq)44  rw [Nat.mul_succ] at h345  have h4 : i + s + n ≤ j + s := by46    rw [h2, h1]47    calc n * q₁ + r + n = n * q₁ + n + r := by rw [Nat.add_assoc, Nat.add_comm r n, ← Nat.add_assoc]48      _ ≤ n * q₂ + r := Nat.add_le_add_right h3 r49  have h5 : i + n ≤ j := by50    have : (i + n) + s ≤ j + s := by51      rw [Nat.add_right_comm]; exact h452    exact Nat.le_of_add_le_add_right this53  exact Nat.lt_irrefl n (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_add_left n i) h5) hj)5455/-- The shift `j ↦ (j + s) mod n` is injective on `[0, n)`. -/56theorem shift_inj (n : Nat) (hn : 0 < n) (s i j : Nat) (hi : i < n) (hj : j < n)57    (h : (i + s) % n = (j + s) % n) : i = j := by58  obtain ⟨q₁, h1⟩ := FRC.Nat.mod_spec n hn (i + s)59  obtain ⟨q₂, h2⟩ := FRC.Nat.mod_spec n hn (j + s)60  rw [h] at h161  rcases Nat.lt_or_ge q₁ q₂ with hq | hq62  · exact (no_lower_quot hj h1 h2 hq).elim63  · rcases Nat.lt_or_ge q₂ q₁ with hq' | hq'64    · exact (no_lower_quot hi h2 h1 hq').elim65    · have e : q₁ = q₂ := Nat.le_antisymm hq' hq66      rw [e] at h167      exact Nat.add_right_cancel (h1.trans h2.symm)6869/-- A sum over the cycle is invariant under the shift of its index by `s`. -/70theorem sum_shift (n : Nat) (hn : 0 < n) (F : Nat → Shell p) (s : Nat) :71    sumRange (fun j => F ((j + s) % n)) n = sumRange F n :=72  sum_perm F (fun j => (j + s) % n) n (shift_lt n hn s) (shift_inj n hn s)7374end FRC.Cycle75