The status panel
| 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 |
The status panel: every item of every phase as a lamp, from the setup to the first release declared; the aim is every lamp green. Each phase's own page tells its items in words.
DONE PARTIAL n of m UNDER WAY BLOCKED NOT STARTED OVERDUE past its likely date and not done; a panel whose rows under way, partial or blocked are unchecked for more than 2 days is STALE. Every lamp carries its word; the colours repeat it.
Master annunciator · lamps judged on 2026-10-18
Phase 0DONE
Phase 1UNDER WAY1 FAULT
Phase 2UNDER WAY
Phase 3NOT STARTED
Phase 4NOT STARTED
Phase 5NOT STARTED
Phase 6NOT STARTED
First releaseNOT STARTED
Faults
| Phase | Item | Fault | Owner | Projected |
|---|---|---|---|---|
| Phase 1 | Test T3: a hundred calls in one scheduled run, against the hourly budget: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows | BLOCKED | Operator | 2026-10-18 |
| updated Date: | Pacific Time | UTC |
|---|---|---|
| 2026-10-18 | 09:08 PDT | 2026-10-18 16:08 |
| 2026-10-18 | 08:43 PDT | 2026-10-18 15:43 |
| 2026-10-17 | 21:16 PDT | 2026-10-18 04:16 |
The seven phases and the first release
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Check 1: one change builds and passes its tests alike on every machine, in a cloud session and in the automatic checks | DONE | Operator | 2026-10-18 | 2026-10-16 |
| Check 2: a task started in a cloud session from one machine, then finished and merged from another | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Check 3: a session served by machine 2, steered from machine 3 and from a phone or tablet | DONE | Operator | 2026-10-18 | 2026-10-17 |
| Check 4: a broken proof's error read through the agent's Lean tools in each kind of session | DONE | Operator | 2026-10-18 | 2026-10-16 |
| Check 5: line endings identical when committed from Windows and from Linux | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Test T1: a Lean program run on the wiki's host | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Test T2: one timed call with a 1 MB input, through the wiki's command framework: PASS, 0.070 CPU-seconds a call | DONE | Operator | 2026-10-18 | 2026-10-17 |
| Test T3: a hundred calls in one scheduled run, against the hourly budget: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows | BLOCKED | Operator | 2026-10-18 | 2026-10-18 |
| Test T5: a proof checked on the host by an independent Lean kernel checker: PASS, 0.083 CPU-seconds for a theorem and its closure | DONE | Operator | 2026-10-18 | 2026-10-17 |
| The terminology page, the register of names, on the wiki | DONE | Declarer | 2026-10-18 | 2026-10-15 |
| The three-letter code table approved | DONE | Declarer | 2026-10-18 | 2026-10-15 |
| Version 1's material copied into the source repository | DONE | Operator | 2026-10-18 | 2026-10-18 |
| The declared parameters and tuning options, in Lean | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The record table as Lean types, with the three forms a derivation may take and the class each earns | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The terminology map | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades: set up to run monthly; its first run falls on 2026-10-22 | UNDER WAY | Agent | 2026-10-22 | 2026-10-17 |
| Publishing the framework's pages from the source, by the Declarer's act | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The push that keeps the progress pages current, after every landing and once a day | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The progress pages' wiki account, and their first unattended push | DONE | Operator | 2026-10-18 | 2026-10-17 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Digests and canonical serialization | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Units and dimensions | DONE | Agent | 2026-11-26 | 2026-10-18 |
| The zones: Starting Set, Correspondence Table, Criteria Set | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Declared forms | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Fundamental tests and isomorphism checks | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Records and the register functions: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification | PARTIAL 3 of 4 | Agent | 2026-11-26 | 2026-10-18 |
| The strike rule, distance, SR8 and SR9 | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Hold scope | DONE | Agent | 2026-11-26 | 2026-10-15 |
| The structure check of the equations of motion | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Provisions | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Probes and their comparison | DONE | Agent | 2026-11-26 | 2026-10-17 |
| Score and beta | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Cluster | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Falcons | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Bibliography | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Identity, sponsor and lint | DONE | Agent | 2026-11-26 | 2026-10-18 |
| Governor and permissions: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-18 |
| The structured derivation checker, with its soundness proof: the step language, its checker, its credit and the proof that it is sound, with matching a law to an instance of it; which laws may be matched so and what a derivative means wait on the Declarer's choices | UNDER WAY | Agent | 2026-11-26 | 2026-10-18 |
| The generated specification pages and their converter, shipped with each release: the program that reads the checked library; the converter, its checks and the rewrite of the comments the pages carry follow | UNDER WAY | Agent | 2026-11-26 | 2026-10-18 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4 | NOT STARTED | Operator | 2026-12-13 | 2026-10-14 |
| Custos's page classes | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Custos's API module | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Custos's jobs, run outside the web request | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The call into the Calculator, with the binary's digest checked | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The governor's meter | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The derivation class written at landing, and the kernel checker once test T5 has passed | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Version 1's landing scenarios replayed with the Calculator as the only calculator | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The Research Client in Python, calling the Calculator | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The agent-contract bundle, placed by the client | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The execution challenge | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| Retry-After obeyed | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The session log | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| A petition, a push and a release against the rehearsal wiki from machine 2 | NOT STARTED | Operator | 2026-12-20 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The bootstrap test: each family, given only this wiki's address, reproduces the spring's derivation | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| The certification suite and the conformance probes, each family in turn | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| The names check, the digest convention and the execution challenge, from each family's tools | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| Each vendor's thin implementation, derived from the Agent Contract | NOT STARTED | Agent | 2027-01-03 | 2026-10-14 |
| The agent-contract bundle's changes declared as a new version | NOT STARTED | Declarer | 2027-01-03 | 2026-10-14 |
| The walk-through, revised by hand with the new words, readable to each family's reader | NOT STARTED | Agent | 2027-01-03 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| A certified agent's lifecycle on the synthetic UWC, for each certified family | NOT STARTED | Agent | 2027-01-13 | 2026-10-14 |
| The Calculator and Custos deployed on the host | NOT STARTED | Operator | 2027-01-13 | 2026-10-14 |
| Version 1's pages left untouched, with a banner pointing forward | NOT STARTED | Declarer | 2027-01-13 | 2026-10-14 |
| TPM marked historical on its hub | NOT STARTED | Declarer | 2027-01-13 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The Principia Framework Specification 1.0.0 and the Calculator 1.0.0 declared | NOT STARTED | Declarer | 2027-01-13 2026-12-09 to 2027-03-03 |
2026-10-14 |
Figure 7: the phases
Figure 7. The seven phases, in order, drawn from the status panel: Phase 0 done; Phases 1 and 2 under way; Phases 3 to 6 not started. The current focus is Phase 1, the lowest phase not done. A phase may begin before the one before it is done. Every state is written in its box; the colours repeat it: green, done; blue, under way; grey, not started; a heavier outline, the current focus.
This panel
| Item | State | Owner | Checked |
|---|---|---|---|
| Figure 7 copies current: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs | UNDER WAY | Declarer | 2026-10-18 |
as of 2026-10-18