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-17
Phase 0UNDER WAY
Phase 1UNDER WAY
Phase 2UNDER WAY
Phase 3NOT STARTED
Phase 4NOT STARTED
Phase 5NOT STARTED
Phase 6NOT STARTED
First releaseNOT STARTED
Faults
No faults
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 | NOT STARTED | Operator | 2026-10-18 | 2026-10-15 |
| 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: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-15 |
| Test T3: a hundred calls in one scheduled run, against the hourly budget: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-15 |
| Test T5: a proof checked on the host by an independent Lean kernel checker: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-15 |
| 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: six specification texts and the full sources of version 1's server extension and research client wait on the Operator's copy | PARTIAL 6 of 8 | Operator | 2026-10-18 | 2026-10-15 |
| 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: built; the monthly task waits on the Declarer | UNDER WAY | Agent | 2026-10-18 | 2026-10-15 |
| 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: the account is owed | NOT STARTED | Operator | 2026-10-18 | 2026-10-15 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Digests and canonical serialization: SHA-256 is written in Lean and version 1's digest test cases pass; the digests of the specification and of the instruction set follow | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Units and dimensions: all seven of version 1's unit functions, with all of its test cases; the Calculator's command for them takes its final form with canonical serialization | PARTIAL 7 of 8 | Agent | 2026-11-26 | 2026-10-15 |
| The zones: Starting Set, Correspondence Table, Criteria Set: the checks are ported, the declared forms read in them; the zones' digests and the full Unicode tables wait on the Declarer's choices | PARTIAL 1 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Declared forms: ported and run against version 1's 555 test cases; three that hold characters beyond the interim table wait on the Declarer's choice of Unicode's tables | PARTIAL 1 of 2 | Agent | 2026-11-26 | 2026-10-15 |
| Fundamental tests and isomorphism checks: the tests and checks are ported, the declared forms read in them; 2 of version 1's test cases wait on the Declarer's choice of Unicode's tables | PARTIAL 1 of 2 | Agent | 2026-11-26 | 2026-10-15 |
| Records and the register functions: the functions are ported; the record digests wait on the Declarer's choice of SHA-256 | PARTIAL 1 of 2 | Agent | 2026-11-26 | 2026-10-15 |
| The strike rule, distance, SR8 and SR9: version 1's five test sets pass; its call on the Calculator's command line follows canonical serialization | PARTIAL 5 of 6 | Agent | 2026-11-26 | 2026-10-15 |
| Hold scope: the hold and release records' digests wait on the Declarer's choice of SHA-256 | PARTIAL 4 of 6 | Agent | 2026-11-26 | 2026-10-15 |
| The structure check of the equations of motion: version 1's two test sets pass; its call on the Calculator's command line follows canonical serialization | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Provisions: the functions are ported, with the kinds Interaction and Convention; their digests and Unicode normalization beyond the interim tables wait on the Declarer's choices | PARTIAL 1 of 2 | Agent | 2026-11-26 | 2026-10-15 |
| Probes and their comparison: version 1's test cases computed, all agreeing; the draws wait on the Declarer's choice of SHA-256, and one text on Unicode's tables | PARTIAL 168 of 252 | Agent | 2026-11-26 | 2026-10-15 |
| Score and beta: ported with exact values, all of version 1's test cases passing, the user score's evidence with them now that the sponsor's functions are ported; the Calculator's command for the family follows | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Cluster | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Falcons: the functions are ported, 820 of version 1's 949 test cases passing; the digests and Unicode normalization beyond the stopgap wait on the Declarer's choices; the Calculator's command follows | PARTIAL 1 of 4 | Agent | 2026-11-26 | 2026-10-15 |
| Bibliography: the functions are ported; the canonical entry's digest and Unicode normalization beyond ASCII wait on the Declarer's choices | PARTIAL 1 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Identity, sponsor and lint: identity and lint are ported, the prompt digest and Unicode normalization beyond the interim tables waiting on the Declarer's choices; sponsor waits on beta | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Governor and permissions: the permissions function and the governor's admission; five questions on admission wait on the Declarer; the pressure levels, then the traffic stages, follow | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| 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-15 |
| The generated specification pages and their converter, shipped with each release | NOT STARTED | Agent | 2026-11-26 | 2026-10-14 |
| 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: Phases 0 to 2 under way; Phases 3 to 6 not started. The current focus is Phase 0, 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: both copies match this page's | DONE | Declarer | 2026-10-17 |
as of 2026-10-17