Prime Circle Math — machine-checked

Formalization of the prime/modular structure of ancient counting systems (360° dial, base 60, the 19×19 board, flower of life, abacus, circle of fifths). Lean 4.28.0 + Mathlib v4.28.0 — 53 modules, ~425 theorems, no sorries.

Start here

OVERVIEW.md — what the project checks, proves and corrects
SYNTHESIS.md — the main write-up
README.md — provenance (edited by Aristotle)

Audit trail

File	Contents
AUDIT.md	Claim-by-claim audit of the source documents
CLAIM_TO_THEOREM_REGISTRY.tsv	Claims mapped to Lean theorem names
CROSS_PROJECT_CLAIM_LEDGER.tsv	Cross-project claim ledger
IMAGE_CLAIM_LEDGER.tsv	Image claim ledger
RENDERING_AUDIT.md	√ tables, vector arithmetic, rendering/projection
RECURSIVE_REASSESSMENT.md	φ-depth recursion
SELF_SIMILAR_MODEL.md	Recursive cell across figures
SHARED_MODEL.md	Terminology → standard structures
LEXICON.md	Lexicon

Source

RequestProject/ — 53 Lean modules (entry: Main.lean, synthesis: Synthesis.lean)
bench/ — single-machine C benchmark (not formally verified)
prime-circle-math.html — interactive explorer
lakefile.toml / lean-toolchain — build with lake build
deployment-info.json — bundle manifest

Project ID: 9b854e2d-2ae1-4d55-9b53-bf308b5e3648 · Deployed via aristotle-manager deploy → Cloudflare Pages · Build tile: solana.solfunmeme.com/aristotle-builds