Circle Calculus Living Book

Claim boundary Lean-proved where cited widgets are examples no universal-circle claim

Most of mathematics quietly runs on one move: count, and when you run out of room, wrap around. A clock does it. So does a week, a music scale, the hours on a parking meter, and the remainder you learned in grade school. Circle Calculus takes that single move seriously and rebuilds familiar mathematics on top of it, one careful step at a time — and every step is backed by a machine-checked proof.

Start With One Idea: The Finite Circle

A finite circle C_n is just a loop of n reusable addresses, numbered 0, 1, 2, ... , n-1.

Picture a clock with n labels. To find where an address lands, you keep the remainder after dividing by n:

address i  ->  node (i mod n)

On a 12-hour clock (C_12), address 14 lands on node 2: one full turn of 12 is discarded, and 2 is what remains. Address 26 lands on 2 as well. That is the whole starting idea — naming positions by wrapping around.

Everything else in this book grows out of that move:

count -> wrap -> move -> repeat -> close -> lift -> build up -> apply

Rotation is adding a step. A coil is repeating a rotation. The period is when a coil closes back to its start. Winding remembers how many turns you took. Higher dimensions stack circles into spheres. None of it leaves the finite circle behind.

Who This Book Is For

This book is written for one reader: a curious person who knows a little modular arithmetic and wants to watch familiar math get rebuilt from circles, with the proofs kept honest the whole way. You do not need a research background. If “remainder after dividing by n” makes sense to you, you can start at the beginning and keep going.

You do not have to trust anything on faith. Each lesson teaches an idea in plain language, gives you a picture and a worked example, asks you one question you can answer by hand, and then — only if you want to audit it — links to the exact Lean proof, Python model, and paper behind the claim.

Start Here

  1. Read Lesson 0: Mathematical Building Blocks — the small toolkit every later lesson reuses.
  2. Begin Lesson 1: Finite Circles and work straight through the S1 lessons in order.
  3. Finish the S1 review before climbing into higher dimensions.

That is the entire on-ramp. The rest of this page is for when you want to know how the book keeps itself honest, or you arrived as a reviewer rather than a learner — feel free to skip it and just start reading.

Under The Hood

Everything below is how this book stays trustworthy, not part of the lessons. A first-time reader can ignore it entirely and come back later.

How A Lesson Is Built

Every mature lesson gives the same shape: a goal stated before the math, a plain-language explanation, a diagram or widget when a picture helps, one worked example, one checkpoint you can do by hand, and a source trail back to the formal record. You can read at three depths:

Intuition Mode — use the widgets and diagrams to build a picture. These are explanations, not proofs.

Formal Mode — open theorem cards, Lean declaration names, and manifests. A theorem is treated as proved only when the generated manifest status and the local Lean build agree. See What “Proved” Means Here.

Code Mode — compare a widget’s behavior against the Python reference models and tests. Python examples are executable support, not formal proof.

Where The Words Come From

The public site is downstream of the formal repository:

Lean proofs -> theorem manifests -> dictionary -> Python models -> papers -> interactive site

The prose teaches; the widgets illustrate; the dictionary fixes vocabulary; the manifests carry theorem status; Lean is the formal proof source. That pipeline is why the book can read like a story without drifting away from what is actually proved.

For Reviewers And Skeptics

If you came to audit rather than to learn, three pages are built for you:

If you are here specifically for proof-carrying AI contracts, start with the RoPE certifier, then walk the AI contract ladder. That path shows the flagship position-distinguishability contract first, then generalizes the same contract shape to KV-cache freshness, sparse-attention coverage, recurrence schedules, exact Python CLIs, Lean declarations, theorem ids, paper trails, and limitations.

Proof-Backed Portfolio

If you are asking why anyone should use Circle Calculus, start with the Proof-Backed Showcase. It is the serious public advertisement for the project: every advertised capability is required to name a standard anchor, a Circle expression, a Circle-native value claim, a proof scope, a not-claimed boundary, paper ids, proved theorem ids, dictionary ids, executable examples, and Living Book pages or widgets. The advertised surfaces are generated from manifests/capability_showcase.yaml and validated by scripts/check_capability_showcase.py.

If you want to use the project as a library rather than read the textbook, start with Use This As A Library.

Read How To Verify A Claim beside it. The portfolio does not prove universal expressiveness by assertion; it shows the current checked surfaces and the source trail needed to audit each one. The widgets, diagrams, and Python examples on this site are illustrations and executable support — they are not proofs and not formal proof of the theorems they accompany.

This is a disciplined way to relearn many familiar ideas through recurrence, phase, closure, and proof-carrying records. It is not a claim that all of mathematics is literally a circle.

Next lesson Start Lesson 0: Mathematical Building Blocks