S2: Sphere Scaffolding
You have a circle. How do you build a sphere from it? S2 answers with one move — suspension — and then organizes the result into the latitude/longitude grid you already know from a globe.
Unit Goal
See how finite S1 circles get stacked and capped into a sphere-like scaffold, and be able to count its cells and check that its Euler characteristic is 2.
The Idea
S2 is the first place the book leaves a single loop behind. The safe, current version stays finite and combinatorial: poles, equators, latitude rows, longitude addresses, and antipodal pairs are tracked as explicit data rather than borrowed from continuous geometry. Each latitude row is, underneath, just an S1 circle — so everything you learned about rotation and period keeps working along every row.
Lesson Path
- Suspended Circles — add two poles to a finite circle and watch
χgo from0to2. - Sphere Grids — read the sphere as latitude rings (each an S1 circle) indexed by longitude.
When you want to know which of these claims are Lean-proved, the theorem cards on each page are the status source; continuous sphere geometry is future work.
This is a scaffold unit: the theorem cards are the status source, and the widgets and diagrams are explanations, not proofs. See What “Proved” Means Here.
Checkpoint
In one sentence, what is the difference between a finite suspended-circle model and a claim about the continuous sphere S^2?