Phase 2

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

Phase 2: the Calculator

Goal: version 1's calculator ported to Lean as the Calculator, one function family at a time, each with version 1's test cases and the properties Lean proves about it.

Done

2026-10-15: the cluster rule and its resolving step, which place the leading models in or out of the top group each month, ported with exact arithmetic in place of version 1's floating point. All 67 of version 1's test cases pass, with no difference from version 1's results. Proved: ranks 1 and 2 are always in, and down the ranking a model's class never goes back from CUSP to IN or from OUT to CUSP; the cases where a gap lies exactly on a threshold are settled exactly, as theorems.
2026-10-15: the strike rule, distance, SR8 and SR9 in Lean, all but the parts that read the zones. A record's distance from the Research Assembly, the two mechanical contradiction tests between measurements and derivations, the ordering of two contradicting records, the count of independent contradictions and the audit it opens, the scale factor of disagreeing measurements, and the compliance checks a ranking entry of the Criteria Set must pass. Every number is exact; version 1's 56 test cases for these functions pass, none needing a recorded divergence. Lean proves that the contradiction test is symmetric in its two measurements, that the scale factor never creates a contradiction, that distance is a total order, and that the strike skeleton never ranks a record failing SR1 above one passing it and never lets a measurement strike a derivation, on every suite.
2026-10-15: the canonical serialization, ported: version 1's text of a result and its canonical JSON, written by hand in Lean with exact numbers and no floating point. All 17 of version 1's test cases for it pass, 15 as version 1 wrote them and 2 as recorded differences: version 1 first rounded a number to the nearest binary floating-point value, where the Calculator keeps its exact value. Lean proves that an object's text does not depend on the order its members were given in, that two strings are never written alike, that no control character is written raw, and that a number's text depends on its value, not its spelling. A number read from text is held to stated bounds on its digits and its exponent, and one that version 1 would have read as infinite is refused. The inputs of the digests are ported too, and match version 1's on all 8 of its digest test cases.
2026-10-15: units and dimensions, in Lean: the unit grammar with its closed catalogue of symbols and prefixes, the canonical form of a dimension and of a decimal, and four of version 1's seven unit functions, run against version 1's 79 test cases for them and its 69 test cases for dimensions and decimals. Every number is exact, with no floating point; version 1's refusal of a number that floating point cannot hold is kept, decided on the exact number, and the 5 cases where version 1's floating-point results differ from the exact ones are recorded with their cause. Lean proves that a dimension is canonical exactly when normalizing it leaves it unchanged, and that every one of the 807 unit tokens is spelled one way only.
2026-10-15: units and dimensions: the three unit functions that compare measurements through the strike rule, run against version 1's 12 test cases for them, so all 91 of its unit test cases now run. A measurement in degrees is compared with one in radians exactly: the comparison is decided with pi bounded to as many as 4096 bits, and the bounds are checked against 1400 reference digits of pi.
2026-10-15: the Calculator's command line, built: one call names a function family and a function, reads one JSON value and writes one answer in canonical JSON, or a refusal that says why. The request is read by a reader written by hand that refuses, each with a reason of its own and the place it was found, any text outside the JSON standard, a key given twice, and a text past its stated bounds on size, nesting and numbers. Lean proves that every string reads back from its canonical JSON unchanged. The canonical serialization, the digests' inputs and the record table answer on it now; each other function family adds one line.
2026-10-15: the cluster rule, the strike rule and SR9 answer on the Calculator's command line. Each takes its request in version 1's argument names and answers as version 1 did; all 67 of version 1's cluster test cases, its 25 strike and scale-factor cases and its 31 SR9 cases pass through the command line as well. Where a function's cost grows faster than its input, it states the most it takes, measured, so that no request accepted runs long.
2026-10-15: the three zones' checks, in Lean: the Starting Set, the Correspondence Table and the Criteria Set with its yardstick terms. 100 of version 1's test cases for them pass. 125 wait, and the Calculator refuses to judge them in the meantime: 90 on the declared forms, which come next, 33 on the zones' digests and 2 on Unicode's tables. Lean proves that a zone the Calculator cannot yet judge is never passed, and that a malformed yardstick term is never altered into a well-formed one.
2026-10-15: the structured derivation checker's first increment, in Lean. A derivation starts from a law of the Starting Set or an ASSUMPTION record, or from an expression equal to itself, and each step rewrites one part of the current equation, either by a cited law or record, matched exactly, or by one of a fixed list of identities: the order and grouping of sums and products, multiplying out, adding zero, multiplying by one and double negation. The checker accepts a derivation only when every step gives exactly the equation it states and the last is the result's equation; otherwise it names the first failing step and why. Lean proves the checker sound: when it accepts, the result holds for every value of the variables and every meaning of the functions and derivatives under which the cited laws hold, with division by zero included. 24 hand-written derivations, 11 to accept and 13 to refuse, all come out as written.
2026-10-15: the bibliography, in Lean: the checks of the six kinds of identifier (DOI, arXiv, ISBN, ISSN, PubMed and PubMed Central), the key form that compares titles and names, the write check of an entry and its canonical form, the lookup address at a registry and the comparison with what the registry holds, the literature view and the hold list. 381 of version 1's 405 test cases for it pass. 24 wait on the Declarer's choices: 8 on how the Calculator computes SHA-256, whose canonical text agrees with version 1's, and 16 on Unicode's tables for text beyond what the Calculator carries. Version 1's own table of character classes is carried as version 1 wrote it and checked against version 1's text. Lean proves that the text rule and the key form never answer for text the Calculator cannot yet normalize, and that a comparison's result is always one of version 1's six.
2026-10-15: the fundamental tests T2, T3 and T5, the isomorphism checks IC1 to IC4 and the final pass over the three zones, in Lean. 93 of version 1's 120 test cases for them pass; 27 wait, and the Calculator refuses to judge them in the meantime: 25 on the declared forms and 2 on Unicode's tables. Two values fixed for one quantity are compared exactly through version 1's twelve-digit form, also where a unit carries pi, as a degree does. Lean proves that a failure of T1 stops the run, and that the isomorphism checks pass only with no problem and no gap.
2026-10-15: the strike rule's parts that read the zones and the register's records, in Lean: whether a quantity is compared by machine or listed for inspection, a record's conditions (the situations its assumptions set and the points it was measured at, in SI units), the pairs of records the contradiction test compares, and the groups the scale factor is computed over. All 125 of version 1's test cases for them pass, none needing a recorded divergence. Lean proves that two derivations are never paired for a measurement's contradiction test, on any register.
2026-10-15: the structure check of the equations of motion, in Lean: which unknown each law determines, the parts of the system that are under- or over-determined, the index and the initial values of the square part, the findings with their questions for the Declarer, and what the register's records settle, each law's equation read by the declared forms. All 438 of version 1's test cases for it pass, none needing a recorded divergence. Lean proves that a container whose structure check is switched off is never validated, whatever its laws.
2026-10-15: hold scope, in Lean: the blocks held after an account fails a canary, the records held with them in a register, the identifiers Custos draws for the records it writes, and the hold and release records. 90 of version 1's 140 test cases for it pass. 50 wait on the choice of how the Calculator computes SHA-256, since each ends with or checks a digest; everything else they check agrees with version 1. Lean proves that the held records form a closure: the seeds are held, a record citing or assuming a held record is held, and closing again changes nothing.
2026-10-15: the yardsticks a Criteria Set declares, in Lean: a declared ranking of records, evaluated exactly and run through the compliance checks of SR9 on the synthetic records. Version 1's 46 test cases pass, none needing a recorded divergence and none waiting on Unicode's tables. Lean proves, for every yardstick the Calculator accepts, that it never ranks a record failing SR1 above one passing it and never lets a measurement strike a derivation; and that the check the Criteria Set's grammar makes at entry settles the third check, that adding an assumption never improves a record's rank, wherever the count of a record's assumptions does not fall when one is added.
2026-10-15: the third check of SR9 proved with no condition left. Lean proves that adding an assumption to a record never lowers the count of its assumptions, and that the check the Criteria Set's grammar makes at entry, which reads each weight's sign from its written value, agrees with the yardstick's exact values. So every yardstick the Calculator accepts with no limiting cases never ranks a record higher when an assumption is added, on every suite. Version 1's test cases for the strike rule (56) and the yardsticks (46) still all pass.
2026-10-15: the permissions function, version 1's table of who may read, change or protect each kind of page, now one Lean function that the wiki's gatekeeper will ask. The charter's four rules are proved about it: only the Declarer appends to the declarations, no agent changes a page that carries a declaration, the restricted pages are read only by the Declarer, the Operator and, where its setting allows, the user account a page names, and in a closed research container an agent writes only from the container's access list. Every cell of the table has its test case. Where version 1 is silent or contradicts itself, eight questions are put to the Declarer, and until he answers the function refuses there.
2026-10-15: the cluster rule's tests compare each result with version 1's expected text field by field, as values of their own kind, rather than as one printed line in which two different results could print alike. All 67 cases still pass, and a swapped or changed field is shown to fail.
2026-10-15: the declared forms, in Lean: the closed grammar of a law's equation, a boundary's condition and a signature's form, its one canonical spelling and its parse tree, with version 1's bounds on length, nesting and exponents; the dimension and totality checks, the names and D-variable rules, fundamental tests T3, T4 and T6 over the forms and the syntactic image check. 552 of version 1's 555 test cases pass, 1 of them a recorded difference: the cosine of 90 degrees is exactly 0, where version 1's floating point gave 6.1e-17. Values are exact where they can be, and otherwise held between bounds that are rounded outward, so that every answer is the exact number's. Lean proves version 1's 33 grammar witnesses, that each canonical spelling reads back to itself, and that the bounds enclose every sum, difference, product and quotient.
2026-10-15: SHA-256 read wherever the zones, the hold, the bibliography, identity, the records and Provisions compute a digest, in place of the answers that waited on it. The zones' canonical serialization is ported whole: each zone's preimage and digest, the Research Assembly's digest and the successor classes, one port that Provisions and the record check read as well. All 360 of version 1's test cases in these families that waited on SHA-256 are computed, with the 41 cases of the zones' serialization not run before, and every one agrees with version 1; none needs a recorded divergence. The prompt lint's tables are checked against the SHA-256 version 1 records for them. Lean proves that every zone digest is the SHA-256 of its preimage, that a Research Assembly is IDENTICAL to itself, that a HOLD and a RELEASE end with the digest of their fields and that a RELEASE is written only for a HOLD whose digest matches its fields, that a PROMPT digest is the SHA-256 of its fields, and that a WITHDRAWAL and a PROMOTION end with their digests.
2026-10-15: SHA-256 in the falcons and the probes: a falcon kind's output schema digest, the order of a falcon's draw between accounts equal on window and share, and every draw of the probes (the parrot ratio's epochs, the canary schedule's bursts and gaps, the probe draw) are computed with the Calculator's SHA-256, each drawn value compared exactly. All 37 of version 1's falcon test cases and all 83 of its probe test cases that waited on SHA-256 agree with version 1, so all 949 falcon and all 252 probe test cases pass and none waits; 19 further falcon cases, chosen by hand and each answered by version 1's own code, check the draw's order between equal accounts and the schema digests, and the falcons' table of character classes now passes the SHA-256 check version 1 made on it. No case diverges: on every one the exact comparison falls as version 1's floating point did, a drawn value never closer than about one hundredth to what it is compared with, and no number comes near a bound on its size. Lean proves that a drawn value lies between 0 and 1, never reaching 1; that a drawn count lies in its range, which version 1's guard against rounding never needs to enforce; that a drawn ratio is one of the declared ratios and a burst rate is drawn from a position within the declared list; that the test of whether a block is probed compares whole numbers; that the falcon draw's order leaves no two accounts unordered; and that every schema digest is 64 characters.
2026-10-15: the falcons in Lean: the canonical forms in which agents' answers are compared (text, decimal, value with unit, date, web address, enumeration, yes or no); the quote check, which finds a value in a quoted text only as a whole number or word; the match of a cited web address against a falcon's declared sources, and of each redirect; the reconciliation of two or three agents' answers; the draw of a falcon's agents; a sponsor's stage; the stop of a falcon kind; and the canonical text of a kind's output schema. 820 of version 1's 949 test cases for them pass. 129 wait, and the Calculator refuses to judge them in the meantime: 33 on SHA-256 and 96 on Unicode's tables. 240 further cases, chosen by hand and each answered by version 1's own code, pass. Version 1's table of character classes is carried as version 1 wrote it and checked against version 1's text. Lean proves that the written text of a canonical form never stands for two forms, and that no text is answered whose normalization needs Unicode's tables.
2026-10-15: the declared forms read in the zones' checks and in the fundamental tests: an equation, a condition or a signature's form is parsed, named against what it cites, and checked for its dimensions, its guards and its values. The 115 of version 1's test cases that waited on the forms pass: 90 of the zones' and 25 of the fundamental tests'. What still waits: the zones' digests, and 4 cases on Unicode's tables.
2026-10-15: the governor's admission, in Lean: the function that decides whether a request to the wiki is let in, by its lane, the seats its operation costs against what an agent and its sponsor may spend in an hour, the requests already in flight and the Operator's stop switch. A request refused for going too fast is told when to come back, with a small random delay added, and Lean proves that a client coming back then is not refused for that reason again. Lean also proves that the requests of the Declarer, the Operator and the people signed in, and an agent's work already under way, are never refused on budget, and that more free capacity never turns an admission into a refusal. Version 1 described the governor but never built it; its rules are checked here against 509 requests whose answers a separate program computed from the same rules. The pressure levels and the traffic stages follow as later steps of the same function.
2026-10-15: identity in Lean: the canonical form of the tool definitions an agent is offered, the inputs of a prompt's digest, the model map's lookup and the vendor family key, a reported model's change class, and the comparison of the four vendor values. 82 of version 1's 102 test cases for them pass. 20 wait, and the Calculator refuses to judge them in the meantime: 11 on SHA-256, whose inputs match version 1's wherever the Calculator computes them, and 9 on Unicode's tables. Lean proves that a change of family is never recorded as a change of model, that a closed and an open family key never coincide, and that a comparison differs exactly when one of its pairs does.
2026-10-15: the prompt lint, in Lean: the advisory findings on a Sponsor's zone and on the tools an agent is offered, each a code, an entry of version 1's tables and a place, never an excerpt of the text: hidden characters, credential shapes, a source of authorization other than the human, relaxing the rules or spotting probes, a second copy of the specification, tool text addressed to the model, open-ended tools, a zone over its cap and instructions to persist; and their counts. 218 of version 1's 231 test cases for it pass. 13 wait on Unicode's tables, and the Calculator refuses to judge them in the meantime. Version 1's own tables are carried as version 1 wrote them and checked against version 1's text. Lean proves that the findings are unique and in version 1's order, that an input that cannot be linted has exactly one finding, that the lint always answers unless a character beyond its interim table makes it wait, and that a key is shown by name only when version 1's table of names holds it.
2026-10-15: probes and their comparison, all but the draws: the comparison of a reproduction with its target, LOAD and expected loss, the end of a reset by the account's state, the historical view of the register, and every check version 1 makes before a draw. 168 of version 1's 252 test cases are computed, all agreeing; an equation found by a reproduction is read in the declared forms' spelling. The other 84 wait on the Declarer's choices, each listed with its reason and checked: 83 on how the Calculator computes SHA-256, which the draws use, and 1 on Unicode's tables, for text beyond the characters the Calculator knows. Proved: a passed parrot never ends a reset, under SUSPENDED no canary pass ends one, only a non-corroboration starts one, the expected loss lies between 0 and the load, an equation is accepted only in the declared forms' spelling, and text the Calculator cannot yet normalize is never accepted.
2026-10-15: Provisions, in Lean: the reading and checks of a Provision's text and its canonical form for the digest; its binding to a draft's Starting Set and the expansion that writes its constants, assumptions and boundaries and adds its terms to the equations of motion the structure check names; the check that a draft carries its own expansion; the interview's check and the lines the check page lists as not included; the catalogue the Declarer's acts build; the checks before a Provision is declared; a draft's statuses and the use view. The kinds the Declarer chose are recorded: GRAV-UNIFORM, AIR-QUADRATIC and AIR-LINEAR are Interactions, MATH is a Convention. 226 of version 1's 418 test cases for them pass as the Calculator answers today. 192 wait, and the Calculator refuses to judge them in the meantime: 190 on SHA-256 and 2 on Unicode's tables; given version 1's SHA-256 values for the very inputs the Calculator computes, all 190 come out as version 1's. Lean proves that no two versions of one Provision are offered at once, that a withdrawn version stays withdrawn, and that the order in which Provisions are chosen changes nothing in the expansion.
2026-10-15: the records and the register functions, in Lean: version 1's record table, carried as version 1 wrote it and checked against the record types, and the functions that read it: the record check at a push and at landing, the record's canonical field list, the views other functions read a record through, the grade and the status a record holds now and the events that move them, the check of what a new record cites, the records a withdrawal reaches and its record, a measured result's uncertainty budget, the pair a parrot comparison reads, the declared form on a record, named gaps, the verification's checks, and the promotion of results. 1,065 of version 1's 1,145 test cases for them pass, none needing a recorded divergence. 80 wait on the Declarer's choices: 66 on how the Calculator computes SHA-256, since each writes or compares a digest, 6 on Unicode's tables, and 8 on the numeric meaning, since version 1 computed the verification's difference with a square root in floating point; what they check without it agrees with version 1. Lean proves that a grade only moves away from standing, that an inherited record never lands ESTABLISHED, that a hold never clears a strike, and that a withdrawal never reaches its own record.
2026-10-15: the reliability score and its Beta layer, in Lean: the evidence an account's resolved events give, weighted by their age in half-lives, capped by the diversity quota and widened when the account is idle, with its mean and its 95 per cent interval; the standing of two accounts, the ranking and the trust tier, the choice of the Prime, the state an account's pending items put it in and how it leaves it, the score's update, the cuts, the trip, the inquiry's cost, the override and the pad, the gate on releasing a held record, the inheritance, and the user score's pooling of its agents' events. Every number is the exact value: the mean exactly, and the gamma function, the incomplete beta function and the interval's ends between bounds narrowed until their twelve digits are settled. All 99 of version 1's test cases for the Beta layer pass, 2 of them as recorded differences where version 1's floating point moved a digit (the logarithm of the gamma function at 1 is exactly 0, where version 1 printed -8.9e-16); 471 of its 487 for the score pass with no difference, and 16 wait on the sponsor's functions, which come next. Lean proves that the mean lies between 0 and 1, rises with the evidence for and falls with the evidence against; that the quota never admits more than a match's weight; that a score never leaves its bounds nor moves by more than the step allowed; that a cut or an inquiry never raises a score; and that CLEARLY HIGHER and CLEARLY LOWER mirror each other.
2026-10-15: SHA-256, written in Lean as part of the Calculator, as the standard FIPS 180-4 defines it, with no library and no code from outside: the Declarer's choice for every digest. It passes all 129 of the test messages NIST publishes for it, from the empty message to 6400 bytes, and the standard's three examples, one million letters "a" among them, each checked beforehand with an independent implementation; together they take about a tenth of a second. Lean proves that its 64 constants and its starting value are the ones the standard derives from the cube and square roots of the first primes, that the padded message is a whole number of blocks that begins with the message and ends with its length, and that every digest is 32 bytes; the Lean kernel computes the standard's first example itself. The digests of version 1's digest functions now answer on the Calculator's command line, and all 8 of its digest test cases pass, each digest compared.
2026-10-15: the digests of the specification and of the instruction set, in Lean: version 1's functions that read the preformatted blocks of the specification's pages, list the pages kept with the digest of each, and compute the specification's digest over that list and the instruction set's digest over the specification's version, its digest and the other members of the instruction set. All 189 of version 1's test cases for them pass, directly and on the Calculator's command line, and none needs a recorded divergence. Lean proves that a digest's input never stands for two different inputs: the encoding of a list of texts, of a list of fields of fixed kinds, of a list of digests and of a zone's tree. It proves too that the specification's digest is the digest of its list of pages, that no text outside the blocks and no order of the pages changes it, and that the input of each of the two digests gives back the version, the pages and the members it was computed from.
2026-10-15: the sponsor's functions, in Lean: how each of a sponsor's conduct events resolves, for, against, neutral or pending, from the facts counted or the audit's finding; the user's evidence, from the sponsor's agents' events and its own conduct events, each weighted by its age in half-lives, with its mean and its 95 per cent interval; and the count of new agents admitted close to the exit of another agent of the sponsor that left in trouble (a whitewash). Every number is the exact value, the interval's ends between bounds narrowed until their twelve digits are settled. All 83 of version 1's test cases for them pass with no difference, and with them the 16 of the score's that waited on the sponsor's functions: all 487 of the score's test cases now pass. Lean proves that a conduct event of a kind for the sponsor never counts against it and one of a kind against it never counts for it; that a whitewash is never left pending and is judged alike whether the new agent came before or after the exit; that a succession or a declared change counts for the sponsor only after 100 blocks; that a neutral event adds nothing and is not counted; and that every whitewash counted is another agent's exit, one the whitewash rule counts against the sponsor.
2026-10-15: SR6's independence count now runs version 1's branch and bound, which stops a search as soon as it cannot beat the best count found, in place of trying every group of contradictions. It compares each assumption by a number standing for it, so a long name costs no more than a short one. Lean proves that the count is the same as the exhaustive search's on every input. 24 contradictions of 8 assumptions each, which took 46 s, now take under a millisecond, and the Calculator accepts 128 assumptions in all across SR6's contradictions, where it accepted 32: the slowest request found at that size takes a third of a second. Version 1's 56 test cases for the strike rule still pass.
2026-10-15: the structured derivation checker joined to the credit a result's derivation earns. A record's structured steps now say where each one rewrites and in which direction, a step may rest on one of the checker's identities instead of a law, and a derivation may start from a cited law, a cited ASSUMPTION record or an expression of its own. The Calculator gathers the laws a record may cite from the Starting Set's laws and the ASSUMPTION records the record names, and from nothing else, reads the steps and checks them against those laws. Lean proves that a derivation is credited as mechanically checked only when the checker accepted it, and that its result's equation then follows from the Starting Set's laws and the record's assumptions. The steps have one written form, which Lean proves reads back unchanged. 30 hand-written records, 5 sets of laws and 28 written forms, accepted, refused and unreadable, all come out as written.
2026-10-15: the structured derivation checker matches a law to an instance of it. A step may now rewrite by an instance of a cited equation, its symbols replaced by expressions: the checker finds the replacement by matching one side of the equation against the part rewritten, and accepts the step only when the instance gives exactly the equation the step states. Lean proves that what matching finds is an instance, that it finds one whenever there is one, and that the checker stays sound: an equation cited by an instance must hold for every value of its symbols, while one cited exactly need hold only for the values at hand. A record's derivation still cites the Starting Set's laws and its ASSUMPTION records exactly: they state facts about one system, not identities, and an instance of one need not hold where it does. Which laws may be matched so is put to the Declarer. The calculus of derivatives is not added: a form writes a derivative only of a named quantity, never of an expression, and what a derivative means in the checker is the Declarer's to choose. 14 more hand-written derivations, 6 to accept and 8 to refuse, and 25 matches all come out as written.
2026-10-15: Unicode's tables read wherever the Calculator reads text, in place of the interim tables: text is put in its composed normal form (NFC), and a character judged by its general category, at Unicode 15.1.0, as version 1 did, in the zones, the declared forms, the fundamental tests, the bibliography, identity, the hold, the yardsticks, the strike rule's conditions, the structure check, the records, Provisions, probes, the falcons, the prompt lint and the units' refusals. All 150 of version 1's test cases that waited on Unicode's tables are computed, and every one agrees with version 1; six of them reach a digest next and wait on SHA-256 instead. No test case of version 1 waits on Unicode's tables any more. Lean proves that a character is refused exactly when version 1's rule refuses it, that the text the Calculator reads is the NFC of the text given, that two forms with one NFC read alike, that no zone is left unjudged for its text, and that the prompt lint always answers.
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 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 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: 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 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

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 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, 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.
The governor: the pressure levels, then the traffic stages, each a later step of the admission function, in that order.

Done

Open

Next