Phase 0

Principia Machina: map
Reading the program The move to Lean Status Terminology: the words of both versions
Lean itself Lean theorem prover Principia Machina in Lean
Version 1 The Principia Machina its specification

Phase 0: the team of three

Goal: three development machines and cloud sessions working one source repository, with automatic checks as the proof gate, before any physics code is ported to Lean.

Done

2026-10-10: the source repository created, private, with its main line protected against deletion and history rewriting. The charter of the Lean rewrite and its three companion documents (the environment guide, the evaluation of v1's development, the register of TPM words checked against Lean) added.
2026-10-10: the skeleton. Lean 4.34.1 pinned; the library Principia with a first module (the preimage of a digest) and three theorems; the Calculator as the executable pcalc; a test runner over a first vector corpus (netstring encoding); a proof gate that refuses sorry, native_decide, unsafe and any axiom beyond Lean's own. Automatic checks on Linux and Windows, green.
2026-10-12: a names check refuses any personal name on a private list in every file; real identifiers that must appear in a test are placeholders. In force since 2026-10-12.
2026-10-12: a session check runs at the start of every working session on every machine and in the cloud, and reports whether these progress pages are current and whether the working copy is behind; each network step is bounded, so it never holds a session up.
2026-10-11: naming rules for the project's documents: no version in a file name, the version in the document's header, edited in place, each document closing with its own end line; a lint checks them.
2026-10-12: two design notes: the durable prompt (how an agent's standing instructions stay current, are read and are attended to) and the naming rules.
2026-10-12: machine 1 set up by the setup script: Lean 4.34.1, the Lean tools for the agent, the commit hooks.
2026-10-12: the same commit built and passed its tests (6 of 6 vectors, 7 definitions and theorems through the proof gate, 0 failures) on Linux and Windows in the automatic checks, in a cloud session and on machine 1. Machine 2 is owed (acceptance check 1).
2026-10-12: in a cloud session and on machine 1, a deliberately broken theorem's error and goal were read through the agent's Lean tools rather than pasted from a terminal. Machine 2 is owed (acceptance check 4).
2026-10-12: the cloud working environment created; its setup succeeded on the first session.
2026-10-12: a change started in a cloud session from machine 3 was continued on machine 1 with its whole history, finished there and merged with every check green (acceptance check 2).
2026-10-12: line endings: the same text committed from Windows and from Linux is stored identically (acceptance check 5).
2026-10-12: publishing and disclosure settled. Information is PUBLIC (what scientific inquiry and independent reproduction need) or RESTRICTED (anything whose disclosure could undermine that goal); the wiki carries PUBLIC text only. Pages are published from the source repository only by the Declarer's act, which the wiki itself verifies; a page he also edits by hand changes only inside its marked blocks. A disclosure check refuses restricted terms in text bound for the wiki. These progress pages carry dates and phase items only.
2026-10-13: v1's pages that should not have been public: 57 retired (moved to neutral titles under "The Principia Machina/Retired", their earlier text hidden), and a restricted term edited out of the current text of other pages in two reviewed rounds (78 page saves in the second). The declared TPS and TPC-PY pages stay as v1's frozen record. Nothing was deleted.
2026-10-13: the wiki's extension updated to TPX 0.6.1, with the check that guards publishing; the check was proved both ways (refused without the Declarer's act, accepted with it). The first publish saved "Principia Machina/Lean transition" and the Main Page's box for the move to Lean, each read back equal.
2026-10-13: wide figures shrink to their column on every page, through a shared style sheet ("Template:Principia Machina/styles.css"); the Main Page box became one box, "The Current Program (Round 3): the move to Lean".
2026-10-13: a separate management dialog plans this work; it keeps no record of its own, the source repository holding what it produces.
2026-10-13: the standing rules for agents name the Agent Contract's versions among what the Declarer declares, and Custos beside TPX among the deployments that are his.
2026-10-13: cloud sessions read the wiki's public interface.
2026-10-13: v1's record seeded from the wiki, read only: TPS 0.5.0's 54 pages, the foundations record and the Decisions index, each at its current revision and checked against the wiki's own checksum, with a script that re-reads and re-checks them. In the record four author names in bibliography citations read "[cited author]". The charter now names TPS 0.5.0 and records TPS 0.5.0 and TPC-PY 0.3.0 as declared on 2026-10-03.
2026-10-13: these progress pages rewritten as PUBLIC text, and the session check reading the date they carry.
2026-10-13: the renderer for these pages: each phase's page and the log, every page ending with its "as of" date, refusing any source line that would put a development identifier on the wiki; it compares the rendered pages with the live ones, reading only.
2026-10-13: a survey of ways to cut the manual steps in the remote workflow, each rated for security, time saved and steps removed.
2026-10-13: a daily read-only measurement of how reliably automated reads reach the wiki, by the kind of machine that sends them; every publishing run, every comparison of these pages and every check of a change to the publishing tools records the same count.
2026-10-13: a read-only survey script lists which wiki pages use the server-rendered diagram tags and the external-data functions, and whether the wiki's search index is built; the Operator runs it from his machine.
2026-10-14: the push that keeps these pages current, built: after every landing and once a day the pages are rendered and compared with the wiki, and when they are behind they are saved by an account the wiki itself bounds to the progress pages, after the names check and the disclosure check; it waits only on that account.
2026-10-14: the kit for tests T2 and T3 beside T1's: a binary that reads a 1 MB document, one timed call and 100 calls in one run, rehearsed in the automatic checks.
2026-10-14: one closing run for machine 1: every open item machine 1 can reach (the term list, the names list, tests T1 to T3 on the host, the progress account and its first push, v1's other half proposed for reading), asking once for what it cannot read.
2026-10-14: the closing run's first start stopped at its own preflight: the host's SSH alias was known to Windows OpenSSH, not to the Linux side's ssh. The run now takes whichever knows the alias, and copies its files over the connection itself.
2026-10-14: two terms added to the disclosure check's list.
2026-10-14: test T1 on the wiki's host, measured three ways. The compiled binary runs from the host's shell and from a command-line call made by the site's own scripting language, printing the expected line both times. It does not run inside a web request: the host gives a web worker about a twentieth of the address space it gives a command-line process, and that is less than the binary reserves, so it stops before it starts. Pinning the binary's thread count from sixteen down to one does not change what it reserves, and an application cannot raise one of these ceilings from inside. The server design therefore stands as written, with one residence, and the binary is called outside the web request rather than during it.
2026-10-14: v1's seed, the other half, from the work folder: 8 schema and declarations files, 0 vector corpora verbatim, 0 generators, the extension source and the last project meta prompt, each scrubbed of local paths.
2026-10-14: one run for machine 2: the setup, the names check's local list, acceptance checks 1 and 4 and the Remote Control server, each step recording its own result in these pages; check 3 recorded from the session machine 2 serves, steered from machine 3 and from a phone or tablet.
2026-10-14: the page on the move to Lean corrected at its source, for the next publish: it states test T1's result, shows Phases 0 and 1 under way together with Phase 0 the current focus, writes every state in its figures as a label as well as a colour, and shows a plain title as the wiki's other editions do.
2026-10-14: the disclosure check runs in the automatic checks on every proposed change, over the wiki's page sources and over these pages as rendered, so no text reaches the main line unread by it.
2026-10-14: the proof gate closed a gap. A theorem added with the Lean kernel's check switched off, by a tactic that assigns a wrong proof, passed the gate with no axiom listed. The gate now refuses that option and replays every definition and theorem of the library through the Lean kernel with Lean's own re-checker.
2026-10-14: test T1's kit and its run now give each of the test's three calls its own verdict, as the charter defines them: from the shell, from the command line through the site's scripting language, and inside a web request. The first two decide the test.
2026-10-14: the kits for tests T2 and T3 rebuilt to call the binary the way the wiki calls its diagram renderer, through the wiki's own command framework, from a maintenance task on the command line rather than a web request. T2 is one timed call with a 1 MB document; T3 is 100 such calls in one run, from the shell and from one scheduled run, set against the hourly computing budget. Rehearsed against the wiki's own software on a test machine: about a twentieth of a second of processor time per call, and the 100 calls under a fifth of one per cent of the hourly budget.
2026-10-14: the kit for test T5, a check by Lean's kernel rules on the host: an independent checker, written apart from Lean's own, checks one of the library's theorems with everything it depends on (513 items), and refuses two altered copies, one whose statement no longer matches its proof and one whose proof is replaced by an unpermitted axiom. Rehearsed against the wiki's own software on a test machine: under a tenth of a second of processor time per check, in about 8 MB of memory.
2026-10-14: the status panel, a progress page of its own: every item of every phase, from the setup to the first release, as a lamp that carries its word (done, partial, under way, blocked, not started), with the role that owns it, its projected date and the date it was last checked. A strip of one lamp per phase and for the first release on top; a faults panel below it for every blocked item and every item past its likely date; then one panel per phase and the figure of the seven phases. That figure is now computed from the panel's source wherever it appears, here, on the page about the move to Lean and in the Main Page's box, so its copies cannot disagree with the panel. A panel not checked for more than two days shows as stale, and the daily check fails until a landing checks it again.
2026-10-14: staleness on the status panel counts only the items under way, partly done or blocked. A phase whose items have not started is never shown as stale; an item past its likely date still turns red. Phases 2 to 6 and the first release no longer fail the daily check while nothing in them has begun.
2026-10-14: the names check keeps a citation faithful to its source. A bibliography entry that cites an author by a published name containing a word on the private list passes only once that exact line has been reviewed and listed; any change to the line ends the exception, prose is never excepted, and an exception that no longer matches its line fails the check.
2026-10-14: the Declarer's publish put on the wiki the page on the move to Lean as corrected, under its plain title "The move to Lean", the Main Page's box with the figure of the phases computed from the status panel and a link to the panel, and the short title "Principia Machina/Lean transition/Status", which leads to the panel. The same publish saved the terminology page (recorded on Phase 1's page), the shared style sheet and the 71 pages of the Lean theorem prover edition, new.
2026-10-15: a working session now re-reads its task's instructions and any new directions at every step boundary, so a direction that pauses, stops or narrows the work reaches it without a restart. A direction that would add to or change the work is recorded and waits for the Declarer's own word.
2026-10-15: the Declarer's choices on ten open questions, recorded in the charter: the Calculator written in Lean's core alone, without Mathlib; its SHA-256 and its Unicode normalization written in the source repository, checked against published test data and normalizing as version 1 did; the three-letter code table approved as it stands; the two kinds of Provision confirmed; every number the Calculator computes exact, each difference from version 1's floating-point rounding recorded as a divergence; the governor's admission first, its other parts after it in a recorded order; test T3's scheduled run set up on the wiki's host by the closing run, its removal left to the Operator; the eight readings of version 1's permissions table kept as built; and the agent's Lean tool pinned to one version on every machine.
2026-10-15: one command, the Declarer's, now lands the finished changes: each change whose checks all pass joins the main line, in the order the changes build on one another, and a change that does not pass is set aside with every change built on it, each named with the reason.
2026-10-15: changes built side by side now land without touching the same lines. Each change adds one short progress note of its own instead of editing these pages' sources, the status panel's table and the list of test corpora; these pages and the panel read the notes at once, and one landing per batch folds them into the sources, the panel's version moving only then. The lists every newly ported function family extends are kept one entry per line in alphabetical order, so two families added together insert at different places. An automatic check refuses a change that edits the shared sources, and every session's start warns of one.
2026-10-16: machine 2 set up by the setup script: Lean 4.35.0, the Lean tools for the agent, the commit hooks.
2026-10-16: the names check runs on machine 2 from its own local list, clean over every file.
2026-10-16: on machine 2 the current commit built and passed its tests with the same output as the automatic checks on Linux and Windows for that commit (5728401 of 5728401 vectors, 15585 definitions and theorems through the proof gate, 0 failures) (acceptance check 1).
2026-10-16: machine 2 serves Remote Control sessions, kept running as a user service.
2026-10-16: on machine 2, a deliberately broken theorem's error and goal were read through the agent's Lean tools rather than pasted from a terminal (acceptance check 4).
2026-10-16: the account that keeps these pages current exists; its first unattended push is recorded on Phase 1's page.
2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).
2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.
2026-10-17: a change that edits an automatic check's own script together with what that script checks now gets a second, advisory run of that check with the change's own copy of the script. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.

Open

The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.

Done

Open

Next