docs/foundation.md

The Foundation

Status: frozen. This document is infrastructure, not a subject of redesign.

It records the framework used to audit constitutional change: what a defect can be, how a new category of defect is admitted, the sense in which the taxonomy is complete, and the exact assumptions completeness rests on.

Modification of this framework is held to a higher standard than constitutional amendment. A proposal to alter it must demonstrate that the existing framework cannot express an observed phenomenon — not that it expresses it inelegantly. The default assumption is that the architecture is complete until disproven.

1. The witness lattice

A governance system generates executions: sequences of acts by principals against records under rules. A defect is a scenario permitted by the rules but contrary to intent. Defects are therefore properties of executions, and the operative question is not "what kind of thing went wrong?" but:

What is the shape of the smallest object that witnesses a violation?

That object has exactly two structural parameters, and they are the axes:

Witness arity — how many executions must be exhibited together to demonstrate the violation.
Witness finiteness — whether a finite prefix suffices, or only an infinite execution witnesses it.

	finite witness (safety)	infinite witness (liveness)
1 execution	Authority · Content · Binding	Termination, ratchet, tractability
≥2 executions	Attestation, non-repudiation	unexamined

1.1 Authority / Content / Binding are not dimensions

They are a descriptive subdivision of the single cell (1 execution, finite witness), retained because it is a useful search order, not because it is foundational:

Authority — who may act, and how an act binds to an actor.
Content — what the text says, and how it composes with existing text.
Binding — how text connects to reality: form, record, process, enforcement.

Treating these as peers of Liveness was the original taxonomic error. They answer "can something impermissible occur?"; they have no vocabulary for "will something permissible ever occur?"

1.2 State, trace obligation, and evidence are three different things

Conflating them produced a circular argument that took several passes to unwind, so the separation is recorded here as foundational:

State describes the constitutional configuration — what is currently true. Modelled as ⟨C, L, D⟩: constitutional text, ledger, decision received.
Trace obligations constrain how an execution may occur. They are properties of executions, not of states, and need no state variable.
Evidence is whether a later observer can tell which execution occurred.

Failure of auditability does not, by itself, imply missing state. An obligation may be genuinely binding, genuinely violated, and leave no trace distinguishing compliance from violation. That is an evidentiary limitation — sited in this lattice at (≥2 executions, finite), the attestation cell — not a state omission.

Article IX is the worked example. It requires that classification occur before implementation; it does not require that the classification remain verifiable afterwards. Every operative word is act-shaped: "may never silently convert", "Classification is stated before implementation begins". IX.2 anticipates the audit case and disposes of it by voiding the late claim rather than by requiring a record. Decisively, Article XII shows the Constitution knows how to impose a persistence obligation when it wants one — XII.3 enumerates articles affected, reason, probe, initiator, decision — and classification is not among them. VII.1's probe requirement scopes to "every invariant above", and Article VII precedes Article IX, so IX carries no probe obligation either.

Article IX is therefore a trace property, and specifically a safety property: a violation is witnessed by the finite prefix containing an implementation act with no preceding classification. Cell (1, finite).

The corollary matters for any future proof: a transition system over states is the wrong shape for IX-class obligations. Reachability must be computed over executions, not over states, whenever a guard depends on what happened earlier rather than on what is currently true.

2. The admission rule

A candidate category is admitted as a dimension only if it discharges both obligations. Discharging the first alone makes it a sub-class.

(i) Separating witness. Exhibit a concrete scenario that is defect-free under every admitted class and defective under the candidate. Establishes independence.

(ii) Witness-structure novelty. Show the minimal counterexample has a shape not producible in any existing cell — a different arity, or a different finiteness. Establishes that it is a dimension rather than a new occupant of an old cell.

Obligation (ii) is checkable rather than rhetorical: state the minimal counterexample and read off its coordinates. If the cell is occupied, the finding is an instance however novel it feels.

2.0 The companion rule — admission of architectural abstractions

The rule above governs defect classes. This one governs architectural abstractions — layers, concepts, dimensions, types. It is recorded here rather than in its own document because it is the same section's subject seen from a second angle, and because rule 5 below requires preferring refinement to expansion. Splitting it out would have been the first thing it forbids.

The objective is explanatory sufficiency, not minimality.

An abstraction earns its existence only if it increases the system's explanatory power more than it increases its complexity. It should be removed when eliminating it preserves the system's ability to completely reconstruct reality from evidence.

The architecture converges toward the simplest model that preserves complete explanatory power, complete provenance, and complete reconstructability.

The measure of success is therefore not layer count, file count, or conceptual minimalism. It is whether every observation can be reconstructed through the invariant chain, and whether every rendered primitive admits an exact inverse back to evidence.

The goal is not fewer abstractions. The goal is that every abstraction is indispensable. Those differ: minimality would remove a layer that carries real explanatory weight; explanatory sufficiency will not.

Falsified: "optimize for complete reconstructability" as the general criterion

Proposed as a possible replacement — every abstraction must increase reconstructability; any that does not is redundant; any missing abstraction that prevents reconstructability is required. It fails as a general criterion, on three independent counts. It survives, and is retained, as the invariant on the provenance chain, which is where it already lives as the north star.

1. Decisive, and measured here. A complete chain can terminate at the wrong evidence. Building height today reconstructs perfectly:

pixel ← height ← base + log10(code-size + 1) × scale
               ← MeasureFact{metric:"code-size", value, evidence}
               ← repository scan

Every link inverts. The evidence string is present. "Why is this building that tall?" is answerable exactly. And Article II.2 states: "It is forbidden to derive height from code size, file counts, or any measure of how much has been written rather than done." The chain is flawless and constitutionally prohibited. Reconstructability is necessary, not sufficient — a perfectly invertible chain to the wrong fact documents its lie precisely rather than preventing it.

2. It has no cost term. "Any abstraction that does not increase reconstructability is redundant" is one-sided: it admits anything that increases reconstructability at any complexity. A provenance-annotation layer recording which line of code read each fact would increase reconstructability and be required under this wording. Explanatory sufficiency rejects it on the trade-off. Dropping the cost term is a weakening, not a strengthening.

3. It does not reach non-chain abstractions. Liveness does not increase reconstructability at all — it concerns whether a decision ever arrives, which is orthogonal to inverting rendered primitives. Under the literal wording it would be redundant, yet it is the class that identified the governance deadlock.

What this leaves — three criteria, not one

	Question	Scope	Where it lives
Reconstructability	Can the chain be inverted?	the provenance chain	north star, `visualization-invariant.md`
Explanatory sufficiency	Does the abstraction earn its complexity?	all abstractions	§2.0 above
Semantic correctness	Does the chain terminate at the right evidence?	each visual property	the Legend

The proposal collapses the first two and loses the third entirely. The third is not new machinery — the Legend already declares what each visual property represents and which source it derives from. That is precisely the mechanism reconstructability cannot supply, and II.2 is its standing violation.

Recorded as a negative result: the wording is retained where it is correct and rejected where it over-reaches.

Falsified: that the three criteria derive from one deeper invariant

Test. Find a case satisfying any two criteria while violating the third. If all three pairs are realizable, the criteria are independent.

All three were realized, each from live code in this repository.

Case	R	ES	SC	Instance
1	✓	✓	✗	Building height from code-size. The chain inverts perfectly (measured above). `MeasureFact` earns its place — one family serving many metrics, no duplication. And Article II.2 forbids deriving height from code size.
2	✓	✗	✓	`CapacityFact`. Evidence is complete — `hq_agent_run state='running' → N of M enforced slots` — so it inverts. It is semantically correct: the Data Centre's ceiling genuinely is the dispatcher's enforced limit, `basis: "dispatcher concurrency limit"`. But one producer, and every field maps onto `MeasureFact{limit, enforced}`.
3	✗	✓	✓	`dependsOn` → data link. The `Link` abstraction earns its place; nothing else expresses relationships. It is semantically correct — the evidence reads "declared dependency in the estate register", which is exactly what it is. But the chain terminates at a hand-written array, not at evidence (Gap 7).

The criteria are independent. No single invariant yields all three.

The better result — they are already three articles

Independence would ordinarily argue for a new constitutional dimension. It does not here, because the three criteria are restatements of text the Constitution already contains:

Criterion	Existing article
Reconstructability	I.1 — "Every visible object traces to a stored operational fact."
Explanatory sufficiency	I.4 — "One fact has exactly one representation. If two things can disagree, one of them is wrong by construction." A redundant abstraction is a second representation.
Semantic correctness	Article II, the Legend — which declares what each visual property represents and which source it derives from.

They are independent in the Constitution too, and have been since it was written. So the answer to "independent principles, or projections of a deeper invariant?" is neither: three existing articles, already separate.

Consequence: no new dimension, and no amendment. What is required is mechanization — and each of the three already has a standing violation, which is why the criteria felt like discoveries:

I.1 is broken at two points → Gap 7 (accent, data links do not invert).
I.4 is violated → CapacityFact, a second representation of one fact family.
Article II is violated → II.2, height from code size.

The criteria were not new knowledge. They were three unmechanized articles making themselves felt through their violations.

One residual, recorded as a tripwire rather than a gap

I.4 covers explanatory sufficiency's elimination case exactly — an abstraction adding no explanatory power is a second representation. It does not cover the cost case: an abstraction that adds real explanatory power but costs more than it returns. That has no constitutional home.

It also has no measured instance in this repository. Under §2.0 rule 2, an unmeasured ambiguity does not justify new text. Recorded so that if such an instance is ever measured, the gap is already named.

Begin with the smallest architecture capable of expressing the measured system.
Introduce no new abstraction unless a measured ambiguity cannot be expressed within the existing architecture.
Every proposed abstraction must identify: the specific ambiguity it resolves; why the existing architecture cannot resolve it; the minimal responsibility it owns; the invariants it introduces; and why it reduces overall complexity rather than redistributing it.
Reject abstractions introduced solely for symmetry, completeness, or anticipated future use.
Treat every architectural layer as provisional until justified by evidence.

Why this is not a duplicate of §2. Two of the five obligations map onto the existing rule — "the specific ambiguity" is a separating witness, and "why the existing architecture cannot resolve it" is witness-structure novelty. The other three do not map at all, because they ask a different question. §2 asks is this distinct?; this asks is this worth it? A distinct abstraction can still be a bad trade, and nothing in §2 could have said so.

Evidence from this repository

Four data points, three negative and one positive, all from the constitutional work rather than from principle:

Abstraction	Outcome	Rule
K, a classification state variable	Proposed, retracted. Article IX read as a trace obligation absorbed the responsibility with no new state.	5 — refinement over expansion
X.3, a ratification-lifecycle article	Proposed, withdrawn. Advanced partly for completeness; refuted because Article IX could never have been ratified under it.	4 — reject completeness-driven additions
Liveness, a lattice dimension	Admitted, on a separating witness that no existing class could express.	2, 3 — the positive case
`CapacityFact`	Live, and failing. See below.	2

CapacityFact is the standing counterexample and it is measurable rather than argued: it has exactly one producer (substrate/runtime.ts:251), and MeasureFact already carries limit and enforced. Every field maps — used→value, basis→evidence. It resolves no ambiguity MeasureFact cannot express, so under rule 2 it does not earn its existence today. It is retained only because removing it is a migration, not because it is justified.

That entry matters more than the other three: it shows the rule has bite against something already built, not only against proposals.

2.1 The rule caught a misclassification

Attestation — a forged approval is indistinguishable from a real one — was first filed under Authority, a 1-execution cell. But no single execution witnesses forgery: the forged and authorized executions are identical in the record. The violation is that two distinct realities map to one trace, so the witness requires two executions. Attestation is arity-2, and the rule detected the misfiling independently of the intuition that produced it.

3. The convergence theorem

Complete for execution-relative governance defects under a version function that is prefix-determined and well-founded, with the safety/liveness decomposition preserved at every rule-version.

Convergence is established by showing the witness lattice is covered — never by failing to find new defects. Every audit pass that reasoned from absence of findings felt converged and was not.

3.1 Borrowed results

Alpern & Schneider (1985) — every trace property is the intersection of a safety property and a liveness property. Fixes the count at 2 for arity 1.
Clarkson & Schneider (2010) — hyperproperties decompose the same way into hypersafety and hyperliveness. Extends the result to arity ≥ 2.

New dimensions can therefore appear only by increasing arity; within an arity, the safety/liveness split is provably exhaustive and everything else is refinement.

3.2 Lemma 1 — Version-Indexed Decomposition

The system being governed amends itself, so the rules are not static. This was initially recorded as an unresolved assumption ("fixed semantics"). It is not.

Let Σ be the alphabet of recorded acts, σ ∈ Σ^ω an execution, V the rule-versions, and v : Σ* → V the version function giving the constitution in force after a finite history. Call v prefix-determined when v(w) depends only on w.

Two candidate semantics:

S1, prospective — σ ⊨ P_dyn iff for all i, act σᵢ is permitted by v(σ[0..i−1]). Each act is judged by the rules in force when it occurred.
S2, retrospective — σ is judged wholly by the final version; amendments reinterpret history.

The Constitution selects S1 explicitly: Article 0.3 prohibits reinterpreting a rule, and the prohibition is repeated in Article X's blocking clause.

Lemma 1. If v is prefix-determined then (a) P_dyn is a well-defined subset of Σ^ω; (b) Alpern–Schneider applies unchanged, so P_dyn = Safe(P_dyn) ∩ Live(P_dyn); (c) if per-version compliance is a per-act condition, P_dyn is a safety property.

Proof of (c). Suppose σ ∉ P_dyn. Then some σᵢ is not permitted by v(σ[0..i−1]). Take the finite prefix σ[0..i]. Every σ′ extending it shares that prefix, so by prefix-determination v(σ′[0..i−1]) = v(σ[0..i−1]) and σ′ᵢ = σᵢ; hence σ′ ∉ P_dyn. The violation is irremediable, the complement is open, P_dyn is safety. ∎

The operative insight is that Alpern–Schneider requires only that the property be a set of traces — not that the rules be static. Prefix-determination is what collapses a time-varying rule system into a single well-defined trace set. The same argument lifts to Clarkson–Schneider for hyperproperties.

3.3 Theorem — Retroactivity collapses safety into liveness

Under S2, no violation has a finite witness. For any finite prefix exhibiting an apparent violation there is an extension containing a retroactive amendment that legitimizes it, so every violation claim takes the form "no future amendment ever legitimizes this" — a liveness property, refutable only by an infinite trace.

Corollary. A constitution permitting retroactive amendment is not adjudicable in finite time. No finite audit can establish a violation.

This gives Article 0.3 a formal role it did not previously have. The prohibition on reinterpretation is not hygiene; it is the precondition under which constitutional violations are decidable at all.

Retrospective is not retroactive. A clause applying to pre-existing entities going forward is retrospective and harmless. Only changing whether a past act was compliant breaks Lemma 1.

4. Assumptions and their limits

	Status
A1 — In-model restriction. Defects are properties of executions relative to a fixed intent. A failure of the form "the system does exactly what it should, and what it should do is wrong" is a property of the specification's relation to purpose. Outside by construction.	assumption
A3 — Arity is observability-relative. Attestation is arity-2 because principal identity is unrecorded; record it and the same defect becomes arity-1. Cell assignment is relative to the observation model, not intrinsic.	assumption
A4 — Non-probabilistic. Measure-valued properties ("a decision arrives with probability ≥ 0.9") do not decompose into safety ∩ liveness and are excluded.	assumption
A5 — Discrete, countable acts. Required for trace semantics.	assumption
Condition NR — non-retroactivity. Verified: `CONSTITUTION.md` contains no retroactivity provision; the only matches are three prohibitions on reinterpretation. Version in force is determined by recorded acts (X.1.6, XII.2).	verified against the text
Condition WF — well-foundedness.	OPEN — the sole irreducible boundary

4.1 Condition WF, recorded

Not discharged. If an amendment changes the amendment procedure, v is defined by a recursion that may lack a fixpoint: Article X's own procedure would adjudicate a change to that procedure. Whether the recursion is well-founded depends on whether an amendment takes effect before or after its own ratification is judged, and no article says.

This is instantiated, not hypothetical: AMD-0003 draft 1 proposed X.3, an amendment to Article X governing how amendments are ratified. Any future proposal touching Article X re-raises it.

Discharging WF requires either a proof that the recursion terminates under the current text, or an article fixing the effective moment of an amendment relative to its own adjudication.

5. Negative results — permanent boundary conditions

Preserved deliberately. A rejected candidate is part of the theory: it marks where the boundary is, and re-proposing it requires defeating the recorded reason.

5.1 Rejected candidate dimensions

Candidate	Why rejected
Probabilistic liveness — "a decision arrives with probability ≥ 0.9"	Genuinely outside safety ∩ liveness, but the witness is a measure over the full trace set — arity ω. Changes a coordinate rather than escaping the grid. Excluded by A4.
Environmental composition — the pipeline ignores the gate	Witness is one finite trace. Cell (1, finite). Refinement.
Rule-laundering — an amendment proposed in order to legitimize a forbidden act	Without observable motivation the laundering trace is indistinguishable from a legitimate amendment followed by a legitimate act. Structurally identical to attestation: arity ≥ 2, hypersafety.
Self-amendment drift — the boiling-frog sequence	The defect is real but turns on which version is authoritative. The lattice classifies properties; it does not choose them. Property-selection, not classification.
Aesthetics / review tractability	Important, not fundamental. Witness is a single finite artifact — cell (1, finite). Sub-class.

5.2 Failed completeness arguments

Arguing from absence of findings. Four consecutive audit passes concluded convergence because nothing new was found. Each was wrong. Absence of findings is evidence about the search, not about the space.
Searching driven by the previous finding. Passes 1–3 each searched adjacent to the last defect. All three searched two layers of three, because no frame had been declared. Declaring the frame first is what surfaced the missing layer.
Weakly informative negative results. Given the borrowed theorems, "no unclassifiable defect at fixed arity and finiteness" is close to tautological. The lattice's strength is inherited, and transfers only as far as the theorems' hypotheses hold — which is why §4 carries more weight than any failed counterexample.

5.3 Retracted: the classification state variable K

Proposed and withdrawn. Recorded because the reason it failed is the most reusable result in this section.

The claim. Article IX.2 makes the lawfulness of an implementation act depend on whether a classification was stated beforehand. That prior act appears in no constitutional file, so the state must be extended to ⟨C, L, D, K⟩ with K the classification record.

The supporting witness was valid and remains valid. Two lawfully reachable executions — one where the classification was stated, one where it was not — reach a byte-identical ⟨C, L, D⟩, yet the next act is lawful in one and not the other. Verified against this repository: the classification for docs/foundation.md appears nowhere in CONSTITUTION.md, constitution/amendments.json, or src/lib/world/constitution.ts, and the commit message repeating it was authored after the act, making it justification rather than classification under IX.2.

Why the claim nonetheless failed. The witness proves state insufficiency only if the Constitution requires the distinction to remain observable after execution. It does not — see §1.2. So the witness establishes an evidentiary limitation, not a state omission. The error was conflating "affects lawfulness" with "must be in the state"; the correct move is to model the obligation over executions, which the lattice already does.

Reusable form. A history-dependent guard forces a state variable only when the specification requires the history to remain observable. Otherwise it forces a trace property. Any future proposal to extend the state must discharge that distinction first.

6. Where future work belongs

Applying §2.0 to what already exists. The rule has one live failure on record — CapacityFact — and nothing systematically checks the rest. An abstraction that stops earning its existence does not announce itself.
Proofs or refutations of the stated assumptions — principally Condition WF.
Application to constitutional governance and repository evolution.
Discovery of defects within existing lattice cells.
Empirical evidence of a genuine counterexample requiring a new dimension — which must discharge both obligations of §2.

Categories 1–3 are ordinary work. Category 4 is the only route to altering this document, and it carries the burden stated at the top.

7. Open questions

Distinguished from §4's assumptions: those are load-bearing for the theory. These are live questions the theory does not settle.

7.1 Condition WF — formal (see §4.1)

The sole irreducible boundary. A proof that the amendment recursion terminates under the current text, or an article fixing when an amendment takes effect relative to its own adjudication.

7.2 Should Article IX require persistent evidence of classification?

A specification-philosophy question, not a defect. Under the text as written (§1.2), Article IX is intentionally unauditable: it requires the classification to occur and imposes no obligation that evidence survive. That is formally coherent — no article is violated.

The tension worth noting is with Article VII's own preamble: "A rule that cannot be checked is advice, not a constitution." VII.1's probe requirement scopes to articles above VII and so does not reach IX, meaning there is no formal contradiction — but there is a real gap between IX's design and VII's stated philosophy.

Whether to close it is a design choice with a cost on each side. Requiring a recorded classification makes IX auditable and would collapse its evidentiary gap from the (≥2, finite) cell to (1, finite), per A3. It also adds a persistence obligation to every implementation act, and Article XII's field list shows the Constitution has so far reserved that weight for amendments alone.

Not proposed. Recorded so that a future proposal starts from the analysis rather than rediscovering it.

7.3 Re-derivation — discharged

Closed. The constitutional transition-system proofs were built over states and have been reformulated over executions in veto-necessity.md.

The conclusion held; two supporting claims did not. Article IX was found not to be independent of the determinacy assumption — both key on whether the approval settles the rendering — and the theorem was found not to be agent-relative, because X.1.2's grammatical subject is Approval, not the actor, so it binds every principal equally. The earlier assumption that the implementer must be the AI is withdrawn as unnecessary.

The result was then refuted on review (veto-necessity.md §6): Lemma A′ establishes only a one-step claim, while the theorem quantified over all continuations, and a continuation exists — approve, then a further amendment supplying determinacy, then enact. Both branches are progressing; they differ in cost, not in kind. The veto survives as a preference, not a necessity.

One property the state model could not represent, now visible: the current execution is not lawful — it contains two ledger edits made while blocked. Under Article 0.2 that creates a repair obligation rather than nullifying anything, but a model that examines only the current configuration cannot see that the history reaching it was defective.