S1 Unit: Finite Circle Core
S1 is the first complete unit of the Living Book. It teaches arithmetic on finite circular address spaces, then uses that arithmetic to explain motion, repetition, closure, period, primes, and winding.
The important object is not a smooth geometric circle. In this unit, C_n means a finite loop of n addresses. Drawings help you see the loop, but the mathematics is the rule that every address is reduced modulo n.
If the words object, address, rule, composition, iteration, invariant, or proof status feel unclear, read Lesson 0: Mathematical Building Blocks before starting this unit.
Unit Goal
By the end of S1, you should be able to:
- reduce addresses modulo a circle size,
- rotate by adding a stride,
- trace an orbit under repeated stride,
- compute period from
gcd(n,k), - explain prime full-coil behavior, and
- separate winding count from final residue.
The Story In One Picture
Circle C_n has n addresses Node one reduced address Rotation add a stride Coil repeat a stride Period first return Winding turns plus residue
Lesson Sequence
- Finite Circles: learn what
C_nis and how addresses wrap. - Rotation As Addition: turn motion into modular addition.
- Coils And Closure: repeat one motion until it closes.
- Period And Primes: use gcd to predict cycle structure.
- Winding Lift: keep full-turn information that residues forget.
- Review And Exercises: check the whole unit before moving upward.
What Gets Proved Here
The S1 core links to Lean-proved finite facts about rotation identity, rotation composition, inverse rotation, closure, period, orbit decomposition, prime full coils, full-coil/copime behavior, and winding. The cards in each lesson show the precise theorem ids and current status.
Do not use a diagram or widget as a proof. A page may help you see why a theorem should be true, but the proof-status source is the generated theorem card and Lean declaration.
Entry Check
Before the first lesson, make sure this sentence feels plausible: a clock face with 12 labels can treat 14 as the same address as 2 because the full turn has been ignored.