Guided Learning Path

Use this page as the textbook syllabus. It tells you what to read first, what each unit is supposed to teach, and when you are ready to move on.

Targets, widgets, Python examples, and diagrams are not proofs. A theorem is Lean-proved only when generated theorem data and the local Lean build support that status.

The Reading Rule

Read the book in the same order you would read a math textbook: earliest concepts first, source references second. The dictionary, theorem index, paper index, and target index are reference shelves. They are useful after a lesson has given you the concept.

Each mature lesson has the same rhythm:

  1. Learn the goal.
  2. Read the idea in plain language.
  3. Use a diagram or widget.
  4. Work one example.
  5. Check a common mistake.
  6. Try a small exercise.
  7. Open the source trail only when you want to audit the term or theorem.

Before You Start

Circle Calculus is easiest if you keep four layers separate:

  • Picture: the drawn circle, diagram, or widget.
  • Rule: the arithmetic or combinatorial rule the picture is trying to show.
  • Example: Python or browser output for concrete values.
  • Proof: a theorem id with a checked Lean declaration.

If those layers blur together, pause and use How To Verify A Claim.

Part I: Learning Toolkit

Learning Goal

Learn the basic habits that make every later chapter easier: object, address, rule, composition, iteration, invariant, theorem, and proof status.

Start with Lesson 0: Mathematical Building Blocks. It is the front-of-book toolkit for readers who want to relearn the project from first principles before touching S0 or S1.

You are ready to continue when you can explain why a picture, rule, example, and proof are different kinds of mathematical evidence.

Part II: First Objects

Learning Goal

Learn how a tiny finite object can carry useful structure without pretending it is continuous geometry.

Read S0 Two-State Opposition for the absolute smallest object: two points and a flip. Then move to S1, where the book becomes arithmetic.

You are ready to continue when you can explain why a two-point flip is useful for signs, poles, antipodes, and paired states, but is not the same as a larger circular rotation.

Part III: S1 Finite Circular Arithmetic

These are the first mature textbook chapters. Read them in order before jumping to higher dimensions.

1 finite circles 2 rotation 3 coils 4 period and primes 5 winding 6 review

Step Page What You Should Be Able To Do
1 Finite Circles Reduce any integer address to a node in C_n.
2 Rotation As Addition Predict one rotation and a composition of two rotations.
3 Coils And Closure Trace the orbit from a start node and stride.
4 Period And Primes Compute period and cycle count from gcd(n,k).
5 Winding Lift Separate total turns from the final residue.
6 S1 Review And Exercises Solve mixed problems without opening the source trail first.

You are ready to move on when you can answer this by hand:

In C_18, start at 5 and stride by 6. Which nodes are visited before closure? What is the period? How many disjoint stride cycles does the whole circle have?

Part IV: Higher-Dimensional Ladder

Higher dimensions are organized as a ladder, not as isolated essays. Each page should say what finite model is currently checked and what continuous or topological claim remains future.

Layer Page What It Adds
S2 Suspended Circles Adds pole-like endpoints to circular rows.
S2 Sphere Grids Organizes finite rows into latitude/longitude-like coordinates.
S3 Quaternions Introduces bounded rotation algebra and spin sign ambiguity.
S3 Hopf Coils Separates visible base coordinates from hidden phase.
S4-S6 Suspension Euler Parity Tracks suspension-count and Euler bridge facts.
S7 Octonionic Layer Shows bounded octonion-model facts with nonassociativity warnings.
S15 Future Hopf Horizon Keeps horizon work active while marking topology boundaries honestly.

You are ready to continue when you can distinguish a finite scaffold theorem from a full smooth/topological theorem.

Part V: Advanced Frameworks

Phase II pages are framework chapters. They reuse the earlier vocabulary but shift attention to stability, bundles, boundaries, and proof-carrying glyphs.

Read these as bridge chapters. They are valuable because their finite seeds are explicit and their long-horizon claims are kept under status control.

Part VI: Applications

Application chapters are case studies, not hype pages. They reuse S1 language: address, rotation, stride, period, phase, closure, and proof status.

  • Proof-Backed Showcase: a public-facing capability map where every advertised item cites papers and proved theorem ids.
  • Classical Bridges: a reader-facing audit page for the Erdos-style combinatorics showcase lanes.
  • Data Analysis: periodic coordinates and benchmark guardrails.
  • Compute: cyclic addresses, stride layouts, and schedules.
  • AI: the overview for proof-carrying AI contracts and exploratory fixtures.
  • AI Contract Suite: the compact working entry point for RoPE, KV-cache, and sparse-attention certifiers.
  • AI Contract Ladder: the guided contract sequence from RoPE phase banks to KV-cache freshness, sparse-attention coverage, and circulant mixers.
  • RoPE Certifier: exact phase-bank distinguishability plus bounded real-phase proof seeds.
  • KV-Cache Ring Buffer: finite slot, freshness, and live-window certificates.
  • Sparse Attention Coverage: finite local-window plus stride-family coverage, gap-witness, and candidate-budget certificates.
  • Looped Recurrence Contracts: finite recurrence budgets, exit certificates, active-token boundaries, selected block routes, and schedule controls.
  • Physics: finite gauge links, path holonomy, and Wilson-loop certificates.
  • Generative Structures: seed-rule provenance and exact regeneration fixtures.
  • Rendering: direction bins and visual-compute scaffolds.

Use the application proof-audit appendices only when you are checking source status: Application Proof Audit, AI Contract Ladder Proof Audit, RoPE Proof Audit, KV-Cache Proof Audit, Sparse Attention Proof Audit, Looped Recurrence Proof Audit, and Generative Structures Proof Audit.

You are ready to trust an application claim only when you can say whether it is a Lean theorem, a deterministic fixture, a benchmark target, or a research hypothesis.

Appendix: Source Trail

The source trail is how the book stays honest:

Local verification:

make check
make site-render
make living-book-check

The public site deploy path is GitHub Pages. Deployment is generated from site/_site/ only after GitHub Actions builds Lean, runs source checks, and renders Quarto.

Start the textbook sequence Go to Lesson 0: Mathematical Building Blocks