The Invariance Itself - Recent changes [en]

Principia Machina/Progress/Status

PMA Progress — Wed, 21 Oct 2026 02:50:30 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:50, 21 October 2026
Line 10:		Line 10:
	<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-21</div>		<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-21</div>
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22~~</span><span class="pma-tile-flag pma-lamp-red">1 FAULT~~</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">13 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">16 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">16 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>
	<div class="pma-tile pma-lamp-~~grey~~"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">~~NOT STARTED~~</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">1 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 5</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2027-01-03</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 5</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2027-01-03</span></div>
Line 20:		Line 20:

	== Faults ==		== Faults ==
	<div class="pma-~~panel-wrap~~">		<div class="pma-faults"><span class="pma-label pma-lamp-green">No faults</span></div>
	{\| class="pma-~~panel~~ pma-~~faults"~~
	~~! class="pma-c-phase" \| Phase !! Item !! class="pma-c-state" \| Fault !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected~~
	\|-
	~~\| Phase 1 \|\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note~~">~~: FAIL in one scheduled run, 100 of 100 calls failed (call 1: exit -1); the whole run used 1.418 CPU-seconds, under the budget of 400; the Declarer decides what follows~~</span> ~~\|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18~~
	\|}
	</div>

	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-20 \|\| 19:50 PDT \|\| 2026-10-21 02:50
	\|-		\|-
	\| 2026-10-20 \|\| 19:45 PDT \|\| 2026-10-21 02:45		\| 2026-10-20 \|\| 19:45 PDT \|\| 2026-10-21 02:45
	\|-		\|-
	\| 2026-10-18 \|\| 19:29 PDT \|\| 2026-10-19 02:29		\| 2026-10-18 \|\| 19:29 PDT \|\| 2026-10-19 02:29
	\|-
	~~\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15~~
	\|}		\|}

Line 57:		Line 51:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-20		\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-21
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 64:		Line 58:
	\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: ~~FAIL in one scheduled run~~, ~~100~~ of 100 calls failed ~~(call 1: exit -1); the whole~~ run ~~used 1.418 CPU-seconds,~~ under the ~~budget of 400; the Declarer decides what follows~~</span> \|\| class="pma-lamp pma-lamp-~~red~~" \| ~~OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span>~~ \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-20		\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: PASS on the server the Operator controls, 0 of 100 calls failed from a scheduled run and under the job runner's limits</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|-		\|-
	\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
Line 80:		Line 74:
	\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
	\|-		\|-
	\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-20		\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|-		\|-
	\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
Line 135:		Line 129:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 3\|Phase 3]]: Custos · checked 2026-10-14		\|+ [[Principia Machina/Progress/Phase 3\|Phase 3]]: Custos · checked 2026-10-21
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
	\| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4 \|\| class="pma-lamp pma-lamp-~~grey~~" \| ~~NOT STARTED~~ \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-12-13 \|\| class="pma-wide pma-date" \| 2026-10-14		\| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4<span class="pma-note">: made on demand on a fresh server by the provisioning script, when a release needs one</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-12-13 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|-		\|-
	\| Custos's page classes \|\| class="pma-lamp pma-lamp-grey" \| NOT STARTED \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-12-13 \|\| class="pma-wide pma-date" \| 2026-10-14		\| Custos's page classes \|\| class="pma-lamp pma-lamp-grey" \| NOT STARTED \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-12-13 \|\| class="pma-wide pma-date" \| 2026-10-14
Line 225:		Line 219:
	P1 [label="Phase 1 Foundations\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];		P1 [label="Phase 1 Foundations\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];
	P2 [label="Phase 2 The Calculator\nunder way", fillcolor="#cedff2", color="#6a8fbf"];		P2 [label="Phase 2 The Calculator\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
	P3 [label="Phase 3 Custos\~~nnot started~~"];		P3 [label="Phase 3 Custos\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
	P4 [label="Phase 4 The Research Client\nnot started"];		P4 [label="Phase 4 The Research Client\nnot started"];
	P5 [label="Phase 5 Other model families\nnot started"];		P5 [label="Phase 5 Other model families\nnot started"];
Line 234:		Line 228:
	</graphviz>		</graphviz>
	</div>		</div>
	<div class="pma-caption">'''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.</div>		<div class="pma-caption">'''Figure 7.''' The seven phases, in order, drawn from the status panel: Phase 0 done; Phases 1 to 3 under way; Phases 4 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.</div>

	== This panel ==		== This panel ==

Principia Machina/Progress/Log

PMA Progress — Wed, 21 Oct 2026 02:50:30 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:50, 21 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-21, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the wiki moved to the server the Operator controls
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks
Line 7:		Line 8:
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees
			* 2026-10-21, [[Principia Machina/Progress/Phase 3\|Phase 3]]: the rehearsal wiki
	* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it		* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it
	* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it		* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it
Line 17:		Line 19:
	* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly		* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly
	* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk		* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk
			* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: tests T1, T2, T3 and T5 run again on a server the Operator controls, built from nothing by one provisioning script
	* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed		* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed
	* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source		* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source

Principia Machina/Progress/Phase 3

PMA Progress — Wed, 21 Oct 2026 02:50:29 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:50, 21 October 2026
Line 6:		Line 6:

	== Done ==		== Done ==
			* 2026-10-21: the rehearsal wiki: made when a release needs one, on a fresh server, by the same provisioning script that built the wiki's server, running the same software. The standing rehearsal copy used before the move is retired.

	== Open ==		== Open ==
	* The rehearsal wiki on the host's subdomain, the Operator's act, with its accounts.
	* The Calculator's residence on the host and the step that places a released binary there.		* The Calculator's residence on the host and the step that places a released binary there.

Principia Machina/Progress/Phase 1

PMA Progress — Wed, 21 Oct 2026 02:50:28 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:50, 21 October 2026
Line 31:		Line 31:
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
			* 2026-10-19: tests T1, T2, T3 and T5 run again on a server the Operator controls, built from nothing by one provisioning script: every test passes. Test T3's hundred calls pass from the shell, from a scheduled run and under the job runner's limits, 0 of 100 failing each time; every context the wiki starts a program from now admits the address space the Calculator reserves.
	* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.		* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.
	* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.		* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.
			* 2026-10-21: the wiki moved to the server the Operator controls. Its database and its uploads were copied whole and checked row for row against the old host before the switch: every count, the hidden revisions and every upload's checksum equal. The old host was kept read-only during the move and is no longer the wiki's home.

	== Open ==		== Open ==

Principia Machina/Progress/Status

PMA Progress — Wed, 21 Oct 2026 02:45:58 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 8:		Line 8:

	<div class="pma-strip">		<div class="pma-strip">
	<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-19</div>		<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-21</div>
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span><span class="pma-tile-flag pma-lamp-red">1 FAULT</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span><span class="pma-tile-flag pma-lamp-red">1 FAULT</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">15 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">16 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>
Line 30:		Line 30:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-20 \|\| 19:45 PDT \|\| 2026-10-21 02:45
	\|-		\|-
	\| 2026-10-18 \|\| 19:29 PDT \|\| 2026-10-19 02:29		\| 2026-10-18 \|\| 19:29 PDT \|\| 2026-10-19 02:29
	\|-		\|-
	\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15		\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15
	\|-
	~~\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23~~
	\|}		\|}

Line 57:		Line 57:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-19		\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-20
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 64:		Line 64:
	\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 100 of 100 calls failed (call 1: exit -1); the whole run used 1.418 CPU-seconds, under the budget of 400; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span> \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-19		\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 100 of 100 calls failed (call 1: exit -1); the whole run used 1.418 CPU-seconds, under the budget of 400; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span> \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-20
	\|-		\|-
	\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
Line 80:		Line 80:
	\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
	\|-		\|-
	\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-19		\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-20
	\|-		\|-
	\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
Line 91:		Line 91:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 2\|Phase 2]]: The Calculator · checked 2026-10-19		\|+ [[Principia Machina/Progress/Phase 2\|Phase 2]]: The Calculator · checked 2026-10-21
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 104:		Line 104:
	\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Records and the register functions~~<span class="pma-note">: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification</span>~~ \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 3 of 4~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19		\| Records and the register functions \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-20
	\|-		\|-
	\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
Line 126:		Line 126:
	\| Identity, sponsor and lint \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Identity, sponsor and lint \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19		\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|-		\|-
	\| The structured derivation checker, with its soundness proof<span class="pma-note">: 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~~</span> \|\| class="pma-lamp pma-lamp-~~amber~~" \| ~~UNDER WAY~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19		\| The structured derivation checker, with its soundness proof<span class="pma-note">: the checker, its credit and the command that credits a record's derivation; approximation steps with checked bounds follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 1 of 2 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|-		\|-
	\| The generated specification pages and their converter, shipped with each release<span class="pma-note">: the program that reads the checked library; the converter, its checks ~~and~~ the rewrite of the comments the pages carry ~~follow~~</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19		\| The generated specification pages and their converter, shipped with each release<span class="pma-note">: the program that reads the checked library and the converter with its checks; the rewrite of the comments the pages carry follows</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-21
	\|}		\|}
	</div>		</div>
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ Phase 3: Custos · checked 2026-10-14		\|+ [[Principia Machina/Progress/Phase 3\|Phase 3]]: Custos · checked 2026-10-14
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 241:		Line 241:
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked
	\|-		\|-
	\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-19		\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-21
	\|}		\|}
	</div>		</div>

	as of 2026-10-19		as of 2026-10-21

Principia Machina/Progress/Log

PMA Progress — Wed, 21 Oct 2026 02:45:58 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bibliography's checks on the Calculator's command line
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees
			* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the fundamental tests on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the governor's admission on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: SHA-256 and Unicode's normalization on the Calculator's command line, so that an agent's own tools can be checked against the Calculator's
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the permissions function on the Calculator's command line, beside the command that reads words
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the zones on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the converter that writes the specification pages from what the checked library gives, with its checks
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly
	* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk		* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk
	* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed		* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed
Line 7:		Line 21:
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended
			* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the runner's step that requires a check now names the service that posts it
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
Line 141:		Line 156:
	* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton		* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton

	as of 2026-10-19		as of 2026-10-21

Principia Machina/Progress/Phase 3

PMA Progress — Wed, 21 Oct 2026 02:45:57 GMT

Progress pages rendered from the Principia Machina source

New page

{{DISPLAYTITLE:Phase 3}}
{{Principia Machina map}}
'''Phase 3: Custos'''

Goal: the wiki's thin gatekeeper, Custos, built against a rehearsal wiki running the host's software: its page classes, its API module, its jobs run outside the web request, its call into the Calculator with the binary's digest checked, the governor's meter, the derivation class written at landing and the kernel checker, and version 1's landing scenarios replayed with the Calculator as the only calculator.

== Done ==

== Open ==
* The rehearsal wiki on the host's subdomain, the Operator's act, with its accounts.
* The Calculator's residence on the host and the step that places a released binary there.

== Next ==

The first unit: the extension's skeleton, the store seam, the call into the Calculator with the digest check, and a harness that runs without the host.

as of 2026-10-21

Principia Machina/Progress/Phase 2

PMA Progress — Wed, 21 Oct 2026 02:45:56 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 59:		Line 59:
	* 2026-10-18: the Calculator's command for units and dimensions, in its final form: version 1's seven unit functions, each taking version 1's arguments and answering with version 1's lists in canonical JSON, every number exact. All 91 of version 1's unit test cases pass through it, 5 of them as the recorded differences, and so do the 26 hand-written cases of the seven functions. A unit's scale is now held in lowest terms, and the bound on the size of an exact number is built for the units: a scale, a value or a comparison that would cross it is refused as too large, a scale exactly when its numerator or denominator passes the bound, and Lean proves that every answer given is the one given before. The scale factor over measurements whose units carry different powers of pi, and a comparison across powers of pi that pi to 4096 bits does not decide, are refused as owed. The command refuses a unit of more than 1024 characters or 128 tokens, a decimal of more than 4096 characters, and more than 100 measurements, or one of more than 30 digits, for the scale factor, the strike rule's bounds.		* 2026-10-18: the Calculator's command for units and dimensions, in its final form: version 1's seven unit functions, each taking version 1's arguments and answering with version 1's lists in canonical JSON, every number exact. All 91 of version 1's unit test cases pass through it, 5 of them as the recorded differences, and so do the 26 hand-written cases of the seven functions. A unit's scale is now held in lowest terms, and the bound on the size of an exact number is built for the units: a scale, a value or a comparison that would cross it is refused as too large, a scale exactly when its numerator or denominator passes the bound, and Lean proves that every answer given is the one given before. The scale factor over measurements whose units carry different powers of pi, and a comparison across powers of pi that pi to 4096 bits does not decide, are refused as owed. The command refuses a unit of more than 1024 characters or 128 tokens, a decimal of more than 4096 characters, and more than 100 measurements, or one of more than 30 digits, for the scale factor, the strike rule's bounds.
	* 2026-10-19: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source. It still gives the same document every time, byte for byte.		* 2026-10-19: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source. It still gives the same document every time, byte for byte.
			* 2026-10-20: the Calculator's command line checks a structured derivation and credits it. Given a record's structured steps, its result's equation, the Starting Set and the register, it reads the steps, gathers the laws the record may cite (the Starting Set's laws and the ASSUMPTION records the record names, and nothing else), checks the steps against them and answers the verdict with the step and the reason where it fails, and the class the derivation earns: mechanically checked only when the checker accepts it, read by inspection otherwise. A second call takes a whole record and tells its derivation's form by its shape: a prose derivation earns inspection, a structured one is checked as above, and a proof for the Lean checker is answered as owed, since that class is the proof checker's to give; a record that mixes the forms is refused. A third call lists the laws a derivation is checked against. Lean proves that the command answers mechanically checked exactly when the checker accepts, so that the result's equation then follows from the Starting Set's laws and the record's assumptions, and that it never answers proved. The derivation's written form, the three forms together, is proved to read back unchanged. Bounds keep every accepted request short: 1,024 steps, equations of 16,384 characters, 64 entries in each part of the Starting Set, 1,024 records in the register and 512 assumptions; the slowest accepted request found took 0.39 s. The 30 hand-written records and 28 written forms run through the command and come out as written. The tests of version 1's text differences, fingerprints, execution challenge and volunteer work are not this phase's: the execution challenge belongs to the Research Client, the other three to Custos, the server-side gatekeeper.
			* 2026-10-20: the fundamental tests on the Calculator's command line: T2's findings on a proposition and its atomicity check, T3's consistency, T5's yield of the degrees of freedom, their whole run, the isomorphism checks of a Correspondence Table and the final pass over a Research Assembly, each in version 1's form; the run takes the name "fundamental tests". All 120 of their test cases pass through the command line, none owed. A request holds at most 64 entries in a list, 16,384 characters in a string and 131,072 in all; the slowest request found at those bounds takes a quarter of a second.
			* 2026-10-20: the governor's admission on the Calculator's command line: one call decides a request from what Custos has recorded and gives the charge to apply when it is admitted, in the governor's own words; beside it the request's lane, the seats an operation costs and the jitter of a wait. All 709 of the governor's test cases pass through the command line, 4 of them answered as owed: the seats of a falcon's return whose rows are not a whole number of 20 stay the Declarer's open choice.
			* 2026-10-20: SHA-256 and Unicode's normalization on the Calculator's command line, so that an agent's own tools can be checked against the Calculator's: the digest of bytes or of a text, a text's two normal forms, and the general category of each of its characters. All 129 of NIST's test messages and the standard's 3 examples give their digests through it, and all 19,074 lines of Unicode's normalization test pass through it. A text of more than 131,072 characters is refused; at that size the slowest normalization found takes under 1.5 seconds.
			* 2026-10-20: the permissions function on the Calculator's command line, beside the command that reads words: the same words give the same answer, and a second call lists every asker, page class, operation and context, so that Custos can build its table of who may do what from the Calculator alone. Every test case of the permissions function passes through it.
			* 2026-10-20: the zones on the Calculator's command line: the checks of the Starting Set, the Correspondence Table and the Criteria Set, each answering whether the zone passes and its problems; a Criteria Set term's canonical spelling; each zone's preimage and digest, the Research Assembly's digest and the class of a successor; and the canonical forms of a dimension and a decimal. The functions whose earlier names carried earlier codes take the Research Assembly's words. All 335 of the zones' test cases pass through the command line, none owed. A request holds at most 1,024 entries in a list, 32,768 characters in a string and 131,072 in all; the slowest request found at those bounds takes about 3 seconds.
			* 2026-10-20: the converter that writes the specification pages from what the checked library gives, with its checks. It writes one page for each source file of the library and a page that lists them; each page shows the file's comments where they stand among its definitions and theorems, each definition's source text and each theorem's statement with the axioms its proof rests on. A comment is read under a small set of formatting rules, and anything outside them is refused, never passed on. A page that would name a file of the development record, an issue or a decision is refused, and a check builds every page again and compares it letter for letter. A list of the comments still to be rewritten comes with it: 683 places in 101 files today.
			* 2026-10-20: the verification's difference, its uncertainty and its zeta, computed exactly: the difference of the two measured values, the square root of the sum of their uncertainties' squares and the difference over that root, each rounded once to twelve significant digits, with the strike rule's contradiction test beside them. Version 1 computed them in floating point; its 17 test cases for the verification all give its answer, and with them all 932 test cases of the register functions and all 1,145 through the Calculator's command, none owed. Measurements in units that carry pi, a degree against a radian, are answered from bounds on pi; a number past the bound on the size of an exact number is refused as too large. Lean proves that the bounded computation gives the exact one, that the uncertainty is zero only when both uncertainties are, that the zeta has the difference's sign, and that the contradiction test is the strike rule's.
			* 2026-10-21: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed): a literal and a binding are refused as too large when their value passes the bound, and the Calculator proves that every exact number the evaluator forms, from bindings it has read, is within the bound. All 555 of the forms' test cases and the 53 hand-written evaluator cases answer as before; five new cases check the bound.
			* 2026-10-21: the bound on the size of an exact number, built for the yardsticks: a yardstick's weights, each record's field value and steps, and every product and running sum of a weighted sum are checked against the bound before they are formed, and a value that would cross it is refused as too large. When the checked yardstick answers, it answers exactly as before: the Calculator proves it for the key, the checks and the harness. All 46 of the yardsticks' test cases answer through the checked functions as before; none is near the bound. The cluster and the declared forms follow.
			* 2026-10-21: the bibliography's checks on the Calculator's command line: the reading of a DOI, an arXiv identifier, an ISBN, an ISSN, a PubMed and a PubMed Central identifier, the key form and the duplicate key, the check of a proposed entry, its canonical form and digest, the registry address, the comparison with what a registry returned, the withdrawal notice, the literature view and the hold list, each answering in the structure of version 1's answer. All 405 of the bibliography's test cases pass through the command line. A request holds at most 1,024 entries in a list, 64 identifiers, 16,384 characters in a string and 131,072 in all; the slowest request found takes 0.28 seconds.
			* 2026-10-21: hold scope on the Calculator's command line: the blocks held after a failed canary, the records held in a register, an identifier from the range Custos reserves (the name "allocate identifiers"), the HOLD record and its preimage, and the RELEASE record, each in version 1's form with its digest. All 140 of their test cases pass through the command line. A request holds at most 4,000 entries in a list, 1,000 records of a register, 16,384 characters in a string and 262,144 in all; the slowest request found, the records held along a chain of 1,000 citations, takes 2.4 seconds.
			* 2026-10-21: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees: its twelve digits are settled from bounds on pi, as the declared forms settle them, where they were refused as owed before. A value whose twelve digits bounds on pi of up to 4096 bits do not settle is still refused as owed. The rest of the strike rule's work with powers of pi, the scale factor over measurements whose units carry different powers of pi, follows.

	== Open ==		== Open ==
	* Declared forms: the evaluation follows the standing choice of exact values; a choice of binary floating point would change it in one place.		* Declared forms: the evaluation follows the standing choice of exact values; a choice of binary floating point would change it in one place.
	* The structured derivation checker: approximations beyond citing an ASSUMPTION record, and a call on the Calculator's command line that checks a record's derivation and credits it.		* The specification pages: the rewrite of the comments the pages carry, so that none names a file, an issue or a decision, one change for each top folder of the library.
	* The specification pages: ~~the converter that writes them from what the library gives, its checks, and~~ the rewrite of the comments the pages carry, so that none names a file, an issue or a decision~~. What such a comment may still cite~~, ~~and how a page is laid out, wait on~~ the ~~Declarer~~.		* The bound on the size of an exact number: built for the strike rule, the probes, the units, score, beta and the sponsor's user evidence, the records, the yardsticks and the declared forms; the cluster follows.
	* The bound on the size of an exact number: built for the strike rule, the probes, the units, score, beta and the sponsor's user evidence, ~~and~~ the records; the ~~cluster,~~ the declared forms ~~and the yardstick follow, in that order.~~
	* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification; the ~~Calculator answers them as owed~~.
	* Units and dimensions: the scale factor over measurements whose units carry different powers of pi is refused as owed until the strike rule takes them.		* Units and dimensions: the scale factor over measurements whose units carry different powers of pi is refused as owed until the strike rule takes them.
	* The governor: the pressure levels, then the traffic stages, each a later step of the admission function, in that order.		* The governor: the pressure levels, then the traffic stages, each a later step of the admission function, in that order.
			* The structured derivation checker: approximation steps, each with a bound on its error that the checker verifies, a unit of its own after the move to the mathematics library.
			* Records: the record check reads a structured or proof derivation in the written form the derivation command reads; today it reads the prose form alone.

	== Next ==		== Next ==
Line 73:		Line 86:
	The next function families in the order of the plan.		The next function families in the order of the plan.

	as of 2026-10-19		as of 2026-10-21

Principia Machina/Progress/Phase 1

PMA Progress — Wed, 21 Oct 2026 02:45:55 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 32:		Line 32:
	* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
	* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.		* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.
			* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.

	== Open ==		== Open ==
Line 40:		Line 41:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

	as of 2026-10-19		as of 2026-10-21

Principia Machina/Progress/Phase 0

PMA Progress — Wed, 21 Oct 2026 02:45:55 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 64:		Line 64:
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
	* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.		* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.
			* 2026-10-18: the runner's step that requires a check now names the service that posts it. Before adding a check to the set every change must pass, the step lists each check already required and which service it is bound to, binds the new one to the same service, and refuses, naming both, a check already required under another: requiring a check from a service that no longer posts it would have held every change.
	* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.		* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.

Line 73:		Line 74:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-19		as of 2026-10-21

Principia Machina/Progress/Log

PMA Progress — Mon, 19 Oct 2026 19:52:30 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 19 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk
			* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed
	* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source		* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one

Principia Machina/Progress/Phase 1

PMA Progress — Mon, 19 Oct 2026 19:52:28 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 19 October 2026
Line 31:		Line 31:
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
			* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.

	== Open ==		== Open ==

Principia Machina/Progress/Phase 0

PMA Progress — Mon, 19 Oct 2026 19:52:27 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 19 October 2026
Line 64:		Line 64:
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
	* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.		* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.
			* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.

	== Open ==		== Open ==

Principia Machina/Progress/Status

PMA Progress — Mon, 19 Oct 2026 02:29:54 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:29, 19 October 2026
Line 30:		Line 30:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-18 \|\| 19:29 PDT \|\| 2026-10-19 02:29
	\|-		\|-
	\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15		\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15
	\|-		\|-
	\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23		\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23
	\|-
	~~\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07~~
	\|}		\|}

Line 91:		Line 91:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 2\|Phase 2]]: The Calculator · checked 2026-10-18		\|+ [[Principia Machina/Progress/Phase 2\|Phase 2]]: The Calculator · checked 2026-10-19
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 104:		Line 104:
	\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Records and the register functions<span class="pma-note">: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 3 of 4 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Records and the register functions<span class="pma-note">: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 3 of 4 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|-		\|-
	\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
Line 126:		Line 126:
	\| Identity, sponsor and lint \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Identity, sponsor and lint \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|-		\|-
	\| The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|-		\|-
	\| The generated specification pages and their converter, shipped with each release<span class="pma-note">: the program that reads the checked library; the converter, its checks and the rewrite of the comments the pages carry follow</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The generated specification pages and their converter, shipped with each release<span class="pma-note">: the program that reads the checked library; the converter, its checks and the rewrite of the comments the pages carry follow</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|}		\|}
	</div>		</div>

Principia Machina/Progress/Log

PMA Progress — Mon, 19 Oct 2026 02:29:52 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:29, 19 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended

Principia Machina/Progress/Phase 2

PMA Progress — Mon, 19 Oct 2026 02:29:51 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:29, 19 October 2026
Line 58:		Line 58:
	* 2026-10-18: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line: whether a quantity is compared by machine or listed for inspection, a record's conditions, the pairs of records the contradiction test compares, and the groups the scale factor is computed over. Each takes version 1's arguments and answers as version 1 did, its refusals included, and all 125 of version 1's test cases for them pass through the command line, so all five of version 1's test sets for the strike rule now run there. The conditions of a record with a point whose value in SI units carries a power of pi are refused as owed: their twelve digits need the digits of pi, which the Calculator does not compute for them yet. The command refuses a request too large to answer in good time: more than 2,000 records, or 5,000 assumptions and citations, for a record's conditions; more than 200 records, or 500 assumptions and citations, for the pairs and the groups; more than 1,000 points in all, a point's value or unit of more than 64 characters, and a point whose value in SI units holds more than 2,048 bits above or below its fraction line.		* 2026-10-18: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line: whether a quantity is compared by machine or listed for inspection, a record's conditions, the pairs of records the contradiction test compares, and the groups the scale factor is computed over. Each takes version 1's arguments and answers as version 1 did, its refusals included, and all 125 of version 1's test cases for them pass through the command line, so all five of version 1's test sets for the strike rule now run there. The conditions of a record with a point whose value in SI units carries a power of pi are refused as owed: their twelve digits need the digits of pi, which the Calculator does not compute for them yet. The command refuses a request too large to answer in good time: more than 2,000 records, or 5,000 assumptions and citations, for a record's conditions; more than 200 records, or 500 assumptions and citations, for the pairs and the groups; more than 1,000 points in all, a point's value or unit of more than 64 characters, and a point whose value in SI units holds more than 2,048 bits above or below its fraction line.
	* 2026-10-18: the Calculator's command for units and dimensions, in its final form: version 1's seven unit functions, each taking version 1's arguments and answering with version 1's lists in canonical JSON, every number exact. All 91 of version 1's unit test cases pass through it, 5 of them as the recorded differences, and so do the 26 hand-written cases of the seven functions. A unit's scale is now held in lowest terms, and the bound on the size of an exact number is built for the units: a scale, a value or a comparison that would cross it is refused as too large, a scale exactly when its numerator or denominator passes the bound, and Lean proves that every answer given is the one given before. The scale factor over measurements whose units carry different powers of pi, and a comparison across powers of pi that pi to 4096 bits does not decide, are refused as owed. The command refuses a unit of more than 1024 characters or 128 tokens, a decimal of more than 4096 characters, and more than 100 measurements, or one of more than 30 digits, for the scale factor, the strike rule's bounds.		* 2026-10-18: the Calculator's command for units and dimensions, in its final form: version 1's seven unit functions, each taking version 1's arguments and answering with version 1's lists in canonical JSON, every number exact. All 91 of version 1's unit test cases pass through it, 5 of them as the recorded differences, and so do the 26 hand-written cases of the seven functions. A unit's scale is now held in lowest terms, and the bound on the size of an exact number is built for the units: a scale, a value or a comparison that would cross it is refused as too large, a scale exactly when its numerator or denominator passes the bound, and Lean proves that every answer given is the one given before. The scale factor over measurements whose units carry different powers of pi, and a comparison across powers of pi that pi to 4096 bits does not decide, are refused as owed. The command refuses a unit of more than 1024 characters or 128 tokens, a decimal of more than 4096 characters, and more than 100 measurements, or one of more than 30 digits, for the scale factor, the strike rule's bounds.
			* 2026-10-19: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source. It still gives the same document every time, byte for byte.

	== Open ==		== Open ==

Principia Machina/Progress/Log

PMA Progress — Mon, 19 Oct 2026 02:28:28 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:28, 19 October 2026
Line 3:		Line 3:
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
			* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run

Principia Machina/Progress/Phase 0

PMA Progress — Mon, 19 Oct 2026 02:28:26 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:28, 19 October 2026
Line 63:		Line 63:
	* 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.		* 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.
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
			* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.

	== Open ==		== Open ==

Principia Machina/Progress/Status

PMA Progress — Mon, 19 Oct 2026 02:15:47 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:15, 19 October 2026
Line 24:		Line 24:
	! class="pma-c-phase" \| Phase !! Item !! class="pma-c-state" \| Fault !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected		! class="pma-c-phase" \| Phase !! Item !! class="pma-c-state" \| Fault !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected
	\|-		\|-
	\| Phase 1 \|\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds ~~for 100 calls against a cap~~ of ~~4000 an hour~~; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18		\| Phase 1 \|\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 100 of 100 calls failed (call 1: exit -1); the whole run used 1.418 CPU-seconds, under the budget of 400; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18
	\|}		\|}
	</div>		</div>
Line 30:		Line 30:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-18 \|\| 19:15 PDT \|\| 2026-10-19 02:15
	\|-		\|-
	\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23		\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23
	\|-		\|-
	\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07		\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07
	\|-
	~~\| 2026-10-18 \|\| 09:08 PDT \|\| 2026-10-18 16:08~~
	\|}		\|}

Line 57:		Line 57:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-18		\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-19
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 64:		Line 64:
	\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds ~~for 100 calls against a cap~~ of ~~4000 an hour~~; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span> \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 100 of 100 calls failed (call 1: exit -1); the whole run used 1.418 CPU-seconds, under the budget of 400; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span> \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|-		\|-
	\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
Line 80:		Line 80:
	\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
	\|-		\|-
	\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-19
	\|-		\|-
	\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14

Principia Machina/Progress/Phase 1

PMA Progress — Mon, 19 Oct 2026 02:15:45 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:15, 19 October 2026
Line 29:		Line 29:
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls ~~took~~ 1.418 CPU-seconds ~~together~~, ~~against~~ 10 per cent of an hourly cap of 4000 ~~CPU-seconds~~: FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.

Principia Machina/Progress/Status

PMA Progress — Mon, 19 Oct 2026 01:23:42 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:23, 19 October 2026
Line 30:		Line 30:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-18 \|\| 18:23 PDT \|\| 2026-10-19 01:23
	\|-		\|-
	\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07		\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07
	\|-		\|-
	\| 2026-10-18 \|\| 09:08 PDT \|\| 2026-10-18 16:08		\| 2026-10-18 \|\| 09:08 PDT \|\| 2026-10-18 16:08
	\|-
	~~\| 2026-10-18 \|\| 08:43 PDT \|\| 2026-10-18 15:43~~
	\|}		\|}

Line 57:		Line 57:
	<div class="pma-panel-wrap">		<div class="pma-panel-wrap">
	{\| class="pma-panel"		{\| class="pma-panel"
	\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-17		\|+ [[Principia Machina/Progress/Phase 1\|Phase 1]]: Foundations · checked 2026-10-18
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected !! class="pma-wide pma-c-date" \| Checked
	\|-		\|-
Line 80:		Line 80:
	\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| The terminology map \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
	\|-		\|-
	\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-17		\| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-22 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| Publishing the framework's pages from the source, by the Declarer's act \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14

Principia Machina/Progress/Log

PMA Progress — Mon, 19 Oct 2026 01:23:41 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:23, 19 October 2026
Line 5:		Line 5:
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
			* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons

Principia Machina/Progress/Phase 1

PMA Progress — Mon, 19 Oct 2026 01:23:39 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:23, 19 October 2026
Line 30:		Line 30:
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.
			* 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.

	== Open ==		== Open ==

Principia Machina/Progress/Status

PMA Progress — Mon, 19 Oct 2026 00:07:35 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 8:		Line 8:

	<div class="pma-strip">		<div class="pma-strip">
	<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-18</div>		<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-19</div>
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span><span class="pma-tile-flag pma-lamp-red">1 FAULT</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span><span class="pma-tile-flag pma-lamp-red">1 FAULT</span></div>
Line 30:		Line 30:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-18 \|\| 17:07 PDT \|\| 2026-10-19 00:07
	\|-		\|-
	\| 2026-10-18 \|\| 09:08 PDT \|\| 2026-10-18 16:08		\| 2026-10-18 \|\| 09:08 PDT \|\| 2026-10-18 16:08
	\|-		\|-
	\| 2026-10-18 \|\| 08:43 PDT \|\| 2026-10-18 15:43		\| 2026-10-18 \|\| 08:43 PDT \|\| 2026-10-18 15:43
	\|-
	~~\| 2026-10-17 \|\| 21:16 PDT \|\| 2026-10-18 04:16~~
	\|}		\|}

Line 64:		Line 64:
	\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| OVERDUE<br /><span class="pma-lamp-sub">BLOCKED</span> \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
Line 241:		Line 241:
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked
	\|-		\|-
	\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-18		\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-19
	\|}		\|}
	</div>		</div>

	as of 2026-10-18		as of 2026-10-19

Principia Machina/Progress/Log

PMA Progress — Mon, 19 Oct 2026 00:07:33 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
Line 135:		Line 136:
	* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton		* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton

	as of 2026-10-18		as of 2026-10-19

Principia Machina/Progress/Phase 2

PMA Progress — Mon, 19 Oct 2026 00:07:32 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 72:		Line 72:
	The next function families in the order of the plan.		The next function families in the order of the plan.

	as of 2026-10-18		as of 2026-10-19

Principia Machina/Progress/Phase 1

PMA Progress — Mon, 19 Oct 2026 00:07:31 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 38:		Line 38:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

	as of 2026-10-18		as of 2026-10-19

Principia Machina/Progress/Phase 0

PMA Progress — Mon, 19 Oct 2026 00:07:29 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 62:		Line 62:
	* 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: 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.		* 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.
			* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.

	== Open ==		== Open ==
Line 70:		Line 71:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-18		as of 2026-10-19

Principia Machina/Progress/Status

PMA Progress — Sun, 18 Oct 2026 16:08:53 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 16:08, 18 October 2026
Line 10:		Line 10:
	<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-18</div>		<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-18</div>
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">12 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span><span class="pma-tile-flag pma-lamp-red">1 FAULT</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">15 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">15 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>
Line 20:		Line 20:

	== Faults ==		== Faults ==
	<div class="pma-faults"~~><span~~ class="pma-~~label~~ pma-~~lamp~~-~~green~~">~~No faults~~</span></div>		<div class="pma-panel-wrap">
			{\| class="pma-panel pma-faults"
			! class="pma-c-phase" \| Phase !! Item !! class="pma-c-state" \| Fault !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Projected
			\|-
			\| Phase 1 \|\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18
			\|}
			</div>

	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! 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-18 \|\| 08:43 PDT \|\| 2026-10-18 15:43
	\|-		\|-
	\| 2026-10-17 \|\| 21:16 PDT \|\| 2026-10-18 04:16		\| 2026-10-17 \|\| 21:16 PDT \|\| 2026-10-18 04:16
	\|-
	~~\| 2026-10-17 \|\| 20:16 PDT \|\| 2026-10-18 03:16~~
	\|}		\|}

Line 58:		Line 64:
	\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: ~~PASS from the shell~~, 7.~~432~~ CPU-seconds for 100 calls; the ~~scheduled run owed~~</span> \|\| class="pma-lamp pma-lamp-~~amber~~" \| ~~UNDER WAY~~ \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: FAIL in one scheduled run, 1.418 CPU-seconds for 100 calls against a cap of 4000 an hour; the Declarer decides what follows</span> \|\| class="pma-lamp pma-lamp-red" \| BLOCKED \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</span> \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17

Principia Machina/Progress/Log

PMA Progress — Sun, 18 Oct 2026 16:08:52 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 16:08, 18 October 2026
Line 3:		Line 3:
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
			* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons

Principia Machina/Progress/Phase 1

PMA Progress — Sun, 18 Oct 2026 16:08:51 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 16:08, 18 October 2026
Line 29:		Line 29:
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
			* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.

	== Open ==		== Open ==
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.

	== Next ==		== Next ==

Principia Machina/Progress/Status

PMA Progress — Sun, 18 Oct 2026 15:43:59 GMT

Progress pages rendered from the Principia Machina source

Principia Machina/Progress/Log

PMA Progress — Sun, 18 Oct 2026 15:43:58 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 15:43, 18 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons

Principia Machina/Progress/Phase 1

PMA Progress — Sun, 18 Oct 2026 15:43:56 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 15:43, 18 October 2026
Line 28:		Line 28:
	* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.		* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
			* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.

	== Open ==		== Open ==
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.
	* Version 1's specification texts at the versions the charter names: six of them still wait on the Operator's copy, as does the full source of version 1's research client.

	== Next ==		== Next ==

Principia Machina/Progress/Phase 0

PMA Progress — Sun, 18 Oct 2026 15:43:55 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 15:43, 18 October 2026
Line 65:		Line 65:
	== Open ==		== 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.		* 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.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.

	== Next ==		== Next ==

Principia Machina/Progress/Status

PMA Progress — Sun, 18 Oct 2026 04:16:05 GMT

Progress pages rendered from the Principia Machina source

Principia Machina/Progress/Log

PMA Progress — Sun, 18 Oct 2026 04:16:04 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 04:16, 18 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for identity, the sponsor and the prompt lint
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for Provisions
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the register functions
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for score and beta
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for units and dimensions, in its final form
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated
Line 16:		Line 23:
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, as the Declarer chose		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, as the Declarer chose
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: a Provision's kind read from its text, as the Declarer chose		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: a Provision's kind read from its text, as the Declarer chose
			* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Declarer's answers on the governor's admission, built
	* 2026-10-16, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2 set up by the setup script		* 2026-10-16, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2 set up by the setup script
	* 2026-10-16, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the names check runs on machine 2 from its own local list, clean over every file		* 2026-10-16, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the names check runs on machine 2 from its own local list, clean over every file

Principia Machina/Progress/Phase 2

PMA Progress — Sun, 18 Oct 2026 04:16:02 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 04:16, 18 October 2026
Line 49:		Line 49:
	* 2026-10-17: the bound on the size of an exact number, as the Declarer chose: at most 65,536 bits above its fraction line and as many below, checked from the sizes of the numbers a step combines before the step is taken, and refused past it as too large. It is built for the strike rule's scale factor and its two mechanical tests and for the probes' comparison, which the Calculator's command line computes from a request's own numbers; each is proved, when it answers, to answer what it answered before. None of version 1's test cases comes near the bound. Measurements whose sizes differ by more than about a thousand powers of ten, which once took the scale factor seconds, are now refused in a fraction of one.		* 2026-10-17: the bound on the size of an exact number, as the Declarer chose: at most 65,536 bits above its fraction line and as many below, checked from the sizes of the numbers a step combines before the step is taken, and refused past it as too large. It is built for the strike rule's scale factor and its two mechanical tests and for the probes' comparison, which the Calculator's command line computes from a request's own numbers; each is proved, when it answers, to answer what it answered before. None of version 1's test cases comes near the bound. Measurements whose sizes differ by more than about a thousand powers of ten, which once took the scale factor seconds, are now refused in a fraction of one.
	* 2026-10-17: a Provision's kind read from its text, as the Declarer chose: one that writes no force term and binds no slot is a Convention, every other an Interaction. The first catalogue's four come out as recorded, and nothing a Provision's digest covers changes.		* 2026-10-17: a Provision's kind read from its text, as the Declarer chose: one that writes no force term and binds no slot is a Convention, every other an Interaction. The first catalogue's four come out as recorded, and nothing a Provision's digest covers changes.
			* 2026-10-17: the Declarer's answers on the governor's admission, built. A request refused for want of a free slot is told to retry after 5 seconds, a tuning option, with the jitter every such wait carries. Taking the head of the queue costs one seat. A request that costs more than its payer may spend at once is admitted when that payer has nothing left to drain, and charged in full. With the governor switched off, admission drops the rate alone: the Operator's stop on agents, an account's suspension and the slots still refuse, and nothing is charged. All 709 of the governor's hand-written test cases pass. Proved: every refusal for want of a slot carries its wait, within the jitter's share; with the governor off nothing is refused on budget and nothing charged; the stop and the suspension refuse whether the governor is on or off; and a client that waits as told is not refused on the rate again, now for a request of any cost.
			* 2026-10-18: the Calculator's command for the structure check of the equations of motion: version 1's five functions on the command line (the map of each degree of freedom to the law that determines it, the findings with their questions for the Declarer, the class, the test of the register's records and the settlement of its open gaps), each taking version 1's arguments and giving version 1's answer, and all 438 of version 1's test cases for them pass through it. No answer is owed. The command refuses a request too large to answer in good time: more than 64 entries in any of the Starting Set's DOF, CONSTANT, LAW and CONSTRAINT kinds, more than 64 records, status words or namings, or an equation's text of more than 16,384 characters. The search for a matching, which went back over columns it had already tried and took seconds on twenty unknowns, now tries each once, as version 1's did; every answer is unchanged.
			* 2026-10-18: the Calculator's command for the falcons: version 1's eleven falcon functions on the command line (the draw, the canonical forms, the QUOTE CHECK, the source match and its hops, the reconciliation, the output schema's canonical text and digest, the per-kind stop and the sponsor's stage), each taking version 1's arguments and answering with version 1's text, and all 949 of version 1's test cases for them pass through it, with the 259 written by hand; nothing is owed. The command refuses a request too large to answer in good time: strings of more than 200,000 characters in all; a QUOTE CHECK whose text sought, times the text it is sought in, passes 2,000,000 characters; a draw from more than 100 candidates; a reconciliation of more than 10 outputs or 1,000 rows, or whose lines would repeat a row's key past 1,000,000 characters; more than 10,000 events for the stage or records for the stop; more than 1,000 source entries. The slowest request it answers takes about a second.
			* 2026-10-18: the Calculator's command for identity, the sponsor and the prompt lint: version 1's functions of the three on the command line, each taking version 1's arguments and answering with version 1's text, and all of version 1's test cases for them pass through it, 102 for identity, 83 for the sponsor and 231 for the lint; nothing is owed. The command refuses a request too large to answer in good time: for the user evidence, more than 50 events, a number of more than 30 digits, or a shape of its Beta distribution below 1/10 or above 1,000; for the whitewash count, more than 4,000 admissions, retirements or states; and a lint whose findings would run past 1,048,576 characters, whose counts per code are still given. The bound on the size of an exact number is checked for the user evidence. Identity now sorts a tool list's members and a model map's names once, so that a large list or map takes a fraction of a second, not many seconds.
			* 2026-10-18: the Calculator's command for Provisions: version 1's eleven Provision functions on the command line, each taking version 1's arguments and answering with version 1's value, and all 418 of version 1's test cases for them pass through it. An answer is owed only where the checks before a Provision is declared meet, in the fundamental tests over a test binding, a value the Calculator's exact bounds cannot settle, such as a value exactly zero but not known so: the command refuses it with the word OWED, how such a value is answered being not yet chosen, and none of version 1's cases meets one. The command refuses a request too large to answer in good time: more than 8 texts, or 64 KiB of texts where it takes several; more than 256 declaring lines, 8 claims, 64 rounds of the interview's answer or 1,024 certificates; a Starting Set with more than 64 entries of a kind or 1,024 in all; a proposition of more than 256 characters, as written or once its slots are filled with the names bound to them; more than 64 placements of a term. Reading a Provision's text, which took up to two minutes for a long text of many short items, now takes a fraction of a second, every answer unchanged.
			* 2026-10-18: the Calculator's command for the register functions: version 1's 37 functions on the command line (the record check, its preimage, its digest and its views; grade and status; citations and the withdrawal; a record's measured fields and declared form; named gaps; verification; promotion and successors), each taking version 1's arguments and giving version 1's answer. All 1,145 of version 1's test cases for them run through it: 1,137 give version 1's answer, and the 8 that reach the verification's difference, its uncertainty and its zeta are answered as owed, saying that these wait on the numeric meaning's application to the verification; every check before them is answered. Every number these functions form from a request, a measurement brought to coherent SI or a budget's sums of squares, is checked against the bound on an exact number's size before it is formed and refused past it. The command refuses a request too large to answer in good time: a list of more than 1,024 entries, a text of more than 16,384 characters or more than 131,072 in all, a register of more than 64 records or whose records cite, assume and name more than 512 in all, or more than 64 open audits.
			* 2026-10-18: the Calculator's command for score and beta: version 1's 29 functions of the reliability score, the Beta layer and the user score's evidence on the command line, each taking version 1's arguments and answering with version 1's text, every number exact and rounded once to twelve digits, and all 586 of version 1's test cases for them pass through it, the Beta layer's two recorded departures from version 1 among them. Their numbers are held to the bound on the size of an exact number the Declarer chose, each answer proved to be the one computed without it: an event aged by more half-lives than the bound allows, or a product that would grow past it, is refused as too large, where it once took seconds or minutes. A number whose bounds do not settle its twelve digits is refused as owed. The command refuses a request too large to answer in good time: more than 30 events in all for the user score, sums of more than 64 powers of two for the evidence, more than 2,000 accounts for the ranking, and, for the Beta layer's quantile, shapes outside a tenth to 10,000 or tails within a millionth of 0 or 1.
	* 2026-10-18: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line: whether a quantity is compared by machine or listed for inspection, a record's conditions, the pairs of records the contradiction test compares, and the groups the scale factor is computed over. Each takes version 1's arguments and answers as version 1 did, its refusals included, and all 125 of version 1's test cases for them pass through the command line, so all five of version 1's test sets for the strike rule now run there. The conditions of a record with a point whose value in SI units carries a power of pi are refused as owed: their twelve digits need the digits of pi, which the Calculator does not compute for them yet. The command refuses a request too large to answer in good time: more than 2,000 records, or 5,000 assumptions and citations, for a record's conditions; more than 200 records, or 500 assumptions and citations, for the pairs and the groups; more than 1,000 points in all, a point's value or unit of more than 64 characters, and a point whose value in SI units holds more than 2,048 bits above or below its fraction line.		* 2026-10-18: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line: whether a quantity is compared by machine or listed for inspection, a record's conditions, the pairs of records the contradiction test compares, and the groups the scale factor is computed over. Each takes version 1's arguments and answers as version 1 did, its refusals included, and all 125 of version 1's test cases for them pass through the command line, so all five of version 1's test sets for the strike rule now run there. The conditions of a record with a point whose value in SI units carries a power of pi are refused as owed: their twelve digits need the digits of pi, which the Calculator does not compute for them yet. The command refuses a request too large to answer in good time: more than 2,000 records, or 5,000 assumptions and citations, for a record's conditions; more than 200 records, or 500 assumptions and citations, for the pairs and the groups; more than 1,000 points in all, a point's value or unit of more than 64 characters, and a point whose value in SI units holds more than 2,048 bits above or below its fraction line.
			* 2026-10-18: the Calculator's command for units and dimensions, in its final form: version 1's seven unit functions, each taking version 1's arguments and answering with version 1's lists in canonical JSON, every number exact. All 91 of version 1's unit test cases pass through it, 5 of them as the recorded differences, and so do the 26 hand-written cases of the seven functions. A unit's scale is now held in lowest terms, and the bound on the size of an exact number is built for the units: a scale, a value or a comparison that would cross it is refused as too large, a scale exactly when its numerator or denominator passes the bound, and Lean proves that every answer given is the one given before. The scale factor over measurements whose units carry different powers of pi, and a comparison across powers of pi that pi to 4096 bits does not decide, are refused as owed. The command refuses a unit of more than 1024 characters or 128 tokens, a decimal of more than 4096 characters, and more than 100 measurements, or one of more than 30 digits, for the scale factor, the strike rule's bounds.

	== Open ==		== Open ==
	* Units and dimensions: the Calculator's command for them takes its final form with canonical serialization. The scale factor over measurements whose units carry different powers of pi is refused until the strike rule takes them.
	* Identity: its call on the Calculator's command line waits on the canonical serialization of its arguments.
	* The prompt lint: it does not yet answer on the Calculator's command line.
	* Falcons: their call on the Calculator's command line follows.
	* Declared forms: the evaluation follows the standing choice of exact values; a choice of binary floating point would change it in one place.		* Declared forms: the evaluation follows the standing choice of exact values; a choice of binary floating point would change it in one place.
	* The governor: the pressure levels, then the traffic stages, each a later step of the admission function, in that order. Three of the Declarer's answers on admission are still to be built: the wait a request refused for want of a free slot is told; the cost of an operation the seat table does not price, and of one that costs more than an agent may spend at once; and what switching the governor off leaves in force.
	* Score, beta and sponsor: the Calculator's command for them follows. The bound on the size of an exact number the Declarer chose is still to be built; none of version 1's test cases comes near it.
	* The structured derivation checker: approximations beyond citing an ASSUMPTION record, and a call on the Calculator's command line that checks a record's derivation and credits it.		* The structured derivation checker: approximations beyond citing an ASSUMPTION record, and a call on the Calculator's command line that checks a record's derivation and credits it.
	* The specification pages: the converter that writes them from what the library gives, its checks, and the rewrite of the comments the pages carry, so that none names a file, an issue or a decision. What such a comment may still cite, and how a page is laid out, wait on the Declarer.		* The specification pages: the converter that writes them from what the library gives, its checks, and the rewrite of the comments the pages carry, so that none names a file, an issue or a decision. What such a comment may still cite, and how a page is laid out, wait on the Declarer.
	* The bound on the size of an exact number: built for the strike rule ~~and~~ the probes~~; the cluster~~, the units, the ~~declared forms~~, ~~score~~ and ~~sponsor~~, the ~~yardstick~~ and the ~~records~~ follow, in that order.		* The bound on the size of an exact number: built for the strike rule, the probes, the units, score, beta and the sponsor's user evidence, and the records; the cluster, the declared forms and the yardstick follow, in that order.
	* Provisions: their call on the Calculator's command line follows, answering what it cannot judge yet as owed.		* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification; the Calculator answers them as owed.
	* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning~~. The Calculator~~'s ~~command for~~ the ~~register functions follows, answering what it cannot yet settle~~ as owed.		* Units and dimensions: the scale factor over measurements whose units carry different powers of pi is refused as owed until the strike rule takes them.
	* The ~~Calculator's command for~~ the ~~structure check~~ of the ~~equations of motion~~.		* The governor: the pressure levels, then the traffic stages, each a later step of the admission function, in that order.

	== Next ==		== Next ==

Principia Machina/Progress/Status

PMA Progress — Sun, 18 Oct 2026 03:16:25 GMT

Progress pages rendered from the Principia Machina source

Principia Machina/Progress/Log

PMA Progress — Sun, 18 Oct 2026 03:16:24 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 03:16, 18 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated

Principia Machina/Progress/Phase 2

PMA Progress — Sun, 18 Oct 2026 03:16:23 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 03:16, 18 October 2026
Line 49:		Line 49:
	* 2026-10-17: the bound on the size of an exact number, as the Declarer chose: at most 65,536 bits above its fraction line and as many below, checked from the sizes of the numbers a step combines before the step is taken, and refused past it as too large. It is built for the strike rule's scale factor and its two mechanical tests and for the probes' comparison, which the Calculator's command line computes from a request's own numbers; each is proved, when it answers, to answer what it answered before. None of version 1's test cases comes near the bound. Measurements whose sizes differ by more than about a thousand powers of ten, which once took the scale factor seconds, are now refused in a fraction of one.		* 2026-10-17: the bound on the size of an exact number, as the Declarer chose: at most 65,536 bits above its fraction line and as many below, checked from the sizes of the numbers a step combines before the step is taken, and refused past it as too large. It is built for the strike rule's scale factor and its two mechanical tests and for the probes' comparison, which the Calculator's command line computes from a request's own numbers; each is proved, when it answers, to answer what it answered before. None of version 1's test cases comes near the bound. Measurements whose sizes differ by more than about a thousand powers of ten, which once took the scale factor seconds, are now refused in a fraction of one.
	* 2026-10-17: a Provision's kind read from its text, as the Declarer chose: one that writes no force term and binds no slot is a Convention, every other an Interaction. The first catalogue's four come out as recorded, and nothing a Provision's digest covers changes.		* 2026-10-17: a Provision's kind read from its text, as the Declarer chose: one that writes no force term and binds no slot is a Convention, every other an Interaction. The first catalogue's four come out as recorded, and nothing a Provision's digest covers changes.
			* 2026-10-18: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line: whether a quantity is compared by machine or listed for inspection, a record's conditions, the pairs of records the contradiction test compares, and the groups the scale factor is computed over. Each takes version 1's arguments and answers as version 1 did, its refusals included, and all 125 of version 1's test cases for them pass through the command line, so all five of version 1's test sets for the strike rule now run there. The conditions of a record with a point whose value in SI units carries a power of pi are refused as owed: their twelve digits need the digits of pi, which the Calculator does not compute for them yet. The command refuses a request too large to answer in good time: more than 2,000 records, or 5,000 assumptions and citations, for a record's conditions; more than 200 records, or 500 assumptions and citations, for the pairs and the groups; more than 1,000 points in all, a point's value or unit of more than 64 characters, and a point whose value in SI units holds more than 2,048 bits above or below its fraction line.

	== Open ==		== Open ==
	* The Calculator's commands for the strike rule and the structure check, which wait on the canonical serialization of their answers.
	* Units and dimensions: the Calculator's command for them takes its final form with canonical serialization. The scale factor over measurements whose units carry different powers of pi is refused until the strike rule takes them.		* Units and dimensions: the Calculator's command for them takes its final form with canonical serialization. The scale factor over measurements whose units carry different powers of pi is refused until the strike rule takes them.
	* Identity: its call on the Calculator's command line waits on the canonical serialization of its arguments.		* Identity: its call on the Calculator's command line waits on the canonical serialization of its arguments.
Line 64:		Line 64:
	* Provisions: their call on the Calculator's command line follows, answering what it cannot judge yet as owed.		* Provisions: their call on the Calculator's command line follows, answering what it cannot judge yet as owed.
	* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning. The Calculator's command for the register functions follows, answering what it cannot yet settle as owed.		* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning. The Calculator's command for the register functions follows, answering what it cannot yet settle as owed.
			* The Calculator's command for the structure check of the equations of motion.

	== Next ==		== Next ==

Principia Machina/Progress/Status

PMA Progress — Sun, 18 Oct 2026 01:13:38 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 8:		Line 8:

	<div class="pma-strip">		<div class="pma-strip">
	<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-17</div>		<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-18</div>
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">11 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">11 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>
Line 24:		Line 24:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-17 \|\| 18:13 PDT \|\| 2026-10-18 01:13
	\|-		\|-
	\| 2026-10-17 \|\| 16:59 PDT \|\| 2026-10-17 23:59		\| 2026-10-17 \|\| 16:59 PDT \|\| 2026-10-17 23:59
	\|-		\|-
	\| 2026-10-17 \|\| 16:01 PDT \|\| 2026-10-17 23:01		\| 2026-10-17 \|\| 16:01 PDT \|\| 2026-10-17 23:01
	\|-
	~~\| 2026-10-17 \|\| 15:41 PDT \|\| 2026-10-17 22:41~~
	\|}		\|}

Line 66:		Line 66:
	\| The three-letter code table approved \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-15		\| The three-letter code table approved \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Version 1's material copied into the source repository<span class="pma-note">: six specification texts and the full ~~sources~~ of version 1's ~~server extension and~~ research client wait on the Operator's copy</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 6 of 8 \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Version 1's material copied into the source repository<span class="pma-note">: six specification texts and the full source of version 1's research client wait on the Operator's copy</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 6 of 8 \|\| class="pma-wide" \| Operator \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| The declared parameters and tuning options, in Lean \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14		\| The declared parameters and tuning options, in Lean \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-10-18 \|\| class="pma-wide pma-date" \| 2026-10-14
Line 235:		Line 235:
	! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked		! Item !! class="pma-c-state" \| State !! class="pma-wide pma-c-owner" \| Owner !! class="pma-c-date" \| Checked
	\|-		\|-
	\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-17		\| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Declarer \|\| class="pma-date" \| 2026-10-18
	\|}		\|}
	</div>		</div>

	as of 2026-10-17		as of 2026-10-18

Principia Machina/Progress/Log

PMA Progress — Sun, 18 Oct 2026 01:13:37 GMT

Progress pages rendered from the Principia Machina source

Principia Machina/Progress/Phase 2

PMA Progress — Sun, 18 Oct 2026 01:13:36 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 69:		Line 69:
	The next function families in the order of the plan.		The next function families in the order of the plan.

	as of 2026-10-17		as of 2026-10-18

Principia Machina/Progress/Phase 1

PMA Progress — Sun, 18 Oct 2026 01:13:35 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 27:		Line 27:
	* 2026-10-15: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.		* 2026-10-15: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.
	* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.		* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.
			* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.

	== Open ==		== Open ==
	* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.
			* Version 1's specification texts at the versions the charter names: six of them still wait on the Operator's copy, as does the full source of version 1's research client.

	== Next ==		== Next ==
Line 37:		Line 38:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

	as of 2026-10-17		as of 2026-10-18

Principia Machina/Progress/Phase 0

PMA Progress — Sun, 18 Oct 2026 01:13:34 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 61:		Line 61:
	* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).		* 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: 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 ==		== Open ==
Line 70:		Line 71:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-17		as of 2026-10-18

Principia Machina/Progress/Status

PMA Progress — Sat, 17 Oct 2026 23:59:22 GMT

Progress pages rendered from the Principia Machina source

Principia Machina/Progress/Log

PMA Progress — Sat, 17 Oct 2026 23:59:21 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:59, 17 October 2026
Line 7:		Line 7:
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T2 on the wiki's host, under MediaWiki's shell framework from the command line		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T2 on the wiki's host, under MediaWiki's shell framework from the command line
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from the shell		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from the shell
			* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T5 on the wiki's host, under the wiki's command framework from the command line
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Declarer's choices on eight more questions about the Calculator, recorded in the charter		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Declarer's choices on eight more questions about the Calculator, recorded in the charter
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose

Principia Machina/Progress/Phase 1

PMA Progress — Sat, 17 Oct 2026 23:59:20 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:59, 17 October 2026
Line 26:		Line 26:
	* 2026-10-17: test T3 on the wiki's host, from the shell: 100 calls in one run took 7.432 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: PASS; its scheduled run follows.		* 2026-10-17: test T3 on the wiki's host, from the shell: 100 calls in one run took 7.432 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: PASS; its scheduled run follows.
	* 2026-10-15: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.		* 2026-10-15: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.
			* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.

	== Open ==		== Open ==
	* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.		* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* ~~Test T5 on the wiki's host, run by the Operator from the closing run; its kit is ready.~~ Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded~~. T5 checks a proof with a Lean kernel written independently of Lean's own~~.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.

	== Next ==		== Next ==

Principia Machina/Progress/Phase 0

PMA Progress — Sat, 17 Oct 2026 23:59:19 GMT

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:59, 17 October 2026
Line 64:		Line 64:
	== Open ==		== 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.		* 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.
	* Test T5, a kernel checker on the host: its kit is ready.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.		* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.

← Older revision		Revision as of 02:50, 21 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-21, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the wiki moved to the server the Operator controls
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks
Line 7:		Line 8:
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line
	* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees		* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees
			* 2026-10-21, [[Principia Machina/Progress/Phase 3\|Phase 3]]: the rehearsal wiki
	* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it		* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it
	* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it		* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it
Line 17:		Line 19:
	* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly		* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly
	* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk		* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk
			* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: tests T1, T2, T3 and T5 run again on a server the Operator controls, built from nothing by one provisioning script
	* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed		* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed
	* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source		* 2026-10-19, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source

← Older revision		Revision as of 02:45, 21 October 2026
Line 2:		Line 2:
	{{Principia Machina map}}		{{Principia Machina map}}
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the declared forms, as the Declarer chose (an input past the bound refused, an intermediate value that would cross it enclosed)
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bound on the size of an exact number, built for the yardsticks
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the bibliography's checks on the Calculator's command line
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: hold scope on the Calculator's command line
			* 2026-10-21, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the strike rule's conditions of a record now take a point whose value in SI units carries a power of pi, such as an angle given in degrees
			* 2026-10-20, [[Principia Machina/Progress/Phase 1\|Phase 1]]: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command line checks a structured derivation and credits it
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the fundamental tests on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the governor's admission on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: SHA-256 and Unicode's normalization on the Calculator's command line, so that an agent's own tools can be checked against the Calculator's
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the permissions function on the Calculator's command line, beside the command that reads words
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the zones on the Calculator's command line
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the converter that writes the specification pages from what the checked library gives, with its checks
			* 2026-10-20, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the verification's difference, its uncertainty and its zeta, computed exactly
	* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk		* 2026-10-19, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a check that reads a restricted list now runs only code from the trunk
	* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed		* 2026-10-19, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed
Line 7:		Line 21:
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended
			* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the runner's step that requires a check now names the service that posts it
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
Line 141:		Line 156:
	* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton		* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton

	as of 2026-10-19		as of 2026-10-21

← Older revision		Revision as of 02:28, 19 October 2026
Line 3:		Line 3:
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
	* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one		* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: machine 2's setup tells an installed runner from a running one
			* 2026-10-18, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a scheduled build session can now take queued tasks unattended
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run

← Older revision		Revision as of 01:23, 19 October 2026
Line 5:		Line 5:
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
			* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons

← Older revision		Revision as of 16:08, 18 October 2026
Line 3:		Line 3:
	'''Progress log''': one line per item done, newest first; each phase's page has the whole item.		'''Progress log''': one line per item done, newest first; each phase's page has the whole item.
	* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy		* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
			* 2026-10-18, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from one scheduled run
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the structure check of the equations of motion
	* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons		* 2026-10-18, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Calculator's command for the falcons

← Older revision		Revision as of 04:16, 18 October 2026
Line 11:		Line 11:
	<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>		<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">11 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">11 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div>
	<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">9 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>		<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">15 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div>
	<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>		<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div>
Line 24:		Line 24:
	{\| class="wikitable"		{\| class="wikitable"
	! updated Date: !! Pacific Time !! UTC		! updated Date: !! Pacific Time !! UTC
			\|-
			\| 2026-10-17 \|\| 21:16 PDT \|\| 2026-10-18 04:16
	\|-		\|-
	\| 2026-10-17 \|\| 20:16 PDT \|\| 2026-10-18 03:16		\| 2026-10-17 \|\| 20:16 PDT \|\| 2026-10-18 03:16
	\|-		\|-
	\| 2026-10-17 \|\| 18:13 PDT \|\| 2026-10-18 01:13		\| 2026-10-17 \|\| 18:13 PDT \|\| 2026-10-18 01:13
	\|-
	~~\| 2026-10-17 \|\| 16:59 PDT \|\| 2026-10-17 23:59~~
	\|}		\|}

Line 90:		Line 90:
	\| Digests and canonical serialization \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Digests and canonical serialization \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Units and dimensions~~<span class="pma-note">: 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</span>~~ \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 7 of 8~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Units and dimensions \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| The zones: Starting Set, Correspondence Table, Criteria Set \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| The zones: Starting Set, Correspondence Table, Criteria Set \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
Line 98:		Line 98:
	\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Fundamental tests and isomorphism checks \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Records and the register functions<span class="pma-note">: ~~the functions are ported, the record digests computed with SHA-256 as in version 1;~~ the verification's difference ~~waits~~ on the numeric meaning~~, and the Calculator~~'s ~~command follows~~</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Records and the register functions<span class="pma-note">: the verification's difference, its uncertainty and its zeta wait on the numeric meaning's application to the verification</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 3 of 4 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The strike rule, distance, SR8 and SR9 \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
Line 104:		Line 104:
	\| Hold scope \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Hold scope \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| The structure check of the equations of motion~~<span class="pma-note">: version 1's two test sets pass; its call on the Calculator's command line follows canonical serialization</span>~~ \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 2 of 3~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The structure check of the equations of motion \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Provisions<span class="pma-note">: the functions are ported, with the kinds Interaction and Convention, a Provision's kind read from its text, text read in NFC and the digests computed with SHA-256 as in version 1; the Calculator's command for them follows, answering what it cannot judge yet as owed</span> \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 2 of 3~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Provisions \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Probes and their comparison \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-17		\| Probes and their comparison \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-17
	\|-		\|-
	\| Score and beta<span class="pma-note">: 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</span> \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 2 of 3~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Score and beta \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Cluster \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Cluster \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Falcons~~<span class="pma-note">: the functions are ported, all 949 of version 1's test cases passing, text in NFC and the digests in SHA-256 as in version 1; the Calculator's command follows</span>~~ \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 3 of 4~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Falcons \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Bibliography \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15		\| Bibliography \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-15
	\|-		\|-
	\| Identity, sponsor and lint~~<span class="pma-note">: identity, sponsor and lint are ported, text in NFC and the prompt digest computed with SHA-256 as in version 1; the Calculator's command for them follows</span>~~ \|\| class="pma-lamp pma-lamp-~~lgreen~~" \| ~~PARTIAL 3 of 4~~ \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Identity, sponsor and lint \|\| class="pma-lamp pma-lamp-green" \| DONE \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission~~; five questions on admission wait on~~ the Declarer; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow</span> \|\| class="pma-lamp pma-lamp-lgreen" \| PARTIAL 2 of 3 \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18
	\|-		\|-
	\| The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18		\| The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> \|\| class="pma-lamp pma-lamp-amber" \| UNDER WAY \|\| class="pma-wide" \| Agent \|\| class="pma-date" \| 2026-11-26 \|\| class="pma-wide pma-date" \| 2026-10-18

← Older revision		Revision as of 01:13, 18 October 2026
Line 4:		Line 4:
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)
	* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated		* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the status panel says when it was last updated
			* 2026-10-17, [[Principia Machina/Progress/Phase 0\|Phase 0]]: 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
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the survey of Lean's toolchain set to run once a month, on the 22nd, as a scheduled task of its own		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: the survey of Lean's toolchain set to run once a month, on the 22nd, as a scheduled task of its own
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T2 on the wiki's host, under MediaWiki's shell framework from the command line		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T2 on the wiki's host, under MediaWiki's shell framework from the command line
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from the shell		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T3 on the wiki's host, from the shell
	* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T5 on the wiki's host, under the wiki's command framework from the command line		* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: test T5 on the wiki's host, under the wiki's command framework from the command line
			* 2026-10-17, [[Principia Machina/Progress/Phase 1\|Phase 1]]: version 1's named texts copied from the Operator's copy
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Declarer's choices on eight more questions about the Calculator, recorded in the charter		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the Declarer's choices on eight more questions about the Calculator, recorded in the charter
	* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose		* 2026-10-17, [[Principia Machina/Progress/Phase 2\|Phase 2]]: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose
Line 122:		Line 124:
	* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton		* 2026-10-10, [[Principia Machina/Progress/Phase 0\|Phase 0]]: the skeleton

	as of 2026-10-17		as of 2026-10-18