# Stating an invariant > This section covers how an invariant is written down so that something can object when it breaks. Page: Methodology · Collaborate Canonical: https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant This section is stop 80 of 102 in the learning route. Previous: [41 - A turn never ends to wait](https://banes-lab.com/disciplined-methodology/collaborate/a-turn-never-ends-to-wait.md). Next: [01 - Orchestration as declared structure](https://banes-lab.com/pag/orchestration/declared-structure.md). It builds on [38 - Coordination is software](https://banes-lab.com/disciplined-methodology/collaborate/coordination-is-software.md), [32 - Counting copies](https://banes-lab.com/disciplined-methodology/verify/counting-copies.md). This section covers how an invariant is written down so that something can object when it breaks. A topology relies on invariants, and an invariant it relies on without stating cannot be told apart from a property a reader happened to infer. Stating one is [design by contract](https://banes-lab.com/records/arch/design-by-contract.md) for a collaboration, where the preconditions and postconditions belong to the parties. The test is not whether the invariant is true, but whether anything would disagree if it stopped being true. A stated invariant fills the four slots shown in [G1·a four slots](https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant-panel-a). A lifetime has the three axes shown in [G1·b three axes](https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant-panel-b) and typed in [G1·c a lifetime declaration](https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant-panel-c), and a relation between two states needs the two readings shown in [G1·d two readings](https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant-panel-d). The same four slots appear for a declared workflow under [orchestration invariants](https://banes-lab.com/pag/orchestration/orchestration-invariants.md) on the grammar page. ### Property, set, parties, objector An unstated invariant is not a gap in the documentation but a defect in every claim that rests on it. Two documents state opposite versions of one invariant, every mechanism faithfully implements its own version, nothing reports a defect, and the contradiction exists only for a reader who holds both documents in mind at once. Nothing objects when an unstated invariant stops holding, so its first violation goes unnoticed. For this reason I state an invariant with its property, its set, its parties and its objector, or I state it as unheld. The objector is named before the property is relied on, rather than the property being stated alone. In practice, an invariant is written with four parts: the property, in a form that could turn out false; the set it quantifies over; the parties it binds; and whatever would object if it stopped holding. The invariant is delivered in a surface the bound parties receive, because a mechanism that must honour an invariant is the consumer most easily forgotten, being the only one that cannot ask. Where no objector exists, the invariant is stated as unheld, and every derivation that rests on it is marked. To check this, take an invariant the design relies on and name what would disagree if it stopped holding. If nothing would, the invariant is held by circumstance. Stating an invariant does not enforce it. A statement is a claim about the topology, while a check is a mechanism over artifacts, and where one exists without the other, the honest form says which. An invariant held by a tool holds only as long as every party uses the tool, and a path around the tool by hand is invisible to everything. The contradicted invariant is the failure that no single check can see, so the unit of checking is the set of statements rather than any one statement. An invariant is restated wherever a party needs it, because delivery requires that, and every restatement is a copy that can disagree. Adding a statement therefore adds an obligation to re-derive the whole set whenever the invariant changes, starting with the copies delivered most often. ### A lifetime is three axes A lifetime has three independent axes, and describing it in one word makes the other two impossible to state; [immutability](https://banes-lab.com/records/arch/immutability.md), for example, is a single value on one of them. Retention says what ends a piece of content. Mutability says whether a statement that has landed may be rewritten, and by whom. Removal authority says who may take content out. None of the three can be derived from another, and a topology that runs more than one kind of surface has surfaces that differ on each axis independently. The axis a one-word description drops first is removal authority, because a reader assumes it follows from retention. It does not: keeping content and forbidding its removal are separate claims, and a mechanism that faithfully implements the first can still remove content. Each axis takes its value from a closed set, which is what makes the declaration something a check can read rather than a sentence. ### Two states need two readings A property that is a relation between two states cannot be enforced by a check that looks at only one of them. Presence, shape, membership and conformance can be decided from a single reading, through the [structural](https://banes-lab.com/records/reason/node-ana-structural.md) lens. A rule that content may grow but not shrink, be corrected but not removed, or advance but not retreat is a [happens-before relationship](https://banes-lab.com/records/arch/happens-before-relationship.md), seen through the [temporal](https://banes-lab.com/records/reason/node-ana-temporal.md) lens, and it can be decided only from two readings. A required section is enforced as it goes from empty to full, but nothing notices when it goes from full to empty, and a stricter single-state check has exactly the same blind spot. The repair is to change the number of readings: the prior state is kept, the set it was taken over is recorded, and the two are compared. The comparison has three results rather than two, because a comparison across differing sets refuses to compute, and a refusal is the safe direction when the alternative is a false accusation. ### Declared as data Declared as data, a lifetime takes the form shown in [G1·c a lifetime declaration](https://banes-lab.com/disciplined-methodology/collaborate#stating-an-invariant-panel-c). Each axis is a literal tuple, and the field type is derived from it, so a value outside the closed set fails to compile instead of resolving as a fourth state that was never declared. A surface is a key and its lifetime is one record over the three axes, so a check joins on the axis name and reads the value. A region declares only where it differs from its file, naming the span it covers, the lifetime it carries and the reason, and that limit is what keeps the declaration small enough to count. A seed names which live surface a template creates, so the template declares a lifetime for an instance rather than for itself, and a seed pointing at an undeclared surface is a compile error rather than a citation that resolves to nothing. The values have no order and none is a default. A surface that declares nothing is undeclared, which is a state distinct from every value, and treating the two as the same would make an unmeasured surface impossible to tell apart from a measured one. G1·a four slots ```mermaid flowchart TB invariant["A stated invariant"] property["The property · in a form that could be false"] set["The set it quantifies over · never a verdict beyond its range"] parties["The parties it binds · delivered in a surface they receive"] objector["The objector · a check, a refusal, a comparison, a party that would notice"] unheld["Or stated as unheld · and the derivations above it marked"] invariant --> property invariant --> set invariant --> parties invariant --> objector invariant -. no objector .-> unheld ``` G1·b three axes ```mermaid flowchart TB surface["A surface's lifetime"] retention["Retention · what ends a piece of content"] mutability["Mutability · whether a landed statement may be rewritten, and by whom"] removal["Removal authority · who may take content out"] word["One word · true of every surface and sufficient for none"] surface --> retention surface --> mutability surface --> removal surface -. collapsed to .-> word ``` G1·c a lifetime declaration ```typescript export const RETENTION = ["accumulating", "current-truth", "discharged", "computed"] as const; export const MUTABILITY = ["append-only", "owner-rewritable", "frozen"] as const; export const REMOVAL = ["none", "author", "handler", "producer"] as const; export interface Lifetime { readonly retention: (typeof RETENTION)[number]; readonly mutability: (typeof MUTABILITY)[number]; readonly removal: (typeof REMOVAL)[number]; } export interface LifetimeRegion { readonly name: string; readonly span: "item" | "field" | "row" | "column"; readonly lifetime: Lifetime; readonly why: string; } export interface LifetimeDeclaration { readonly declared: Readonly>; readonly regions: Readonly>; readonly seeds: Readonly>; } export const lifetime: LifetimeDeclaration = { declared: { "": { retention: "current-truth", mutability: "owner-rewritable", removal: "handler" }, "": { retention: "accumulating", mutability: "frozen", removal: "none" }, "": { retention: "computed", mutability: "frozen", removal: "producer" }, }, regions: { "": [{ name: "", span: "field", lifetime: { retention: "accumulating", mutability: "owner-rewritable", removal: "author" }, why: "" }], }, seeds: { "