Epistemics

This document defines the four classifications attached to whole results in this repository, the kind each result carries, and the policy for results by others: their scope, credit and import. conventions.md owns field formats and identifiers; packing/frontier/evidence.yaml holds the evidence entries; and the results register holds each classified claim in results.yaml, with a generated reader view in RESULTS.md.

The results checker validates structural support for a declared classification. Human review remains responsible for deciding whether the cited evidence is relevant and complete for the stated claim.

The Four Classifications

Use V4/C3 when describing a whole result. The unqualified term verified remains the formal assurance label for an individual evidence entry.

The two ladders carry the same rung meanings and differ in who earns each rung. V is self-certification or historic certification: it asks what kind of verification exists and how it was examined, and does not require this project to have replayed anything. C is confirmation: the same rungs, earned by a party other than the producing run. For a result of this project that is a later replay from the repository, a second implementation, another project’s replay or an external reviewer; for a result by others it is this project, or another third party whose replay is retained here. Every confirmation beyond a read is also verification evidence, so C never exceeds V from C2 up.

No Blind Trust

No rung rests on blind trust in a formal system or in an agent. Every rung from 4 up names the human who examined the work and states what they examined, in a record retained in this repository and specific enough to audit. A kernel check, a passing certificate replay and an AI review are evidence; a human reading them is what turns evidence into a rung. Rung 4 needs a human’s oversight of the mechanization and of the AI checking; rung 5 needs human experts’ review of the formalization itself. Review Records says what each record holds.

Verification

The rungs are ordered by the kind of verification and how it was examined; they are not cumulative. V3 does not imply publication, and V5 means that a proof assistant checked a formalization and a human expert attested that the formal statement says what the claim says.

The Short column is the form the site’s rubric cards print where a row has two lines; the Meaning is the chip’s title and the rubric’s own words.

The checker derives V1 and V3–V5 from the evidence cited by the result, of any origin, and from the result’s retained reviews. V0 and V2 are declared because the current evidence fields do not distinguish an ordinary unsupported claim from an asserted but unavailable proof; both require an explanatory notes field. The evidence schema separately enforces its own provenance, limitations, and method-specific fields.

Reported Formal Proofs and Source Builds

A readable formalization and a credible announcement are not a successful proof run. Inspect the theorem’s definitions, scope and mathematical premises, the complete build record and its source/toolchain pins, and the theorem’s axiom receipt separately. A build of the statement or construction proves only that component; samples of finite certificate checks do not establish the complete theorem.

An inspected, retained record of a complete producer build can earn V3 without a replay here. Keep the original report as assurance: reported and add a source-build entry with assurance: verified, method: proof-assistant-checked, origin: external and performed_by: source-author. Its replay_status: passed describes that producer execution. It requires a retained build_receipt, axioms_receipt, explicit full coverage, a scoped proof with an audit_record, and a qualifying dated external_review explaining what was inspected. The audit must assess the public proof’s recoverability, build pins, execution completeness, statement fidelity and trust boundary. Conflicting or incomplete source execution records stay reported. A third party’s build retained here is held to the same record, with its own receipts: a confirming claim never needs less retained evidence than the producer’s. A build or axiom receipt records one execution, so entries naming different actors never cite the same receipt. The execution actor and origin must agree, for every method: the producer’s run is external, a retained third-party run is independently-external, and a run here names the repository. A proof-assistant build here is replayed-here; reading someone else’s build receipt is a read on their entry, never audited-here. An origin label alone cannot supply confirmation.

A conditional proof verifies its implication even while a premise remains open. Its unconditional conclusion takes the weakest support along every cited premise chain, separately for V and C. Each premise needs a complete, scope-covering machine execution, exact, interval-certified or proof-assistant; samples, missing references and circular discharge supply no whole-claim rung. A published or audited proof of a premise is read, not run, and discharges nothing, even with a passing status: until a premise is executed, its theorem stands as the implication. A producer’s formal build, once admitted under the rule above, can discharge a premise for V without discharging C; a producer’s exact or interval run has no such admission and discharges nothing. Reading the conditional claim can still support C1.

This credits the source’s verification and does not independently authenticate its execution. C remains C0 or C1 until a complete confirming run exists. The source-build entry can support V4 or V5 when the corresponding retained human and adversarial review records qualify; neither high V nor the word formal raises C. The same project’s internal team may provide those records subject to the rubric’s independence-from-author requirements. An AI team’s inspection alone supplies neither human oversight nor human expert review.

State the actual trust boundary. Lean’s standard axioms with native_decide can support formal verification, but it trusts the compiler and native execution as well as the kernel. An axiom receipt is evidence to examine, not a guarantee that the formal statement matches the intended mathematical claim or that all premises were discharged.

The rule was first applied in the admission audit of 15 October 2026.

Confirmation

Confirmation counts only work performed beyond the producing run: evidence recorded as audited-here, replayed-here or independently-external (a third party’s own replay, retained here), and reviews performed on the confirming side; C1 describes a qualifying read of external evidence.

For C1, a qualifying review state is informally-verified or defect-found; the review note records what was examined and what remains unchecked. A C3 or higher result must also name at least one existing control path. The evidence schema requires a limitations statement on every evidence entry.

These predicates are deliberately literal. A recorded execution performed here, with its receipt retained and hash-bound, is a replay at C3 and C4 even when the final composer reconciles receipts rather than rerunning geometry; a fresh end-to-end replay from the repository is what C5’s “replayed here” requires. Two independently written implementations using the same method, or two different methods, do not change the rung: the count of distinct machine methods among the confirming entries, and a third party’s retained replay, are attributes the register shows beside the rung, not rungs. A control path proves that a control is retained; the checker does not infer from its filename that the control is adversarial. The test suite, validation configuration, and review establish those stronger facts.

Which Code Confirmed It

A confirmation either reproduces a result with the code its producer used or decides it again with other code, and the record says which. Every evidence entry whose method runs code, or that names a replay, lists its programs in verifiers, by their ids in verifiers.yaml. Each program there is external, written outside this repository by a result’s producer or another party, or first-party, written here; it decides the entry’s claim or checks premises (inputs, digests, receipts, a sample) and leaves the decision to another program; and it carries the digests or revisions that ran and the retained path of its source. The entry’s relationship_to_generator says how the deciding programs stand to the code the result’s producer used:

A premise check rides with an entry and never sets its relation: an independent exact preflight run before the source’s own checker leaves the replay same-implementation, with the preflight listed among its programs. A new independent-implementation entry names the record of what its authors read and used, its own independence_record or a deciding program’s in the registry; a clean-room record, one that says the authors never read the producer’s code, is the strongest. The 30 such entries recorded before 2 October 2026 without one are exempt by name in devtools/verifier_registry.py, a list that only shrinks. Since 14 October 2026 the record is also structured (The Independence Record), and the ladder says what each degree of independence can and cannot rule out.

How a result was confirmed is the third attribute beside its rung, and the register prints it as the mark after the status: confirmed, reproduced with the producer’s code. Each part of the claim takes the relation furthest from the producer’s code among the confirming runs that decide it, and the result takes the part closest to it, so an exact value is as independent as the less independent of its two halves: the grid’s replay never makes a lower half re-run with the source’s own checker read as re-implemented. VERIFIERS.md lists every program and what it backs; RESULTS.md and each case record’s Verification Code section list the programs behind each result and each verified bound.

The word confirmed says which kind. In a register claim, a case record, a review or a reply on an issue, confirmed is followed by which confirmation it was: reproduced with the producer’s code, re-implemented sharing named components, or independently re-implemented. The checker refuses a sentence of a register claim, composition or next_rung that says confirmed without one of those phrases; case records, reviews and replies are held to it in review (the result-import process, stage 4), because their prose also uses the word for things that are not results.

The Independence Record

The owner, on 14 October 2026: “I’d like to make sure the validation we do that’s independent is documented, and the degree to which it’s independent is also documented. Was this the same code, or is this all independently validated with our own code? Level of confidence in the confirmation should be a matter of process that we document.” So how independent a confirmation is, and how much of the claim it covered, are fields, not a sentence in a review.

Every program written here that decides, registered from that date, carries an independence record in verifiers.yaml:

Every new evidence entry with a replay carries an independence record with its coverage: full, or a sample that checked so many of so many of a named unit, as in 6 of 273 chunk runs. An independent implementation carries the authorship fields itself where its deciding programs do not. separate_prompt: null means prompt separation was not recorded. The independence_record path stays beside it, pointing at the prose: a read log, a module statement, or the review that wrote the program.

devtools/verifier_registry.py refuses a first-party program that decides without the record; a new independent-implementation entry without the authorship fields on itself or on every deciding program; any new replay without coverage; clean_room beside producer-code read, a shared component, or code not kept separate; an independent entry whose deciding program shares components; and a sample whose count is zero or is not below its total. An entry claiming a clean room must agree with every deciding program that carries a record; a shared-components entry must name a shared component. Legacy programs, independent entries and replays without coverage are exempt by name in fixed lists that only shrink; tests pin their original membership: an exempt one that gains the record, or stops being what the rule covers, has to leave its list.

The Independence Ladder

The relation to the producer’s code is the level. The level is derived for each evidence run, since one program can reproduce its producer in one run and act independently in another. A transcription of the producer’s definitions shares those definitions. Each level rules out a kind of error the one below it cannot, and none rules out an error in the mathematics or the specification that every implementation follows.

Two attributes stand beside the level, and neither is a level:

• Coverage. A run is full, or a sample of so many of a named unit. A sample decides the instances it ran and nothing about the others: it can find an error, and it cannot show that the rest has none.
• Authoring diversity. Who wrote the confirming code, and whether that overlaps the producer’s. Two programs written by sessions of one AI system family can share a misreading that neither the level nor the coverage reveals, even with separate prompts and separate code.

A result’s stated confidence follows from the rung, the level, the coverage and the diversity, in that order:

1. The rung comes from the evidence alone, as the ladders above say. C3 needs one complete replay of every load-bearing part, at any level; a sample, at any level, sets no rung, and devtools.check_results counts no entry whose coverage is a sample. Bound results need evidence of that bound; values need both the lower and upper sides at every count in their scope, taking the weakest derived rung. Full component evidence establishes its component, not the complete bound or value.
2. The level of each part is the furthest from the producer’s code among the complete confirming runs that decide it, and the result takes the part closest to it (Which Code Confirmed It). A sample at a higher level is stated beside the part, never as its level.
3. Coverage is stated for every part that only samples have reached: sampled, 6 of 273 chunk runs, independently re-implemented. A sample is never called confirmed.
4. Diversity is stated after the level wherever the authorship overlaps the producer’s: independently re-implemented after reading the producer’s code, by a Claude agent, a system family the producer also used.

So two results at the same rung can carry different confidence, and the record says which: C3 reproduced with the producer’s code, beside an independent sample of one step, is not C3 independently re-implemented in full.

Every Run’s Code Is Kept

Any review or lane that runs code on a result keeps that code in the repository and registers it, or states, in the review or in the README that keeps the code, that the run decides nothing. Kept means in the result’s packet, or in devtools when it is a tool, with a README that says what each program does, what it read, how to run it and what it printed. Registered means a program in verifiers.yaml with its independence record, and, for each thing a run decides or samples, an evidence entry with its coverage, cited where it derives no rung it does not support: a sample, or a run that decides one part, is cited by the case record and not by the result. A program kept but cited by no evidence entry says so in its README. The result-import process, stage 4 applies this to the mathematical review at intake.

Review Records

A result’s reviews list the retained review documents the rungs rest on, each mapped in document-map.yaml as a non-superseded review. Each entry records the document’s path, its kind, the reviewer as the document names itself, whether that reviewer is ai or human, the reviewer’s relation to this project (owner, project, external, or source for a review the result’s own source performed), the date, the scope in the reviewer’s words, and the verdict (accepted, defects-resolved, defect-open or refuted). A record shared by a family of results names every result it covers.

• Adversarial AI review (kind: adversarial, reviewer_kind: ai). Rung 4 on either axis needs at least two, by distinct reviewers: a different model family, or a separately prompted independent lane with no shared context. The reviewer names the model and its reasoning setting. The latest-dated review of the result must carry an accepting verdict, so that every defect found has a recorded disposition. A review with relation: source counts toward V and not toward C.
• Human oversight (kind: oversight, reviewer_kind: human). Rung 4 on either axis needs one. The record names the person and their relation, and its checked list includes trust-boundary (what the checker trusts and what it decides), certificate-meaning (that the accepted statement is the claim) and ai-findings (that every adversarial review’s defects were dispositioned). The owner of this project may serve. An approved pull request is not such a record unless the record cites it and says what was inspected.
• Formalization review (kind: formalization, reviewer_kind: human, independent_of_author: true). V5 needs one and C5 needs two, each by a named person who states their competence in the proof assistant and the mathematics and is not the formalization’s author; its checked list includes statement-fidelity, definitions, axioms and build.
• Open review (open_review on the result). C5 needs the proof, its formalization and everything needed to replay it to be openly available, so that any other expert can review and replay it: the record points at the public sources at a pinned revision, the terms under which they may be inspected and run, the public replay instructions, and the copy retained here. No particular review venue is required.

The checker verifies the fields, the mapping, the counts, the distinctness and the coverage. Whether a review was in fact adversarial, whether the models were the best available, and whether the human read what the record says they read, are what the record itself lets a reader judge.

Scope and Composition

A classification attaches to the exact statement in a result’s claim field and its declared scope.

• A compound claim takes the minimum rung of its load-bearing parts, on both axes.
• An equality whose upper half is a packing replayed exactly (E-basic-grid-upper or a witness replay) takes the C of its lower half; a construction is confirmed by its replay, and no second method is asked of it. The composition note says which half sets the rung.
• A derived claim takes the minimum rung of its inputs and the derivation itself.
• A construction’s feasibility, the sharpness of its parameter, and global optimality are separate claims.
• C never exceeds V from C2 up: a replay, a rebuild or a review record is also verification evidence, so the checker refuses a confirmation rung above the verification rung. A read (C1) of a recorded claim (V0) is the one exception, reading being no kind of verification.

The checker derives the strongest rung present among the cited evidence entries and reviews. When a compound or derived result declares a lower rung, its composition note identifies the part that sets the minimum. That note, the relevance of each evidence reference, and coverage of every load-bearing premise are review obligations rather than machine inferences.

Status

A result’s status says in one word how far this project’s own work on it has gone. devtools/result_status.py derives it from the register and the evidence the result cites. It is never stored, so it cannot disagree with the rungs.

A result is incomplete while any of these holds:

• a read found a defect and nothing here has replayed past it: a cited evidence entry’s external_review.state is defect-found and the result stands below C2;
• the latest review in its reviews ends defect-open or refuted;
• a cited replay ran and failed (replay_status: failed).

A defect that a passing replay has gone past is dispositioned by that replay. T-005’s subject is the defect in Bentz’s Lemma 10, and it is confirmed.

Status does not compete with the two ladders. V says what the result’s own source certifies, anywhere. C says how far that has been independently confirmed, rung by rung. Status is the confirmation ladder read in three words, for a reader who wants the workflow step and not the rung, and it adds the one thing the ladder cannot say: that a defect is open. confirmed means C2 and up and nothing more. A result of this project is confirmed from the day it is registered, since its certificate is replayed from the repository before it enters the register.

Two marks sit beside a status and are no part of it.

• Superseded is the result’s place on the frontier: it is a bound, a result whose kind is lower bound, upper bound or optimality, no case bound rests on it now, and its cases hold a bound at least as good as each one it states. Superseded means replaced. A bound strictly better than its case’s, in a lane it can hold, that the case records have not taken in yet is pending adoption and carries no mark: nothing has replaced it, and its status says how far it has been checked. T-128’s eight rational sides, each below the ceiling its case holds, are pending adoption. Superseded is derived from the case records and the bounds each entry states by render_recent_results.standing, and devtools/check_standing.py holds it to those bounds. An entry whose words state no bound the check reads is held to the case records alone, so a report the case records do not cite states its sides. The mark names the results that supersede it, the ones its cases’ bounds rest on now (render_recent_results.superseding), so T-037 reads superseded by T-060. A confirmed result may be superseded, and a recorded one may hold a case’s reported bound. A result of any other kind is not superseded by its standing, though it may cite the evidence of the bound it is about: no later bound supersedes the limit of a method or the audit of a proof. Such a result is superseded only where a later result implies it, which nothing can derive, so its entry declares it in superseded_by: the later result, whether it implies the whole of this one or a part, and what it implies. The whole is marked superseded; a part is marked superseded in part and the result stays current, since it still holds the rest. T-060’s $s(11)=T$$s(11)=T$ implies T-036’s bound for its family and not its equality case, since T-060 makes no claim of uniqueness, so T-036 is superseded in part; T-112, the uniqueness corollary of T-060, implies the equality case and is a second part. No mark says that two parts together make the whole, so T-036 stays current. devtools/check_results.py holds each named result to one dated no earlier, on a case the two share, and refuses the field on a bound, whose supersession is derived.
• Activity says who has the next move, where the record shows it. A register entry may carry activity, with a state of in-analysis (a replay, a review or an audit of the result is under way here) or waiting (a question, a request or a missing artifact is with another party: the source, the owner or a third-party), what is in hand, since when, and a link to the bead, issue, branch or file that shows it. It is the one hand-recorded fact in this section, so it expires: the checker refuses one dated more than 30 days before the register’s last_reviewed, and it is then re-dated with what happened since, or removed. Work that is queued and not begun stays in next_rung, and the confirmations among it are also listed in unfinished_confirmations.

Unfinished confirmations are the confirmations a result’s record names and has not run, or has not finished, listed in its optional unfinished_confirmations where the record knows the work concretely: what the confirmation is, the confirmation rung it would reach, and the bead, issue or file that owns it in link. Wherever a price is known, estimated_cost gives it in CPU-hours: cpu_hours, the central estimate, cpu_hours_high where the source gives an upper end, the basis it was priced on (the sample, the ratio, the host or the source’s own run), and the day it was priced. A price recorded only in wall-hours is converted where the number of workers is stated, and the basis says so. next_rung stays the prose of the next evidence-improving action; this list is the structured, priced part of it. It is no mark beside the status: activity says what is under way, and an item under way is in both. A run that would only add an attribute beside the rung, a second machine method or a reproduction with the producer’s code, reaches no rung and is not listed. devtools/check_results.py refuses an item at or below the result’s confirmation, so an item is removed when its confirmation lands, and refuses an upper end below the estimate, a price dated after last_reviewed, and an item listed twice. The validation backlog (devtools.check_requests --backlog) and RESULTS.md show each item’s rung and cost, and the backlog sums the known CPU-hours.

Until 2026-10-01 the site and RESULTS.md showed a standing in this place, which mixed three things: the frontier position (current best, superseded), whether the bound had been replayed (current best, reported), and what kind of result the entry was (second certificate, not a bound). The first is now the superseded mark, the second is the status, and the third is the result’s kind: a second certificate is a second proof, a simplification or, since 2026-10-13, a formalization. The vocabulary is provisional until the owner confirms it; the proposal and the status of every result are in the result-status plan. On 2026-10-13 the owner added the kind formalization, a proof-assistant proof of a result the record already holds, apart from a simplification. The recorded decision quotes “simplification is one thing but formalization is another”, then “let’s go with formalization then”. Review A relays the owner’s third remark as “simplification should be allowed too but that is different”; the original human message was not recovered. Where a second proof fits both kinds, the owner chooses at registration. The decision was made on T-154, Fitzharding’s Lean 4 proof of $s(17)=L$$s(17)=L$, which was registered as a simplification that day and moved to the new kind, decided 13 October, recorded 14 October (Result Kinds). T-054 and T-055, which no proof assistant checked, stay simplifications.

What Changed on 2026-09-30

Ratings published between 2026-08-31 and 2026-09-30 used a ladder on which V4 meant machine-verified (a certificate with a passing replay), C4 meant confirmed by two distinct machine methods, C5 meant review-ready (one mapped review document), and V5 meant a proof assistant had checked a formalization. On 2026-09-30 the owner reserved rung 5 for formal verification with human experts’ review of the formalization, and required at rung 4 adversarial AI review and a human oversight record, under the no-blind-trust principle above. Every result that held V4 moved to V3, and every result that held C4 or C5 moved to C3, because no retained record of human oversight existed; each such result’s notes says what it held and what restores the rung. Dated prose in reviews, handoffs and the synopsis that names a rung describes the ladder in force when it was written. A result’s claim, composition and next_rung and the case records are not dated prose: they describe the present ladder, and the checker holds the rung labels in them to the rungs the register holds. A significance rationale is dated by its scored, but it scores the claim and not its rungs, so since 2026-10-06 the checker holds it to the same rule: it may say what a rung would need, and not which rung the result stands at. The proposal behind the change is the ladder review of 2026-09-30.

Significance and Novelty

Significance is recorded as a score, rationale, date, and scorer. The score guides reading order and never changes validation behavior.

The scored field dates the current assessment; Git retains earlier values.

Three rules govern scoring:

• The score is of the claim. It says what the result establishes if it is correct; V and C say whether it is. A reported result and a confirmed one take the same score.
• The registering lane drafts and the reviewing lane confirms. A score set when a result is registered is a draft, and by says so. The lane that reviews the result’s mathematics compares it with the entries nearest to it, keeps or changes it, and by then names that review.
• A score follows the claim, not the frontier. It is revisited when the entry’s claim or scope changes. A later result that supersedes the entry does not lower it.

Novelty uses four labels:

Novelty is a scoped statement about a performed search, not a claim of priority. An apparently-novel evidence entry records the corpus, search, narrow novel object, and known gaps in novelty_basis. The result-level label is declared and reviewed; the results checker validates its enum value but does not derive it from the cited entries.

Result Kinds

Every result carries one kind, which says what the result is. The four classifications above say how well a claim is supported and how much it matters; the kind says what sort of claim it is.

The register stores a kind in lowercase with hyphens, lower-bound or case-exclusion. A result has exactly one, chosen by five rules.

• The kind is what the claim concludes. Where a claim ends in a bound or a value of $s(n)$$s(n)$, the kind is that bound, however it was reached: by a repaired proof, an exact check of a published packing, or monotonicity from another result.
• A lower bound that meets a known upper bound is optimality, because the claim states the value.
• A classification of the packings at a value the record already settles is uniqueness, not a second optimality: it concludes which packings attain $s(n)$$s(n)$, not what $s(n)$$s(n)$ is.
• A second proof of a result the record already holds is a simplification, and its claim names the result it proves again.
• A proof in a proof assistant of a result the record already holds is a formalization, whether it formalizes an existing argument or takes a route of its own, and its claim names the result it formalizes or proves again. Where a second proof is both checked by a proof assistant and by a shorter, cleaner or more elementary route, either kind fits, and the owner chooses at registration. A proof-assistant proof of a value the record does not yet hold is no formalization: by the first rule it takes that value’s kind, optimality or a bound.

The kind is declared, and the checker holds it to what the record already says. A headline that opens with a relation on $s(n)$$s(n)$ states its kind: ≥ or > is a lower bound, ≤ or < an upper bound and = optimality, and only a simplification or a formalization may restate one. A bound cites evidence that claims that bound, and optimality cites an exact value or both halves. A second proof records proves_kind, the conclusion it proves again: its target’s kind, or that target’s own proves_kind for a chain of second proofs. It agrees with the relations this proof states and a named target on every claimed case. A single bound requires that side, an exact value both sides, and a structural result its structural evidence; each requirement holds at every count. A formalization cites evidence of its own whose method, performed or reported, is proof-assistant-checked and whose scope and claim substantiate that conclusion on every claimed case. A sample or a component check cannot substantiate a whole bound or value. Evidence that the result it proves again cites is not its own, though a second proof may cite it for a half the two share: a proof assistant’s check of that result is no check of the second proof. A simplification may cite such evidence too, where the owner chose that kind for a proof that fits both. Uniqueness, rigidity, case exclusion and restricted optimality cite derived-structure evidence and state no relation on $s(n)$$s(n)$ in their headline. Method limit, correction and audit are told apart by review alone.

A result’s standing, whether a case bound rests on it now, is about bounds. A result whose evidence claims no bound has no standing, and no later bound supersedes it; a later result that implies it is declared instead (Status). Of a standing, the register’s views show one thing, the superseded mark, which a standing gives only a bound; another kind carries the mark only where its entry declares it.

The standing of a simplification or a formalization reads the relation its claim restates as a bound’s. While every bound it states equals its case record’s in the lane it can hold, it is a second certificate. Its own build can land before that of the result it proves again, as when a reported proof of a value the record holds only as reported is replayed first. It then states a bound better than the case’s verified one, and its standing is pending adoption. A bound better than the case’s reported one is another matter: no lane holds that value, so the entry is no second proof and takes the value’s kind by the first rule, and devtools.check_standing refuses a simplification or a formalization that states one. Neither kind moves a bound by itself, so when the case record adopts that bound the kind is revisited: the owner decides what kind the result then is, and the result page’s registered identity is amended with a dated reason (packing/site-urls.yaml). Until the register records that decision, devtools.check_standing refuses a simplification or a formalization that a case bound rests on, in either lane.

Results by Others

The register holds others’ results beside this project’s, under the same T-NNN identifiers and the same derived rungs, because the work this repository does on them is the same work: register the claim, replay its certificate, review its mathematics. It holds every result of this project, and every result by others published on or after 22 August 2026, the day this project’s square-packing work began, that the record acts on: its bound is or was a case’s reported or verified lower or upper bound, or it has been or is queued to be replayed or reviewed here. Older results enter only when they hold or held a verified field here or are machine audits of the literature. Rungs of a ladder that the same release supersedes, publication records never replayed, and results below the standing bound that ask for no work stay in their case records and packets.

Two things are tracked apart for such a result. Credit belongs to the original result: the entry’s attribution names its source keys and the date it was published, and the authors, the credit line and the lineage are read from bibliography.yaml, never restated. A source’s lineage says how it stands to this project, as the source itself says: builds-on-project, credits-project (inspiration or second-hand credit, with its own method), or independent. Verification is this register’s: V is the strongest verification anywhere, and C what this repository has done. A reported result enters at V0/C0, or C1 once a review has read it, with a next_rung naming the replay and review it waits on, and rises by the same derivation as this project’s own results. Its status reads recorded, then reviewed, then confirmed, and every table that lists results lists it as a row like any other. Whether a bound is current or superseded is derived from the case records and never stored.

Parallel Projects and Their Credit

Other people work on $s(n)$$s(n)$ alongside this project: some from its certificates, some crediting it second-hand, and some independently. The policy is to take in every result of theirs that the scope rule above reaches, and to credit it as carefully as this project’s own.

• The source says who did what. Credit and lineage are read from the source’s own attribution files (README, CREDITS, NOTICE, ATTRIBUTION) at the pinned revision, never inferred here from whose method a result resembles. When a later release changes its attribution, the bibliography key for that release records the new wording.
• Attribution has one policy. Attribution Policy owns preferred person names, aliases, project and tool attribution, credit text and lineage, assistance, PDF presentation, and case-specific decisions. Apply it to first-party records and preserve the wording of archived sources.
• A citation, not a disclaimer. A register claim names the result’s authors, its date and its source, with a link. That a result is another’s is what its credit line and attribution state, and where it was published is the citation’s venue; the claim adds no sentence disclaiming it. The revision and digests of the retained copy are the evidence entry’s and the packet’s, and stay out of sentences (conventions.md → Provenance).
• Our rung is not their credit. V and C describe verification. A result replayed here remains its authors’ result, and a rung never changes a credit line. A defect found here goes back to the authors with the review that found it.
• Priority is stated, not defended. When a parallel result predates or matches one of this project’s, the other result’s date is stated beside ours. Our entry keeps its dated source search and gains a dated annotation that it was reached independently. When a parallel result supersedes ours, the case records move to it, and the register derives the supersession from them.
• Upper bounds count too. A parallel packing that improves a best-known side enters its case’s reported upper lane from a retained source, with the same credit. It reaches the verified upper lane only after an exact or interval witness replay. The coverage gate below checks lower bounds only, so the register entry for an upper bound by others is kept by hand.

Import, Integration, and Reply

The procedure is the result import process. Its three end points are fixed here.

1. Imported. The source is retained at a pinned revision, with a coverage entry. Its bibliography key carries dated, credit and lineage. Its literal claim is in the reported lane, and its register entry is at the derived rung with a next_rung.
2. Integrated. A complete replay here and a review of the mathematics have discharged the certificate’s assumptions, and the verified lane carries the bound. The reader documents (README, synopsis, atlas) state it with its credit and its T-NNN.
3. Answered. An author who asked for the registration, on an issue here or otherwise, has been told what was registered, at which rung, what was replayed, and what remains. The answer goes on their issue, which stays open while work they asked for is still queued. Every issue an intake pass touches is answered, and every later change of its state gets a follow-up until the issue closes with a final comment (stage 7 of result-import.md says what touching is). An agent posts each as part of the pass, under the github-workflows grant, once the pull request that carries the change has merged, and without the grant drafts it for the owner; the owner’s standing instruction of 2026-10-11 is why the rule exists, and the owner may post instead. An answer is kept true: when an id or a rung it states changes, a follow-up says so.

Where the Frontier Is Recorded

Each fact about the frontier has one home, and reader-facing lists of results are generated from these files (OR-1): RESULTS.md, STATUS.md, INVENTORY.md, and the project site’s overview, whose recent results, results table and frontier survey are rendered from them by devtools.render_overview. A T-NNN named in the README or the synopsis must be a registered result; the register gate checks it.

Enforcement and Register

Run the executable contract from packing/ with:

uv run --frozen --all-extras --group dev python -m devtools.check_results

The checker:

• resolves evidence references and artifact, control, and review-document paths;
• derives the structural V and C rungs described above, from the cited evidence and the retained reviews, counting no entry whose independence record states a sample;
• refuses unsupported promotion, unexplained understatement, and a C above V;
• requires every review in reviews to be a non-superseded review in document-map.yaml with the fields of Review Records, counts the adversarial reviews and their distinct reviewers, and requires the human oversight record at rung 4 and the human formalization reviews, the axiom receipt and the open-review pointer at rung 5;
• requires attribution on every previously-published result and refuses it on a novel one, resolves its source keys in the bibliography, and requires a lineage on the sources of a result by others published since 22 August 2026;
• requires a kind on every result, one of the Result Kinds, and cross-checks it against the relations the headline and the claim state, the claims of the cited evidence, and, for a simplification or a formalization, the result its claim names and whether a proof assistant checked the evidence it cites;
• refuses builds_on on a result by others, and on a result of this project holds it to the record: each source key resolves in the bibliography and is the source_key of an evidence entry the result cites, and each credited name is an author of one of them;
• requires a headline of at most 100 characters on every result, stating no number its claim does not, and an established date on every result without attribution, the day its certificate or proof first passed here, which it refuses beside attribution and before 22 August 2026;
• refuses a rung label in a result’s claim, composition, next_rung or significance.rationale, or in a case record, that asserts a rung no result the clause is about declares or derives. A statement of what a rung needs, or of what a result once held, passes; notes is exempt, because it records what each result held before 2026-09-30. The rule reads labels and not arguments, so whether a requirement is stated correctly is a review obligation;
• fails when a case’s reported or verified lower bound cites evidence from a source dated on or after 22 August 2026 that no register entry covering that $n$$n$ cites;
• holds an entry’s activity to its fields, a link that resolves and an age of at most 30 days at the register’s last review, and reports how many results hold each status;
• refuses a sentence of a claim, composition or next_rung that says confirmed without saying which kind; and
• rejects unknown T-NNN references in the README and synopsis.

packing/frontier/results.yaml states each result’s kind, headline, claim, scope, classifications, evidence, artifacts, and next_rung. The headline is the claim shortened for a table cell; the claim stays the statement the rungs attach to. That final field records the next evidence-improving action or explains why no independent rung change applies. packing/frontier/RESULTS.md is generated from the register and sorted for readers.