Principia Machina/Progress/Phase 2 - Revision history

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-21T02:45:56Z

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T02:29:51Z

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 ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T00:07:32Z

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T04:16:02Z

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 ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T03:16:23Z

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 ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T01:13:36Z

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T23:01:52Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:01, 17 October 2026
Line 45:		Line 45:
	* 2026-10-15: Unicode's normalization and general category, in Lean, as version 1 used them: the composed normal form (NFC) and the decomposed one (NFD), and each character's general category, at Unicode 15.1.0, as in version 1. Their tables are generated from Unicode's own data files by a script that checks them, and agree with version 1's on all 1,114,112 code points. All 19,074 lines of Unicode's normalization test for that version pass, 190,740 checks, and every character the test does not list is its own normal form. Lean proves that putting combining marks in their canonical order only moves them and leaves each run of marks in order, that ASCII text is its own normal form, and that every Hangul syllable composes back from its parts.		* 2026-10-15: Unicode's normalization and general category, in Lean, as version 1 used them: the composed normal form (NFC) and the decomposed one (NFD), and each character's general category, at Unicode 15.1.0, as in version 1. Their tables are generated from Unicode's own data files by a script that checks them, and agree with version 1's on all 1,114,112 code points. All 19,074 lines of Unicode's normalization test for that version pass, 190,740 checks, and every character the test does not list is its own normal form. Lean proves that putting combining marks in their canonical order only moves them and leaves each run of marks in order, that ASCII text is its own normal form, and that every Hangul syllable composes back from its parts.
	* 2026-10-17: the Declarer's choices on eight more questions about the Calculator, recorded in the charter: the specification pages read from the checked library by a program in Lean's core alone, one page for each source file, and published only with a release of the Calculator; an answer the Calculator does not yet compute refused with a word that says it is owed, never guessed; a structured derivation's step citing one law, assumption or identity at a stated place, each assumption it cites listed among the result's assumptions, a law cited only as written and never by an instance of it, and a derivative left as a quantity whose facts are cited as laws or assumptions; every exact number held to 65,536 bits above and below its fraction line, a larger one refused; a Provision's kind read from its text; and five rules of the governor's admission.		* 2026-10-17: the Declarer's choices on eight more questions about the Calculator, recorded in the charter: the specification pages read from the checked library by a program in Lean's core alone, one page for each source file, and published only with a release of the Calculator; an answer the Calculator does not yet compute refused with a word that says it is owed, never guessed; a structured derivation's step citing one law, assumption or identity at a stated place, each assumption it cites listed among the result's assumptions, a law cited only as written and never by an instance of it, and a derivative left as a quantity whose facts are cited as laws or assumptions; every exact number held to 65,536 bits above and below its fraction line, a larger one refused; a Provision's kind read from its text; and five rules of the governor's admission.
			* 2026-10-17: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose. For each of the library's 94 source files it lists, in order, every definition, theorem, structure and type written there, with its comment and its text; a theorem's text is its statement as Lean checked it, with the axioms it rests on, never its proof. It reads all 3,676 in about half a minute and gives the same document every time.
	* 2026-10-17: the Calculator's command for probes: version 1's ten probe functions on the command line, each taking version 1's arguments and answering with version 1's text, and all 252 of version 1's probe test cases pass through it. A request whose answer the Calculator does not compute yet is now refused with the word OWED, its detail saying what is owed, as the Declarer chose; no probe answer is owed. The command refuses a request too large to answer in good time: more than 400 records for LOAD, more than 4,000 revisions or 4,000 allocated identifiers for the historical view, and more than 100 standing records, or one of more than 30 digits, for a comparison, the strike rule's bounds on SR8.		* 2026-10-17: the Calculator's command for probes: version 1's ten probe functions on the command line, each taking version 1's arguments and answering with version 1's text, and all 252 of version 1's probe test cases pass through it. A request whose answer the Calculator does not compute yet is now refused with the word OWED, its detail saying what is owed, as the Declarer chose; no probe answer is owed. The command refuses a request too large to answer in good time: more than 400 records for LOAD, more than 4,000 revisions or 4,000 allocated identifiers for the historical view, and more than 100 standing records, or one of more than 30 digits, for a comparison, the strike rule's bounds on SR8.
			* 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.

Line 58:		Line 60:
	* 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.		* 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 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.
	* 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.

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T22:41:26Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 22:41, 17 October 2026
Line 45:		Line 45:
	* 2026-10-15: Unicode's normalization and general category, in Lean, as version 1 used them: the composed normal form (NFC) and the decomposed one (NFD), and each character's general category, at Unicode 15.1.0, as in version 1. Their tables are generated from Unicode's own data files by a script that checks them, and agree with version 1's on all 1,114,112 code points. All 19,074 lines of Unicode's normalization test for that version pass, 190,740 checks, and every character the test does not list is its own normal form. Lean proves that putting combining marks in their canonical order only moves them and leaves each run of marks in order, that ASCII text is its own normal form, and that every Hangul syllable composes back from its parts.		* 2026-10-15: Unicode's normalization and general category, in Lean, as version 1 used them: the composed normal form (NFC) and the decomposed one (NFD), and each character's general category, at Unicode 15.1.0, as in version 1. Their tables are generated from Unicode's own data files by a script that checks them, and agree with version 1's on all 1,114,112 code points. All 19,074 lines of Unicode's normalization test for that version pass, 190,740 checks, and every character the test does not list is its own normal form. Lean proves that putting combining marks in their canonical order only moves them and leaves each run of marks in order, that ASCII text is its own normal form, and that every Hangul syllable composes back from its parts.
	* 2026-10-17: the Declarer's choices on eight more questions about the Calculator, recorded in the charter: the specification pages read from the checked library by a program in Lean's core alone, one page for each source file, and published only with a release of the Calculator; an answer the Calculator does not yet compute refused with a word that says it is owed, never guessed; a structured derivation's step citing one law, assumption or identity at a stated place, each assumption it cites listed among the result's assumptions, a law cited only as written and never by an instance of it, and a derivative left as a quantity whose facts are cited as laws or assumptions; every exact number held to 65,536 bits above and below its fraction line, a larger one refused; a Provision's kind read from its text; and five rules of the governor's admission.		* 2026-10-17: the Declarer's choices on eight more questions about the Calculator, recorded in the charter: the specification pages read from the checked library by a program in Lean's core alone, one page for each source file, and published only with a release of the Calculator; an answer the Calculator does not yet compute refused with a word that says it is owed, never guessed; a structured derivation's step citing one law, assumption or identity at a stated place, each assumption it cites listed among the result's assumptions, a law cited only as written and never by an instance of it, and a derivative left as a quantity whose facts are cited as laws or assumptions; every exact number held to 65,536 bits above and below its fraction line, a larger one refused; a Provision's kind read from its text; and five rules of the governor's admission.
			* 2026-10-17: the Calculator's command for probes: version 1's ten probe functions on the command line, each taking version 1's arguments and answering with version 1's text, and all 252 of version 1's probe test cases pass through it. A request whose answer the Calculator does not compute yet is now refused with the word OWED, its detail saying what is owed, as the Declarer chose; no probe answer is owed. The command refuses a request too large to answer in good time: more than 400 records for LOAD, more than 4,000 revisions or 4,000 allocated identifiers for the historical view, and more than 100 standing records, or one of more than 30 digits, for a comparison, the strike rule's bounds on SR8.
			* 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.

	== Open ==		== Open ==
Line 51:		Line 53:
	* 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.
	* The prompt lint: it does not yet answer on the Calculator's command line.		* The prompt lint: it does not yet answer on the Calculator's command line.
	* Provisions: how a Provision declared after the first four gets its kind waits on the Declarer. Their call on the Calculator's command line waits on the Declarer's choice of how the Calculator answers a request it cannot judge yet.
	* Records: the verification's difference, its uncertainty and its zeta wait on the numeric meaning. The Calculator's command for the register functions waits on how it answers a request it cannot yet settle.
	* Falcons: their call on the Calculator's command line follows.		* Falcons: their call on the Calculator's command line follows.
	* Probes: the Calculator's command for probes 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.		* 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.		* 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.
			* 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.

	== Next ==		== Next ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T19:52:39Z

Progress pages rendered from the Principia Machina source

Show changes

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T00:04:41Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:04, 17 October 2026
Line 64:		Line 64:
	The next function families in the order of the plan.		The next function families in the order of the plan.

	as of 2026-10-16		as of 2026-10-17