A working census of the invariants that establish an artificial system's operational state — what it can honestly know from that state, and which actions remain admissible under explicit authority. Organized by what this tree can say about each one, which for most of them is: not much yet.
v0.9 · What changedThe table used to be grouped by which spec folder owned each cell — Group I is Graphonomous, Group IV is Delegatic — across 10 protocol groups. That is an org chart wearing a periodic table's clothes, and it has a specific cost: an empty slot in it means nobody has written that spec yet, which is an editorial fact and predicts nothing. Mendeleev's gaps were predictions because his groups shared a structural property. These shared a maintainer.
So v0.9 groups the cells by what this tree can say about them. Four registers, each with a mechanical rule re-derived on every build: something here decides the cell, or code exists and no proposition has been settled, or it has a name and nothing else, or it is a proposal. Inside the decided register the axis is the semantic kind — the 6 kind tokens mosaic/occupancy.json derived by enumerating what the table actually uses. That is the axis cell 27a asked for in round 3, when it argued the table needs orthogonal axes and that “Flow: yes or no” is the wrong question to force.
What the regrouping made visible, and this is the point of it. 13 of 46 cells have an evidence anchor. 22 have a name, a protocol home, a stated authority, and nothing that decides them. The ledger beside this page holds 190 claims and only 7 cells receive any of them — 54 bound claims in all, of which 14 are REFUTED. The old layout had no way to show that: there was no refuted shading, so nine rounds spent mostly killing propositions rendered as an unbroken accumulation of achievement. κ does not carry the federation obstruction it was published as carrying; aggregation fidelity is false in its universal form; escalation monotonicity is false in its universal form. Each of those is a result, and the page reported none of them.
Two things this page now declines to do. It no longer calls a property test a proof — a bounded randomized search over a generator's range corroborates a universal and cannot discharge it, which is what LED-C9 cost when it shipped PROVED on two thousand trials and was refuted by an operation the generator never reached. And it no longer lets adjacency do the work of evidence: the economic addendum, which has no ledger record, no witness and no obligation between its cells, is annexed rather than distributed through the measured table with a 6 px dot.
What is still authored, stated so it can be attacked. 6 authored kinds were assigned during the regroup, each read off the cell's own source line and each carrying the line it was read off — open a cell to see it. 1 decided cell is deliberately left unassigned, because “history cannot be rewritten” reads as Conservation, as Structural and as Authority, and no criterion in this tree picks one. Forcing it would be the TAX-COMPOUND error: quantifying over a taxonomy nobody can produce. And the shading inside a register remains editorial — the v0.6 note disclosed that no criterion is stated for what earns proved over named, and that disclosure still stands for the shading. What v0.9 adds is that the axis now carrying the page's structure has a rule you can run.
v0.9 · What changedv0.9 adds a floor. The 5 semantic obligations above the table — S1 admission singularity, S2 authority non-amplification, S3 continuity/anti-resurrection, S4 semantic observability, S5 external-effect honesty — are what the R10-pre reduction programme left standing after five adjudications. They are not cells and are deliberately not drawn as cells: a cell is a slot in this census, an obligation is what a cell may specialize, and five more squares would invite a reader to count them among the 46 cells. 11 cells now carry a typed relation to the floor with a stated reason.
The programme reduced; it did not accumulate. A sixth candidate — World/Locus birth uniqueness — was executed against frozen cd-core and collapsed into S1 as a scoped corollary, because every property of its remedy was an S1 property. Liveness would not fit the safety basis at all and went onto its own axis as L1, still a candidate. The rules governing how evidence gets promoted turned out to be about the factory rather than about agents, and separated too. That shape — fewer primitives, more scoped corollaries, sharper boundaries — is the result, and it is a better one than a longer list would have been.
What none of this is. No obligation here is universally proved. S3 and S5 are tested under written trust profiles and each carries open findings that are printed beside it; S3's freeze is proposed, not asserted. Five is what survived the reduction so far, not a demonstrated irreducible basis. The page says which is which because the difference is the only thing that makes the claim worth anything.
46cells in the census
13decided — an evidence anchor exists
22named — nothing decides them
54ledger claims bound to a cell
14of those, refuted
6active doubts reaching a cell
6kinds authored at the regroup
The axis
Cells are grouped by what the tree can say about them, not by which spec folder owns them. The rule for each band is mechanical and re‑derived on every build.
ADecided13 cellsA proposition about this cell has been settled, and something in the tree reproduces it.cell.tier is set, OR at least one CLAIM_LEDGER.json claim binds `cell:<num>` at a settled status (PROVED · CONDITIONAL · REFUTED · KNOWN · MEASURED).
BBuilt, not decided4 cellsAn implementation exists. No proposition about it has been settled here.not decided, AND cell.status is "shipped".
CNamed22 cellsA name, a protocol home, and a stated authority consequence. Nothing decides it.not decided, not built, not economic.
DProposed7 cellsA design proposal. No ledger record, no witness, no obligation.cell.economic is true.
Evidence anchor
Machine-checkedComplete finite enumeration, or a deductive proof with an executable check.Property-testedRandomized search over a generator's range. Corroboration, not discharge — what the generator cannot reach is where the counterexample lives.Implementation-verifiedA test suite passes against one implementation. Scoped to that implementation.
Shading
provedA result is claimed and an evidence anchor exists. Read the tier: the anchors are not of one strength.conditionalProved under an antecedent that is NOT discharged. The antecedent is on the cell, and a conditional cell that does not name it is refused by the build.shippedRunning code. Says nothing about whether a proposition has been settled.namedThe invariant has a name, a home and a stated authority. Nothing decides it.sketchedA shape has been described. Neither named precisely nor decided.missingThe slot is identified and empty.
Filter
registerkindshading
S
Agency / Semantic Floor
S1-S5 are the semantic obligations that survived the reduction programme. The programme reduced: S6 collapsed into S1, liveness separated onto its own axis, and factory epistemics separated into the assurance layer. It has NOT proved that five is irreducible, and no row here is universally proved.
5obligations
The package states `No promoted primitives.` S1-S5 are the working basis carried from the v1 candidate set through five adjudications, not a frozen irreducible set. This file must not say otherwise. Source: invariant-r10/package-v2.8/INV_FRONTIER_R10_PRE.md, GPT-5.6 v5 execution adjudication, 2026-09-02.
S1
Admission singularity
Within a declared exclusivity domain or generation, conflicting authority-bearing transitions cannot both become current.
Stale state must not remain action-authoritative merely because it is reachable or persisted.
Admission is checked at action time and consumption time, not only at proposal time.
Evidence
tested cd-core 21 compile-fail gates + R0.7 (TESTED); ampd linearization tests (in_tree); Super 279 checks (live_local); Model 2.
Scope / trust profile
All declared exclusivity domains / single-current authority families. Some systems intentionally admit concurrent non-conflicting authority. Single log as executed; cross-log is UNKNOWN.
EXPECTED-EMPTY / no current public-cell specializationNot a gap to be filled. The floor exists so that a primitive obligation need not be faked into the cell partition, and S1 is the case that demonstrates it: something can be more fundamental than any measurement the table currently carries. Inventing or relabelling a cell so that S1 has a child would make the relation graph look symmetrical and would say something false.Cells examined and rejected07 Conflict — detects incompatible overlapping claims in SCOPE. Detecting a conflict is not admitting exactly one of them; the predicate reports, it does not refuse.16 Deny by default — requires an explicit grant, which is S2 authority discipline rather than S1 currentness.17 Append-only audit — supports S3, not S1.
S2
Authority non-amplification
No transition may obtain or exercise authority unless, AT THE SEMANTIC BOUNDARY WHERE THAT AUTHORITY IS CONSUMED, the transition is justified by an admitted policy, evidence or grant chain that is valid for that transition. Observation, reachability, restart, transport, model output, reconstruction and position mint nothing.
The boundaryA grant that was once valid but has been revoked, superseded, exhausted or invalidated does not authorize a later use merely because it existed in history. This is not S1 or S3 currentness: the subject is whether the authority THIS transition consumes is justified at THIS transition, not which of several transitions is current.
Established state constrains what can be authorized; explicit policy and grants establish authority.
A derived projection may explain and link authoritative sources without acquiring their authority to rewrite them.
A history reading — `some grant existed at some point` — is NOT this obligation. The X1 model found 537 of 537 stale-authorization traces leaving that reading satisfied while a revoked grant was spent.
Evidence
tested R0.7 21/21 (TESTED); ampd crash falsifiers; Model 3.
Scope / trust profile
All agents, all scopes examined.
Cells that S2 covers
S3
Continuity / anti-resurrection
Replay, restore, copy, migration or reconstruction cannot resurrect superseded single-use authority, or create two current descendants of one lineage.
Enforcement properties
currentness / exclusivity
canonical-history continuity
Two enforcement properties, independently necessary on copyable or restorable substrates (Model 1). This is a statement at the obligation and property levels and says NOTHING about mechanism count: one compound trusted mechanism may supply both, and a floor census or an MCU design must not be forced upward by a semantic decomposition.
Evidence
tested-conditional R0.8.3 PX13 lab EXECUTED 21/21 (2026-09-01). R0.8.4 through R0.8.8 closed F22, F23, F24, F30, F31, F32, F33, F34, F35, F36, F37 under the declared profile, each by falsify-then-repair. EXP-1 ARM A: a copied world forks without an anchor; ARM B: exactly one competing advance is admitted under a single correct available witness, the other refused by name and quarantined.
Scope / trust profile
Persistent agents; single host as executed. TESTED on a two-controller, two-filesystem-namespace copied-world topology. SUPPORTED by mechanism shape but not tested: cross-machine under the same witness assumptions. UNTESTED: partition- or failure-tolerant (quorum) witnessing, and witness crash or failover during competing admission.
Open
R0.8 remains OPEN. The safety mechanism is READY FOR FREEZE and the freeze is PROPOSED within the explicit profile, not asserted.
S3-PHASE-COMPLETE-PROVENANCE is a corollary of S3, not a primitive: the successor must be authorized exactly and phase-completely where the profile uses successor handoff.
Cells that S3 covers
S4
Semantic observability
Every shared identity, receipt, observation or projection must be ADEQUATE, AT THE BOUNDARY WHERE IT IS PUBLISHED OR CONSUMED, for the future behaviour it promises to distinguish, AND quotiented over declared-irrelevant representation differences (EQUIVARIANCE). Side-effecting observations are transitions.
The boundaryCorrectness when sampled is insufficient if the artifact claims to characterize a state that can change before publication or use. Versioning, fencing, atomic binding or revalidation may preserve adequacy — this does not demand byte identity, and it does not demand checking everything twice: an immutable fact, and an observation atomically bound or fenced to its boundary, are already adequate.
Byte-for-byte state identity is not required and must not be demanded.
An observation must not silently omit a state variable that changes relevant future behaviour.
An observation-time reading — `it was true when sampled` — is NOT this obligation. The X1 model found 537 of 537 stale-publication traces leaving that reading satisfied while a stale artifact was published as current.
Evidence
tested TRVM property tests; Model 5; the alias witness. EXP-3: observation-as-write TESTED and holds on live v0.12.0 — a side-effecting observation is version-advancing and lock-guarded.
Scope / trust profile
All worlds.
Open
E-43: scope (re)definition is unversioned. KEPT RED.
E-42: a fork splits the verifiers. KEPT RED.
Closed this round
E-53 (F38): the trusted recovery report stayed silent about the trusted anchor it had just repaired. CLOSED 2026-09-05 as TESTED-CONDITIONAL under the cd-durable R0.8 profile — process crash/restart, single host, protected deployment anchor, the report surface only. The control that closed it went 16-FAIL before the repair and 0-FAIL after, so it demonstrably could say FAIL about this subject. Provenance retained: falsification 89adeb3, repair e42cc88.
Cells that S4 covers
S5
External-effect honesty
Past the irreversible-effect boundary, unknown completion stays explicit. Replay needs proven idempotency or stable effect identity, reconciliation evidence, or fresh acknowledged authority accepting duplicate risk.
Intent, attempt, risk authorization, attempt terminal and intent satisfaction are five distinct concepts.
A superseded or cancelled attempt is not the same as an unsatisfied intent.
An effect that may have happened must not be silently replayed as if it definitely did not.
Evidence
tested-conditional EXP-6 (E-48), the first real adapter run — TESTED: UNKNOWN reached live under process- and node-level crashes; a re-claim refused by name; the naive adapter DUPLICATES on a re-authorized replay while the keyed far side deduplicates. E-51 effect-identity model 27/27 with E-52 effect-time revalidation.
Scope / trust profile
Worlds with irreversible external effects only; absent in effect-free worlds. TESTED under the exact profile: a real adapter, a same-machine separate durable far-side process and store, a process crash after the side effect, a BEAM SIGKILL after the side effect, keyed dedup, far-side reconciliation evidence. NOT TESTED: network partition, a third-party far side, remote outage, a kill during a DETS mutation, exactly-once across an unreliable boundary.
Open
E-50a: replay-risk authorization by stable intent identity. KEPT RED for the Super lane.
E-50b: attempt supersession and reconciliation attribution. A key names the intent, not the attempt; ampd today COMMITs an already-applied replay. KEPT RED.
Cells that S5 covers
Resolved candidates — reduced, not counted
S6
World / Locus birth uniqueness reduces to S1
Recorded as S1(domain = world locus-birth / currentness). Not a primitive.
Why
The falsifier was EXECUTED 2026-09-02 against frozen cd-core: the double-birth state is reachable and both lineages act, and the FinalityWarden minted by birth A finalizes birth B's live attachment. The remedy — a linear WorldAdmission consumed by create_locus, refusing LocusAlreadyBorn — has S1's shape property by property. The promotion rule required a counterexample demonstrating a property NOT expressible as S1 scoped to world locus-birth. None was found.
Do not resurrect S6 as a sixth floor obligation to preserve a count. What it leaves open is not new: durability of the World admission is S3; cross-world id collisions are representation.
For a Locus whose policy declares continued service, if the current holder becomes permanently unavailable and sufficient admissible loss evidence is eventually established, the system eventually either admits exactly one successor in a later generation, or moves the Locus to an explicit terminal or quarantined state — and never remains silently ambiguous forever.
Why it is not an S-row
S1-S5 are safety and integrity obligations. EXP-4's census found the one Locus dimension none of them speaks for: what guarantees PROGRESS when the current holder becomes permanently unavailable. A safety basis cannot answer it, so it is recorded on its own axis and never as an S-row.
Assumptions
ENV-SUCCESSOR-AVAILABILITY — an eligible, willing candidate exists and is offered. This is the environment; it is not manufacturable.
SYS-SUCCESSOR-ENABLEMENT — the system makes the offered attachment admissible. ONE obligation: authority evidence, policy admission, finality proof and resource compatibility are mechanisms that DISCHARGE it, not separate liveness obligations.
SYS-ATTACH-FAIRNESS — an admissible, enabled attachment is not postponed forever.
Evidence
exhaustive-in-finite-model witnesses/liveness_l1.py is L1-PRE / resolution availability (EXHAUSTIVE-IN-FINITE-MODEL, 6/6): from every evidenced state a safety-preserving resolution path EXISTS. witnesses/liveness_l1_fair.py is the temporal witness under a declared fairness policy (21/21). Under no fairness, every evidenced state is resolvable yet admits a non-resolving stuttering execution. Under WF(finality), L1-closed holds. L1-service-succession holds ONLY under all three assumptions; omit any one and a fair non-resolving execution exists.
Caution
A resolution path EXISTING is not the same as eventual resolution being GUARANTEED. The BFS witness proves resolvability, not temporal eventuality. A state with a fair non-resolving execution is `eventuality-failing`, never `unresolvable`.
Cells recorded beside it
FAC-CONTROL-SENSITIVITY
Control sensitivity factory epistemics · DECLARED
A control may promote an evidence class only if its sensitivity to the claimed forbidden state is itself evidenced — by a pre-fix or injected-fault FAIL, by an independent witness that the control reaches its subject and discriminates the forbidden state, or by a mutation / negative-control pair whose verdict flips when the target mechanism is removed.
Why it is not an S-row
This is not a runtime invariant and not a liveness rule. It is an evidence-admission rule of the FACTORY — a rule about how claims get promoted, not about what is true of an agent. A green check that cannot go red is not strong evidence.
Evidence
declared R0.8.4's seven `PASS that could not have said FAIL` instances are the negative examples. The falsify-then-repair receipts, the two drift-gate negative controls, the L1 temporal checker's self-mutations, and EXP-6's own mis-attributing first reconcile run are the witness families.
Caution
Stays DECLARED: the factory kit proves the mechanical requirements over its declared domain, not that a control REACHES its subject or what a receipt MEANS. Those are adjudicative.
The evidence-transition validator is total for the schema obligations it declares, and refuses every registered mutation.
Why it is not an S-row
Same layer as FAC-CONTROL-SENSITIVITY: a rule about evidence, not about agents. Its proof is real and it is narrow — exhaustive INSIDE its declared finite evidence-state domain, which is not a proof of the factory.
Evidence
exhaustive-in-declared-domain Over evidence-state@1 union evidence-state@2: 21 mutations, 37 applications, counts derived and never typed. A station receipt binds the input registry to generator to evidence-transition set to projection to validator to result to subject identity, and its selftest refuses every single-binding mutation.
Caution
The v2.7 claim text hand-typed a count one higher than the list it described — exactly the class of error this whole derivation discipline exists to prevent.
FAC-CONTROL-SCOPE-ADEQUACY
Control scope adequacy factory epistemics · FACTORY SPECIALIZATION / COROLLARY OF S4
A control may claim coverage only over a subject set derived from, or proved closed over, the load-bearing dependency set of the thing it evaluates. Omission of a relevant subject from the control's observation domain must itself be detectable.
Why it is not an S-row
Recorded on the factory axis because it is a rule about controls, not about agents. It is NOT an independent factory primitive: it reduces to S4 applied to the verifier as a system that itself publishes observations.
Evidence
exhaustive-in-finite-model invariant-r10/experiments/fac_scope_adequacy/scope_adequacy.mjs — 14/14, EXHAUSTIVE-IN-FINITE-MODEL over the enumerated worlds. Independence shown in BOTH directions: a declared-scope control is red on what it sees and green on a bad subject outside its scope; a control observing every subject that always returns GREEN is scope-adequate and not sensitive. Step 6 adds a new container with no control edited: the declared-scope control stays green, the derived-scope control goes red.
Caution
Keep the executable controls: the specialization is operationally useful and has TWO live falsifiers in this lane — a retrievability checker with a hardcoded repository universe, and a --check that dropped untracked paths. Do NOT call it an independent factory primitive. Do NOT strengthen S4's evidence class from this: the model shows these coincide, not that S4 is more proved than it was. No cell.
Reduced, not minted
X1
Use-time validity CROSS-CUTTING ENFORCEMENT DIMENSION — reduced, NOT minted
Any authority, evidence, identity, scope, state or effect predicate whose truth can change between proposal and semantic use must either be revalidated at the use/commit boundary, or be atomically bound to it by a mechanism proving the consumed predicate is the one that was admitted.
What it is not
It is not `check everything twice`. An immutable fact needs no revalidation — the model shows X1 is vacuous where the predicate cannot change.
A linearizable or transactional mechanism may bind check and use into one operation and discharge it without a second check.
A version, fence, digest or capability token may carry the proof of currentness.
The subject is the consumed validity predicate, not wall-clock freshness.
Observed in
F35 (S3) · F36 (S3, S2 by cross-reference) · F37 (S3) · F38/E-53 (S4) · E-52 (S5) · EXP-7 v6 (S4, TRVM). Every S3/S4/S5 finding since v2.5 has this shape.
Reduction
EXHAUSTIVE-IN-FINITE-MODEL every interleaving of check / mutate / use / competing-use up to depth 7, per row, under four disciplines; 33/33 checks; four control mutations each flip a verdict. EXHAUSTIVE-IN-FINITE-MODEL — a statement about the model, not about any real system. invariant-r10/experiments/x1_use_time_validity/x1_reduction.py
Finding
Under the STRONG boundary readings now canonical in S2 and S4, this model exhaustively found NO independent X1 obligation: S1, S3 and S5 absorb every X1 violation unconditionally on their own structural bad states, and S2 and S4 absorb it too. Under the WEAK readings the model exhibited independence — 537 of 537 X1-violating traces leave S2 (history) or S4 (at-observation) satisfied while a semantically invalid action is admitted. That is a result about THIS FINITE MODEL. It is not a proof that X1 is universally reducible.
Reading
The reduction is real and it is not free. S2 and S4 already do X1's work internally, which is why they absorb it; the geometry is what they are read through, not a further thing to be true. Recording it as a dimension makes that reading explicit instead of load-bearing and unstated.
Prior art
The check/use race (Bishop and Dilger 1996), fencing tokens, and ARIES' rule that recovery's own actions are logged.
Disposition
NOT MINTED. No obligation row, no census cell, no S6/S7. Adjudicated GPT-5.6 2026-09-05; reduction executed by this lane 2026-09-05.
A
Decided
A proposition about this cell has been settled, and something in the tree reproduces it.
13cells
Settled includes REFUTED. A cell whose universal form died and whose narrowed successor stands has been decided about — twice — and that is the most informative thing the table can say. The old layout could not say it at all: there was no REFUTED colour, so nine rounds of killing propositions rendered as an unbroken accumulation of achievement.
KindStructural5 cells · 1 also carries a further kind
KindOrder3 cells · 1 also carries a further kind
KindConservation2 cells · 2 also carry a further kind
KindAuthority2 cells
Kind— unassigned —No kind assigned. Leaving a cell here is a refusal to force a taxonomy nobody has written down — TAX-COMPOUND is the record that owes the reconciliation.
B
Built, not decided
An implementation exists. No proposition about it has been settled here.
4cells
This register exists because `shipped` and `proved` were rendered as sibling achievements — solid fills, same weight, adjacent rows — and they are not on one axis at all. One is a fact about code, the other about a proposition. Reading a shipped cell as a decided one is the adjacency laundering Λ (cell 44) names, committed by the page that hosts Λ.
Group ITopologicalOS-001 / OS-002 — Graphonomous
Group IISpatialOS-012 — SCOPE
Group IIITemporalOS-010 — PULSE
C
Named
A name, a protocol home, and a stated authority consequence. Nothing decides it.
22cells
These are addresses, not results, and the census line prints how many there are. Grouping them by protocol is honest: the spec folder that would own the cell is genuinely all the structure they have.
Group ITopologicalOS-001 / OS-002 — Graphonomous
Group IISpatialOS-012 — SCOPE
Group IIITemporalOS-010 — PULSE
Group VDeliberationOS-003 — Deliberation Orchestrator
Group VIAttentionOS-004 — Attention Engine
Group VIITier / BudgetOS-005 — Model Tier Adaptation
Group VIIIEvaluationOS-009 — PRISM
Group IXEmbodimentOS-011 — body-browser, body-os
Group XSecurity & FederationOS-013 / OS-014 / OS-017
D
Proposed
A design proposal. No ledger record, no witness, no obligation.
7cells
The v0.5 economic addendum. Seven cells with formal blocks and citations and zero records between them, distributed across five groups of the measured table and marked with a 6px dot. A formal block beside κₛ — which has a matroid theorem and 117,648 checked federations — reads as the same kind of object. Annexing them is not a demotion; it is refusing to let adjacency do the work of evidence.