Microcosm
This page

The system

Doctrine

The laws Microcosm is built under and held to: what a result must carry before it counts, what permits a change, how long a fact stays current, and what a page like this one may inherit from the source beneath it.

Doctrine is how Microcosm keeps its behaviour inside what its evidence can carry. Each law exists because some shortcut once looked reasonable: trusting a label because it was written down, a key because it was held, a cached answer because its name had not changed, a quiet dashboard because nothing reported red. The doctrine is those lessons made binding, and it runs in both directions; the components are written under the laws, and the laws are revised against what the components turn out to do. A result counts only when the material it came from is named and a separate check can rebuild it, and what the result may claim stops where that check stops. The deciding check stays small enough to read and rerun, while the thing that produced the answer, however capable, waits outside. Missing evidence blocks; an unsearched space stays unknown, and unknown is a different verdict from refuted. A number describing live state carries the time it was read, the basis it was read from, and the route to read it again. A stored result may be reused while the content beneath it is unchanged; once that content moves, a familiar name earns nothing. Permission is derived for each specific action from policy, proof, and the present state of the world. A change lands once its way back is declared, or its point of no return is stated in advance. Origin and travel limits ride with material across every boundary, so nothing becomes publishable merely by reaching a public page. Generated views, this page among them, sit below the source they are drawn from; and what Microcosm says about Microcosm is held to the same floor, which is why the cards below spend as many words on limits as on laws.

What doctrine contains

Doctrine decides what everything else is allowed to assert. A standard constrains, a validator runs, a page projects; doctrine sits before all three and fixes what each may claim in the first place. It carries no executable authority of its own, and that is deliberate: a law binds only through the grammars, checks, and records downstream that enforce it. The layer is built from six kinds of object, three that govern what the system may say and three that explain and compress it.

Governingexpanded below

Decide what the system may say.

AxiomsRoot laws of what must hold, admitted rather than proven.
PrinciplesThe operating move an axiom becomes at a boundary.
Anti-principlesThe named shortcuts the system refuses.

Explanatoryin reference

Name and compress the system.

ConceptsVocabulary boundaries shared across the system.Reference
MechanismsCheckable transformations the system can run.Reference
Paper modulesLong-form explanations of a component or a mechanism.Open

This page expands the governing side: axioms, principles, and anti-principles. The explanatory side lives in the reference layer: concepts, mechanisms, and paper modules.

Every component is explained by one paper module and exercised through at least one mechanism. Axioms and principles attach wherever their source rows say they apply, not once per component; the explanatory objects name and describe without raising the strength of what they describe.

The operating loop

Every claim faces the same sequence of questions, whether it is a card, a count, an import, a route, or this page. A missing answer is itself an answer.

  • Claim. What is actually being asserted, stated plainly enough to test.
  • Basis. The exact bytes or rows the claim was computed from.
  • Checker. Which check decides it, and how much of the question that check really covers.
  • Ceiling. The claim is held no stronger than that check, across every dimension of evidence at once.
  • Authority. Whether the action is permitted by policy, proof, and current state, derived at the moment of acting; holding a key is one input to that derivation.
  • Provenance. Where the material came from and how far it is allowed to travel.
  • Freshness. Whether a live value still holds, and how it is re-derived once it does not.
  • Effect. Whether a write is scoped, ordered, and reversible, or honestly declared irreversible.
  • Projection. Whether a generated view stays below the source it draws from.

The sequence ends in a pass or in a typed refusal that names the question that failed. The refusal is the part worth watching: it is where the system tells you what it will not stand behind. Axioms are what let the loop travel, since they hold everywhere; principles aim the same questions at the boundary in front of you.

Admission is not support

An axiom is admitted as law: imposed, the way a constitution is imposed, and exempt from proof. Whether an axiom is witnessed, supported, or strong is a different kind of statement, computed from named checks or withheld; admission alone shows neither enforcement nor completeness. Keeping the two apart is what stops a system believing its own labels, and the separation is itself an instance of the first law: the claim that an axiom holds passes the same floor as any external claim.

Support attaches to obligations, the specific requirements an axiom's formal clause names, and to nothing broader. A principle inherits authority through the obligations it actually operationalises; naming its axiom transfers none. A witness component or a negative case is an input to the computation rather than support in itself, and a new example raises support only when it covers an obligation that had none. A passing example repeated under the same basis is inert.

What a claim may carry is the component-wise meet of eight dimensions: evidence class, checker scope, provenance, freshness, domain scope, negative-case status, authority scope, and projection scope. The weakest covered dimension sets the whole, so a strong checker cannot carry a claim across stale freshness or an unowned scope. A single rank would hide seven of the eight; where a rank appears on this site, it names the one dimension it discloses and stops there.

Positive support and anti-axiom rejection are tracked as separate axes. It is one thing for the right thing to have happened; for a result to read as strong, the tempting wrong thing has to have been tried and refused, and that refusal mapped to its specific obligation rather than inferred from a passing happy path. Until the mapping is verified, the system records the rejection as unproven and says so.

The root constraints

Twelve axioms, grouped by the problem each one governs. Open a card and the same law is stated several ways at once: a plain reading, an analogy with the exact place it stops, a formal clause with every symbol glossed, what the law governs, requires, and refuses, a worked example, the tempting mistake, and the limit of what none of this establishes. The repetition is deliberate. Like the plan, elevation, and section of an engineering drawing, the representations fix one object from different sides; each answers questions the others cannot, and the part is machined from the set rather than from any single view. A reader stops at whichever rendering carries them, a machine reader takes the stack whole, and the build refuses any card whose symbols and formula disagree or whose analogy never names where it breaks.

Claim admissibility

When a claim is allowed to count, and who decides.

AX-1Derivation before assertionA claim is admissible only if it carries a basis, a derivation certificate, and a checker that accepts it; a bare assertion sits at the bottom of the evidence order, however confidently it is stated.

In plain termsA result only counts when the inputs it came from and an independent check can reproduce it. A confident statement on its own is worth nothing.

AnalogyA sports scoreboard is not trusted just because it shows a number. The game log has to list the plays that add up to that score.the claimis likethe number on the scoreboardthe inputs the claim was computed fromis likethe plays recorded in the game logthe checker that recomputes itis likeadding up the plays in the game logWhere the analogy breaksThe game log shows that a score can be recomputed; it does not make a score true in every possible game, and one matching log is bounded evidence the whole season was scored correctly.

Why it mattersIt lets the system treat 'a model said so' or 'a record is labelled passed' as zero evidence until something independent recreates the answer.

Potential misreadingThat a checked result is therefore certain. The check bounds how much the result can claim; it does not bless it as true everywhere.

Microcosm starts from the position that an output is worth nothing until it can be reconstructed. A claim over some basis is admissible only if it arrives with a derivation certificate and a checker that recomputes the verdict and accepts it, and the strength the claim may carry is capped at the strength of that check. The direction matters: the check is what admission requires, not a seal that makes the claim true. A confident sentence, a repeated fixture label, or a model's own answer sits at the bottom of the evidence order until something independent rederives it. This is the floor the rest of the doctrine stands on: it is what lets the system treat "a model said so" and "a record is labelled passed" as zero evidence rather than weak evidence.

Formal statementadm(φ, B)  ⇒  ∃  c, K. K(B, c, φ) = accept  ∧  strength(φ) ⊑ strength(K(B, c, φ));   bare(φ) ⇒ strength(φ) = ⊥A claim over a basis is admissible only if some certificate and checker accept it, with the claim's strength capped by the strength of that check; a claim that arrives with no certificate sits at the bottom of the evidence order. The condition is necessary, not sufficient: passing a check is what admission requires, never a promise that the claim is true.adm(φ, B)the claim is admissible over its basisφa claimBthe basis it is computed fromca derivation certificateKa checker that recomputes the verdictstrengththe position a claim or a check holds in the evidence orderno stronger thanbare(φ)a bare assertion: the claim presented with no certificatebottom: the lowest position in the evidence order
GovernsWhen a stated result is allowed to count as evidence at all.
RequiresA basis, a derivation certificate, and a checker that recomputes the verdict and accepts it.
RefusesAn asserted label treated as truth.

In practiceA replay reads a fixture that declares a monitor caught scheming, recomputes the verdict from the underlying trace, and rejects the run when the declared verdict does not derive from the lower-level evidence.

Enforced inAgent Sabotage Scheming Monitor Replay Belief State Process Reward Replay

The tempting mistakeA page prints "passed" because a result record's title says so, with nothing recomputing the verdict from the evidence beneath it.

GroundsP-1 P-2

Guarded byAP-1 AP-12 AP-15

Scope limitOne checker catching one class of label echo does not establish a claim true in general, and admitting this law is separate from how well it is witnessed: support is computed obligation by obligation, elsewhere. A passing check caps what a claim may say; it does not bless it.

Source JSON · Show relationships →

AX-2Kernelized verificationTrust is decided by a small checker over the certificate a producer emits, so the producer can be large and untrusted while the part that accepts its output stays small enough to inspect and rerun.

In plain termsA claim counts as trusted only when a small, separate check re-derives it from the evidence presented with it. The thing that produced the answer never approves its own answer, however capable it is. A claim is only as strong as what that small check actually covered.

AnalogyAt a secure building, the person who printed a visitor pass does not get to wave themselves in; a small front desk checks the pass against its own list and decides entry, and only what the desk actually checks counts.the small separate checker K that decidesis likethe front desk that checks the pass and decides entrythe producer that emitted the certificate, kept outside the trusted baseis likethe person who printed the pass, who cannot approve their own entrythe certificate the checker readsis likethe pass presented at the deskclaim strength is capped by the checker's scope, not the producer's reputationis likeyou get in only as far as what the desk actually verifies, not how official the pass looksWhere the analogy breaksThe desk shows that the pass-printer cannot self-admit and that trust sits with the checker; it does not establish that the desk's list is complete, that every visitor was checked correctly, or that one admitted visitor means the whole building's access is sound.

Why it mattersIt keeps the part you have to audit small and fixed even as the systems generating answers grow larger and faster, so a clever or broken producer cannot quietly widen what gets accepted.

Potential misreadingThat a powerful, confident producer can be trusted to vouch for its own output, so the small separate checking step is optional once the output looks authoritative.

AX-2 says where the trust lives, not just that a check happened. The thing allowed to decide a claim is a small, separately maintained checker K that reads a certificate; the producer that emitted the certificate, however large, fast, or capable, is outside the trusted base and gets no vote on its own output. This is the architecture that makes AX-1's floor cheap to believe: shrinking the decider to a small K means the part you have to audit stays small even as the producers around it grow, so a clever or broken producer cannot quietly widen what counts as accepted. The bite is that confidence does not transfer from producer to verdict; an answer is trusted to the extent a small checker rederived it, and the strength of any claim is capped by the scope of that checker rather than the reputation of whatever generated the certificate.

Formal statementtrust(φ)  ⇒  ∃  c. K(c) = accept  ∧  Kproducer(c)  ∧  small(K)A claim is trusted only when some certificate is accepted by the designated checker, the checker is not the thing that produced the certificate, and the checker is small enough to audit and rerun.trust(φ)the claim is trustedφa claim seeking trustca certificate a producer emitsKthe small checker that decidesproducer(c)the component that generated c, kept outside the trusted basesmall(K)the checker is small enough to audit and rerun
GovernsWhere trust is concentrated when a claim is decided: in the small checker, not the producer.
RequiresA small checker that decides over a certificate, kept separate from the producer that emitted it.
RefusesProducer trust replacing checker trust.

In practiceThe certificate kernel lab keeps the part that emits certificates separate from a small checker that decides them, and a companion Lean witness compiles a tiny example through a real verifier whose kernel rejects an invalid proof body rather than trusting that the producer meant well.

Enforced inCertificate Kernel Execution Lab Formal Math Lean Proof Witness Verifier Lab Kernel

The tempting mistakeA generator's own confidence is taken as the verdict, so a large producer effectively certifies itself and the small checking step is skipped because the output looked authoritative.

GroundsP-3

Guarded byAP-2 AP-15

Scope limitA small checker accepting one certificate proves only that this certificate passed this checker; it does not establish the producer is correct in general, that the checker covers every claim the producer can make, or that the kernel is itself bug-free. The scope of the check is the ceiling, and this reader illustration carries no support weight on its own.

Source JSON · Show relationships →

AX-7Typed partiality and refusalA computation that cannot honestly produce a value returns a typed refusal carrying its reason, never a plausible-looking number that means nothing.

In plain termsA calculation may return a real number only when the conditions it needs actually hold. When they don't, it must hand back a clearly labelled refusal that names the reason and the evidence, never a quiet number or a blank that the next step reads as an answer.

AnalogyA cash machine that can't complete a withdrawal prints a stated decline reason and gives you nothing, rather than spitting out some arbitrary amount of cash that you'd carry off as if it were correct.the precondition that must hold for a real resultis likethe conditions the machine needs to launch cash, like a valid balance and a reachable accountOk carrying a value when the precondition holdsis likethe machine dispensing the requested amount when everything checks outa typed refusal carrying a reason and evidenceis likethe printed decline notice naming why it stoppednever a silent number or NaN leaking downstreamis likenever handing out an arbitrary stack of cash that you'd treat as a real withdrawalWhere the analogy breaksThe cash machine shows that a failed operation must decline with a reason instead of emitting a stray figure; it does not establish that every operation in the system declines this way, and untested failure paths can still leak a bad value rather than a clean refusal.

Why it mattersIt means a missing input or an out-of-range condition shows up as a visible, routable gap instead of a plausible-looking figure that a later page prints as a genuine result.

Potential misreadingThat a number coming out the end means the conditions were fine, so a calculation that quietly produced a value can be treated as a valid answer without checking it had grounds to run.

AX-7 refuses the most common way numerical code lies: producing a plausible-looking value where its preconditions do not actually hold. Microcosm requires a partial computation g to be totalized into a Result, so it returns Ok(y) only when a declared precondition Pre(x) is met, and otherwise returns a Refusal that names the reason and carries the evidence behind it. The refusal is the load-bearing half, because a number with no precondition check and no failure path is indistinguishable from a number that happens to be wrong; a NaN, an out-of-range horizon, or a missing dependency must surface as a typed object the caller can route, not leak downstream as a figure that reads as a result. This connects directly to the evidence model: a refusal with a reason is admissible information, whereas a silent number is a claim with no basis beneath it, so AX-7 is what lets the upstream admissibility floor see a gap instead of inheriting a fabricated value.

Formal statement∀  x. (Pre(x) ⇒ ∃  y. g(x) = Ok(y))  ∧  (¬ Pre(x) ⇒ ∃  r, e. g(x) = Refusal(r, e))For every input: when the declared precondition holds, the computation returns Ok carrying some value; when it does not hold, the computation returns a typed Refusal carrying a reason and the evidence behind it. Both branches are total; there is no third, silent outcome.ga partial computation, totalized into a Resultxan input to the computationPre(x)the declared precondition on input xOk(y)a successful result carrying value yRefusal(r, e)a typed refusal carrying a reason r and evidence e
GovernsWhat a partial computation is allowed to return when its precondition does not hold.
RequiresA declared precondition for the Ok path and a typed Refusal carrying a reason and evidence on every other path, including missing dependencies and undefined values.
RefusesAn inadmissible number or silent NaN returned where no precondition was checked.

In practiceThe finance forecast evaluation spine returns a typed refusal naming the reason when a forecast horizon is at or above the sample size, or when the statistics dependency needed for a t-distribution is unavailable, instead of returning a number computed outside its domain.

Enforced inFinance Forecast Evaluation Spine Corpus Readiness Mathlib Absence Gate

The tempting mistakeA statistics routine divides by a sample size that is too small and returns the resulting NaN as if it were a score, and a downstream page prints it as a real forecast number.

GroundsP-8

Guarded byAP-6

Scope limitReturning typed refusals at these named computations does not establish that every partial path in the system is totalized. It covers the declared preconditions and dependency gaps that are actually checked; uncovered partial functions remain a gap rather than a guaranteed refusal.

Source JSON · Show relationships →

Authority and effect

What permits an action, and what a change has to carry.

AX-3Authority by derivation, not possessionPermission to act is derived from dereferenced policy, proof, and current world state; holding a token, a role, or a session is not authority by itself.

In plain termsHolding a key or a token is not permission. Permission is worked out for this specific action, at the moment you act, from the rules and the current situation.

AnalogyA hotel key card opens one room for the nights you paid for. Holding a card does not mean every door should open for you.the standing account secretis likeholding the key cardauthority derived per effect from policy and world-stateis likethe lock checking this door, tonight, against the bookingWhere the analogy breaksThe card-and-lock picture compresses tokens, policy, proof, and the live world-state into one swipe; real authorization weighs all of those, and the analogy does not show that detail.

Why it mattersIt closes the confused-deputy hole, where a component with broad standing power is talked into using it on someone else's behalf.

Potential misreadingThat a valid account secret is enough. The account secret is only one input; permission still has to be derived for the exact action.

Microcosm refuses to treat a account secret as the thing that grants power. Authority for a subject to cause an effect is computed at the point of action from the tokens actually dereferenced, the governing policy, the proof references, and the current world-state, so that ambient identity, a long-lived key, or simply having a tool reachable confers nothing on its own. This is the claim and evidence model applied to action rather than to assertion: just as a label is bottom evidence until something recomputes it, a account secret is bottom authority until a derivation over policy and proof admits the specific effect. It bites hardest at the confused-deputy boundary, where a component holds broad standing power and is steered into exercising it on someone else's behalf; here the bound on what may happen has to be derived per effect from declared scope and approval, not inherited from whatever the holder could in principle do.

Formal statementauth(u, e) = F(deref(tok), policy, proof, world);   holds(u, cred)  ∧  deref(tok) = ∅  ⇒  auth(u, e) ≠ grantAuthority for a subject to cause an effect is the output of the authorizer's derivation over the dereferenced tokens, governing policy, proof references, and current world-state; a standing account secret whose tokens dereference to nothing grants nothing. Possession is one input to the derivation, never the derivation.auth(u, e)the authority decision for subject u to cause effect euthe subject requesting an effectethe effect to be authorizedFthe authorizer's derivation over its inputsderef(tok)the tokens actually dereferenced, not merely presentedpolicythe governing policyproofthe proof references the authorizer derives overworldthe current world-stategrantthe authorizer's derived decision to permit the effectholds(u, cred)the subject merely possesses a standing account secret
GovernsWhether a subject may cause a given effect, decided per effect at the point of action.
RequiresA derivation over dereferenced tokens, policy, proof references, and world-state, plus declared scope, approval, and side-effect records bounding any tool effect.
RefusesA standing account secret treated as authority.

In practiceThe governed-mutation authorizer dereferences proof, policy, and rollback evidence for each requested change and refuses the mutation when authorization does not derive from that evidence, so a standing account secret alone cannot drive the effect.

Enforced inProof Derived Governed Mutation Authorization MCP Tool Authority Replay

The tempting mistakeA tool call is allowed to write because the caller holds a broad token and the tool is reachable, with no derivation bounding the effect to a declared scope and approval.

GroundsP-4 P-16 P-18

Guarded byAP-2

Scope limitTwo authorizers deriving authority for their own effect classes does not establish that every effect in the system is so governed, and these witnesses are inputs to a separately computed support verdict, never support themselves. This reading illustrates the rule and establishes no authority the source does not already carry.

Source JSON · Show relationships →

AX-9Compensable transactional effectsAn effect needs a declared scope, ordering, and either a compensator or an explicit irreversible boundary; multi-step effects land as a transaction under compare-and-swap and single-writer constraints.

In plain termsA change to the world only counts as done if there is a stated way to undo it, or a clear note saying it can never be undone. A multi-step change only goes through if the starting point it expected is still there and nobody else is changing the same thing at the same time.

AnalogyA money transfer between accounts only completes if the bank can either reverse it or has marked it as final and non-refundable, and a multi-leg transfer only proceeds when the balance it started from has not changed and no second transfer is touching the same account.an effect treated as landedis likea transfer treated as completeda declared compensator that can reverse the effectis likethe bank's ability to reverse the transfera declared irreversible boundaryis likethe transfer marked final and non-refundablethe compare-and-swap expected-parent check still holdingis likethe starting balance being unchanged when the leg runsthe single-writer constraint on the pathis likeno second transfer touching the same account at the same timeWhere the analogy breaksThis only describes when a change is allowed to be called done; it does not show that every change in the system can be undone, and one transfer that passed its checks does not establish that all transfers are reversible or collision-free.

Why it mattersIt stops a half-finished change from being silently treated as complete, which is how a system ends up in a state nobody chose and nobody can walk back.

Potential misreadingReading this as a promise that everything is reversible. It actually allows changes to be marked permanently final too; the rule is that the change must declare which one it is, not that undo is always possible.

Microcosm treats a write as inadmissible until there is a way back from it or an explicit declaration that there is not. An effect counts as landed only if it carries a compensator that can reverse it or a declared irreversible boundary that marks the point of no return, and a multi-step effect lands as a saga whose every step compares against the head it expected and finds a single writer holding the path. The failure this refuses is the half-completed write: a sequence that succeeds partway, hits a moved head or a second writer, and leaves the world in a state nobody declared and nobody can undo. This ties back to the admissibility floor, because a landing that cannot be recomputed against its expected parent or rolled back is an effect asserting its own success with no check behind it, which is exactly the bare assertion the evidence order puts at the bottom.

Formal statementland(e)  ⇒  (comp(e) ∨ irrev(e))  ∧  (multi(e) ⇒ parent(e) = headwriters(path(e)) ≤ 1)An effect may count as landed only if it declares a compensator or an irreversible boundary; and a multi-step effect lands only while the parent it expected still matches the head and at most one writer holds its path. Reversibility is not promised; what is required is that every effect declares which kind it is.land(e)the effect e is treated as landedcomp(e)a declared compensator that can reverse eirrev(e)a declared irreversible boundary for emulti(e)the effect e is a multi-step effectparent(e) = headthe compare-and-swap expected-parent check still holdswriters(path(e)) ≤ 1the single-writer constraint on e's path
GovernsWhen a mutation is allowed to count as landed.
RequiresA declared compensator or an irreversible boundary, and for multi-step effects a compare-and-swap expected-parent check plus a single-writer constraint on the path.
RefusesA blind irreversible write.

In practiceThe mission transaction work spine lands a multi-step effect only when its expected parent still matches the head, so a run whose head advanced underneath it fails with a parent-mismatch rather than overwriting the newer state.

Enforced inMission Transaction Work Spine Durable Agent Work Landing Replay Concurrency Mission Control

The tempting mistakeA step writes to a shared path and is treated as landed because the call returned, with no expected-parent check and no single-writer constraint, so two concurrent writers interleave and the final state matches neither.

GroundsP-10 P-16 P-17 P-18

Guarded byAP-8

Scope limitBlocking parent-mismatch and same-path conflict on these named paths does not establish every effect in the system is compensable or every concurrent write is serialized. The legacy strong label is not a computed support verdict, and the routing registry still records that mapping these negative cases to a full rejection of the blind irreversible write remains unverified.

Source JSON · Show relationships →

Identity, time, and reuse

What makes a result the same result, and for how long.

AX-4Content-addressed determinismA derived artifact's identity is the hash of its actual inputs, so equal inputs may be reused, any drift in the basis forces a recompute, and a missing basis yields no result.

In plain termsA reused or cached result is the same as before only when the exact inputs it was built from are the same, not when it merely shares a name or location. If the inputs changed, it must be rebuilt; if the inputs can't be found, there is no result at all rather than an optimistic hit.

AnalogyA pharmacy refills a prescription only when it matches the exact current doctor's order, not just because your name is on file; if the order changed it must be re-issued, and if no order can be found you get nothing rather than last time's pills.the derived artifact identified by the digest of its declared basisis likethe medication identified by the exact current order it was filled fromequal basis licenses reuseis likea matching, unchanged order lets the same refill be dispensedbasis drift forces recomputeis likea changed order forces a re-issued prescription, not the old onea missing basis is bottom, not a hitis likeno findable order means you get nothing, not a guess from historymatching name or path is not matching basisis likeyour name being on file is not the same as a matching current orderWhere the analogy breaksThe pharmacy shows that identity must come from the exact inputs and not the name on file; it does not establish that every counter in the system checks orders this way, and it leaves unaddressed the open coverage gap where some reuse paths are not yet keyed to their inputs.

Why it mattersIt stops a stale or tampered result from passing as fresh just because a name or path matched, which is how a poisoned cache or an out-of-date view sneaks through dressed as a performance win.

Potential misreadingThat a matching name or filename is enough to safely reuse a stored result, so re-checking the underlying inputs is just wasted work.

AX-4 fixes what a cached or reused result is allowed to mean. A derived artifact is a function of a declared content basis, and its identity is the digest of that basis, so two results are the same only when the inputs they were computed from are the same, not when they happen to share a name or a path. Equal basis licenses reuse or coalescing; any drift in the basis forces a recompute or a refusal; and a basis that cannot be resolved is bottom rather than an optimistic hit. This is the same admissibility floor as AX-1 pushed down to the build and cache layer: reusing an output because its name matches, while the inputs underneath have changed, is the label-echo failure dressed as a performance optimization, and it is what lets a stale projection or a poisoned cache pass for fresh.

Formal statementa = f(B)  ∧  id(a) = H(B);   reuse(a) ⇒ H(B') = H(B);   H(B') ≠ H(B) ⇒ recompute(a);   missing(B) ⇒ reuse(a) = ⊥A derived artifact is a function of its declared basis and is identified by the digest of that basis; reuse is permitted only while the current basis digest equals the stored one; digest drift forces a rederivation; and a basis that cannot be resolved yields no result at all, never an optimistic hit.aa derived artifactfthe deterministic derivation from basis to artifactBits declared content basis (the inputs it is computed from)id(a)the artifact's identityH(B)the digest of the basis that serves as that identityreuse(a)serving the stored artifact instead of recomputingB'the current basis at reuse timerecompute(a)rederiving the artifact rather than serving the stored copymissing(B)the declared basis cannot be resolvedbottom: no result, rather than a hit
GovernsWhen a cached or reused result is allowed to stand in for a fresh derivation.
RequiresA declared content basis, an identity that is the digest of that basis, and a digest comparison that gates reuse against recompute.
RefusesCaching by name across drift.

In practiceThe source-import protocol brings material in by manifest and digest, and refuses to reuse an imported copy when the source digest no longer matches, so a changed input cannot pass as an unchanged result.

Enforced inSource Projection Import Protocol Durable Agent Work Landing Replay

The tempting mistakeA pipeline serves a cached output because the requested name matches a prior run, while the inputs that produced it have since changed underneath the key.

GroundsP-5 P-14 P-15 P-17

Guarded byAP-4 AP-12 AP-13 AP-17

Scope limitRefusing a digest mismatch at the named import and work-landing surfaces does not establish that every reuse path in the system is basis-keyed. One required part of this axiom, a stable freshness-basis mismatch code for work landing, is recorded as open unfinished coverage rather than claimed, and admission of this axiom as a root law is independent of whether it is witnessed, strong, or complete.

Source JSON · Show relationships →

AX-10Temporal validity and freshness contractsA claim about live state is a cached read, valid only while it carries its value, its as-of time, its basis, and a way to re-derive it once it goes stale.

In plain termsA number about something that keeps changing is just a reading taken at a moment, not a permanent fact. To be usable later it has to say when it was read, where it was read from, and how to read it again.

AnalogyAn electricity meter reading is only useful on a bill if it records the date it was taken, which meter it came from, and how to take a fresh reading; the bare number alone tells you nothing about today's usage.a claim over live, moving stateis likea number describing ongoing electricity usagethe value assertedis likethe figure shown on the meterthe as-of time the value was takenis likethe date the reading was recordedthe basis the value was read fromis likewhich meter the reading came fromthe rule that recomputes the valueis likethe procedure for taking a fresh readingWhere the analogy breaksThis only covers when a live number can still be stated as current; it does not establish that any particular reading is right now, and a reading that carries its date is not therefore fresh today.

Why it mattersIt keeps a number that was true once from quietly being read as if it were still true weeks later, after the thing it measured has moved on.

Potential misreadingThinking that attaching a date and a source makes the number current. It only makes the number checkable; whether it still holds has to be read again from the source.

A number that describes a moving system stops being true the moment the system moves, so Microcosm treats every claim over live state as a cached read rather than a fact. To be admissible such a claim has to carry four things: the value, the time it was taken, the basis it was read from, and the rule for recomputing it; a bare value with none of these is a frozen snapshot wearing the costume of a current reading. This is where the evidence model meets time: the admissibility floor decides whether a claim counts at all, and this axiom adds that a live claim's strength decays with its own staleness unless its declared basis still holds. It bites hardest on the things that look most authoritative, the running counts and dashboard totals, because those are exactly the values a reader assumes are fresh.

Formal statementvalid(φ, t')  ⇒  φ = ⟨ v, t, B, ρ ⟩  ∧  (holds(B, t, t')  ∨  v = ρ(B))A live-state claim may still be stated as current at a time of use only when it carries its value, its read time, its basis, and its rederive rule, and either the basis is unchanged between reading and use or the value has been freshly recomputed by that rule.valid(φ, t')the claim may still be stated as current at use time t'φa claim over live statevthe value assertedtthe time the value was readt'the later time the claim is usedBthe basis the value was read fromρthe rule that recomputes the value from the basisholds(B, t, t')the declared basis is unchanged between the read and the use
GovernsWhen a value read from live state is still allowed to be stated as current.
RequiresA value carrying its as-of time, its basis, and a rederive rule, with invalidation or recomputation once that basis no longer holds.
RefusesA frozen live count stated without a refresh basis.

In practiceThe fact-claim audit flags a volatile numeric claim that carries no freshness binding as a stable blocking code, so a live count cannot be published as if it were still current without declaring when it was taken and how to recompute it.

Enforced inDoctrine Fact Claim Audit Live Source Drift Bundle

The tempting mistakeA page prints a running total once and leaves it on display for weeks, with no as-of time and no rule to recompute it, so a stale snapshot reads as a live figure.

GroundsP-11

Guarded byAP-4 AP-9

Scope limitBlocking unbound volatile numbers does not make any specific number current or correct, and it does not establish that staleness is caught everywhere. The freshness component of this axiom's own ceiling stays an ordered unknown until a source-owned refresh contract exists, so this object names the obligation rather than certifying that it is met.

Source JSON · Show relationships →

Coverage and lattice discipline

How partial knowledge combines without overstating itself.

AX-5Fail-closed monotone latticeA composite's status is the meet of its parts; missing evidence defaults to blocked, and a later stage may lower authority but never raise it without a new derivation.

In plain termsSomething built from parts is only as trusted as its weakest required part. A part with no evidence counts as blocked, not as fine, and a later step can lower trust but never quietly raise it.

AnalogyA plane does not take off because most of the pre-flight checklist passed. One required check left blank keeps it at the gate.the composite is only as trusted as its weakest partis likethe flight is grounded by its one failing checkmissing evidence defaults to blockedis likea blank checklist item counts as not-done, not as doneWhere the analogy breaksThe checklist shows fail-closed status and the weakest-link rule; it does not show that trust here is measured along several separate dimensions at once, not a single pass or fail.

Why it mattersIt makes a gap the safe state, so a launch that finds private-adjacent content or overclaiming language stops instead of shipping.

Potential misreadingThat enough green parts can outvote a blocked one. They cannot; the weakest required part sets the ceiling.

AX-5 fixes the default and the direction of trust so that absence and silence cannot be read as permission. The status of a composite is the meet of its parts, so one blocked or unknown component pulls the whole down and no amount of green elsewhere lifts it back up; a missing witness defaults to blocked, not to a silent pass. The monotone half forbids the quiet upgrade: a downstream stage may demote authority freely, but raising it requires a new derivation under AX-1, never a stage that simply asserts a higher status than the evidence it received. This is the axiom that makes the gap the safe state, which is why a launch step that finds private-adjacent content or overclaiming language stops rather than shipping, and why an uncovered obligation reads as blocked instead of as quietly satisfied.

Formal statementstatus(c) = ⨅pparts(c) status(p)  ∧  ∀  pparts(c). (evidence(p) = ∅ ⇒ status(p) = ⊥)  ∧  (status'(c) ⊐ status(c) ⇒ ∃  d. derives(d, status'(c)))A composite's status is the meet of its parts' statuses; every part with no evidence is blocked; and a later status may exceed the earlier one only when some fresh derivation establishes it.status(c)the trust status of a composite cthe meet (greatest lower bound) taken over the partsparts(c)the parts the composite is built frompa part of the compositeevidence(p)the evidence available for part pbottom: blocked, the default when a part's evidence is absentstatus'(c)a later status proposed for the same compositestrictly higher in the trust order thanda fresh derivationderives(d, status'(c))derivation d establishes the higher status
GovernsThe default status of missing evidence and the direction trust is allowed to move across stages.
RequiresTaking the meet of part statuses, defaulting an unwitnessed part to blocked, and a fresh derivation before any stage raises authority.
RefusesA silent default pass.

In practiceThe launch wording gate runs over the system's own public copy and stops the export when it finds overclaiming language, so a later packaging stage cannot raise the claim above what the evidence beneath it supports.

Enforced inRelease Public Wording Gate Proof Diagnostic Evidence Spine Self Ignorance Coverage Ledger

The tempting mistakeA status board marks a composite green because no part reported a failure, treating the absence of a recorded check as if it were a passing one.

GroundsP-2 P-6 P-15 P-19

Guarded byAP-3 AP-14

Scope limitDefaulting to blocked and refusing silent upgrades does not establish any composite actually correct or complete; it fixes the safe direction of trust, and an obligation with no admissible witness stays blocked rather than becoming true by default.

Source JSON · Show relationships →

AX-6Open-world epistemicsFailing to prove something does not establish its negation; coverage is closed-world only inside a domain the system has declared finite on purpose.

In plain termsNot finding evidence for something is not the same as showing it is false. You can only call an absence a 'no' inside a list you have fully checked; otherwise the honest answer is 'unknown'.

AnalogyNot finding your keys in one drawer only tells you they are not in that drawer. It does not tell you they are gone.the declared finite domain with complete coverageis likethe one drawer you searched all the way throughthe unknown verdict outside itis likethe rest of the house you have not checkedWhere the analogy breaksThe drawer picture works only when the search space is small and fully declared, like one drawer; it does not let you call something false across an open world you never finished searching.

Why it mattersIt stops the system turning 'we did not see a problem' into 'there is no problem', which is how silent failures get signed off.

Potential misreadingThat no evidence means no problem. Outside a fully checked list, no evidence just means not yet known.

Microcosm refuses the cheap move of reading a blank as a no. Failing to prove a claim does not license proving its negation; the most an unproven claim earns is unknown, and unknown is a distinct verdict from refuted. The one case where absence does become a negative is narrow: the domain has to be explicitly declared finite and its coverage has to be complete, so that "nothing found" is backed by "everything was looked at." This is what keeps the system from converting gaps in its own map into false confidence: a missing relation, an unmapped region, or a fact with no cited evidence reads as open and computable, not as settled, and the limit is recorded rather than papered over.

Formal statementscope(φ) ⊆ D  ∧  closed(D)  ∧  covered(D)  ∧  ¬ proven(φ)  ⇒  proven(¬φ);   else verdict(φ) = unknownOnly when a claim ranges inside a domain that is declared finite and completely covered does failing to prove it license concluding its negation; in every other case the verdict on an unproven claim is unknown, never refuted.φa claim under considerationscope(φ)the domain the claim ranges overDa declared domainclosed(D)the domain is explicitly declared finite (closed-world)covered(D)coverage over D is complete, so nothing in it was left unexamined¬ proven(φ)the claim has not been provenverdict(φ)the verdict the system records for the claimunknownthe open-world verdict, distinct from refuted
GovernsWhether an absence of evidence is allowed to count as a negative result, and inside what scope.
RequiresAn explicitly declared finite domain with complete coverage before any closed-world conclusion; outside it, an unproven claim yields unknown rather than its negation.
RefusesAbsence of evidence treated as evidence of absence.

In practiceThe self-ignorance coverage ledger tracks the gap between what has been declared in scope and what has actually been materialized, and forbids the inference that an unmapped region is empty; the open space stays a recorded, computable gap rather than a quiet claim of completeness.

Enforced inSelf Ignorance Coverage Ledger Doctrine Fact Claim Audit

The tempting mistakeA status surface reports a property as clean because a scan returned no findings, without ever declaring the finite domain the scan covered, so silence over an unbounded space is read as a guarantee.

GroundsP-7 P-19

Guarded byAP-5

Scope limitTracking a declared-versus-materialized gap does not exhaust the space of unknown unknowns or prove the unmapped region empty. The open-world unknown it preserves is a coverage state, not a support verdict, and it never certifies that what was not found does not exist.

Source JSON · Show relationships →

Flow and projection

How material and authority move without leaking.

AX-8Provenance propagation and non-interferenceLabels and ceilings travel with data across every boundary, so untrusted material reaches a privileged sink only through a declared transform the sink's policy allows.

In plain termsWhere a value came from, and how far it is allowed to travel, must follow it everywhere. Untrusted material can only reach a sensitive place after passing through a stated cleaning step.

AnalogyAllergen information has to follow an ingredient all the way through the kitchen. A clean-looking label on the final plate is not enough if nobody tracked the nuts.the provenance label and ceiling carried with the valueis likethe allergen tag that travels with the ingredientthe declared transform before a sensitive outputis likethe documented step that removes or contains the allergen before servingWhere the analogy breaksThe kitchen-label picture shows that the tag must travel and be transformed on purpose; it does not capture the full tracing of how information flows and combines, which is stricter than one label.

Why it mattersIt blocks private, provider, or unverified input quietly reaching a public or privileged output just because the final step looked clean.

Potential misreadingThat a clean label at the end shows a clean path. Only a label that actually travelled, with a declared cleaning step, counts.

Trust is not a property of where a value ends up, it is a property of where it came from and what was done to it on the way. Every value carries a provenance class and a ceiling, and those travel with it across every boundary it crosses. Untrusted material, a prompt, a model-output data, or private-adjacent source, may reach a privileged or public sink only through a declared transform whose output the sink's policy admits. The endpoint cannot certify its own cleanliness: the label has to have been carried, not stamped on at the door. This is why a clean-looking final step is not enough, and why the system tracks how far a value may travel rather than just what it currently looks like.

Formal statementy = f(x)  ⇒  label(x) ⊑ label(y);   (xs)  ⇒  label(x) ⊑ policy(s)  ∨  (xTs  ∧  declared(T)  ∧  label(T(x)) ⊑ policy(s))A derived value carries at least the restriction of what it was derived from; and for any flow into a sink, either the value's label already sits within the sink's policy, or the flow passes through a declared transform whose output label the sink's policy admits. The endpoint never stamps the label; the label arrives with the value.xa value entering a flowya value derived from it along the flowfa processing step along the flowsa sink (a public or privileged output)label(x)the value's provenance class and how far it may travelpolicy(s)what the sink is allowed to admitTa declared sanitising transform the flow passes throughdeclared(T)the transform is declared, not stamped at the door
GovernsHow material and its trust label move across boundaries.
RequiresA provenance class and ceiling carried with the value, and a declared transform before untrusted material reaches a privileged sink.
RefusesAn endpoint asserting a clean label without that label having propagated.

In practiceThe prompt-injection replay carries the information-flow policy with the data, so untrusted instructions arriving at a tool call are caught at the boundary instead of trusted because they reached a trusted endpoint.

Enforced inIndirect Prompt Injection Information Flow Policy Replay Source Projection Import Protocol

The tempting mistakeA public page prints a value lifted from a private-adjacent source because the final copy step looked clean, with no provenance carried across the copy.

GroundsP-9 P-14

Guarded byAP-7 AP-12 AP-14 AP-16

Scope limitCatching labelled flows at named endpoints does not establish non-interference across the whole graph. General propagation is bounded by what is actually traced, and the registry records that debt rather than hiding it.

Source JSON · Show relationships →

AX-11Executable grammar before doctrine authorityA rule earns authority by entering a machine grammar with its required fields, result records, and scope boundaries; prose on its own stays a projection that can orient but cannot decide.

In plain termsA rule is only allowed to govern when it passes a fixed format check and comes with the evidence it must produce and a clear statement of what it does not cover. A well-written paragraph on its own is just something to read, not a rule.

AnalogyA customs declaration only clears goods when it passes the required form check, arrives with its supporting paperwork, and states plainly what it does not vouch for; a politely worded letter describing the shipment, however convincing, clears nothing.a doctrine artifact carrying governing authorityis likea declaration that clears the goodsmembership in the executable grammaris likepassing the required customs form checkthe evidence obligations the artifact must carryis likethe supporting paperwork that must travel with itthe declared statement of what it does not establishis likethe declaration's stated exclusions, what it does not vouch forprose held only as a readable projectionis likethe convincing letter that clears nothingWhere the analogy breaksThis only governs whether a rule is allowed to bind at all; passing the format check does not show the rule is complete or correct, and a cleared declaration is not therefore an accurate account of the goods.

Why it mattersIt stops a confident-sounding paragraph from being treated as an enforced rule just because it reads authoritatively, keeping unchecked prose out of the seat of governance.

Potential misreadingAssuming that passing the format check means the rule fully covers its subject. Passing the check admits the rule's shape only; it never certifies that what the rule says is complete.

AX-11 turns the doctrine itself into something the system can execute rather than merely read. A standard, contract, or rule may carry authority only when an executable grammar accepts its form and it arrives with its result record obligations and its own scope boundary attached; a clause that is only well written sits at the level of a projection, not a law. This is what stops a confident standard from governing by rhetoric: the gate decides on the artifact's checkable shape, not its prose, so the same admissibility discipline AX-1 imposes on claims is imposed on the documents that define how claims are judged. The bite is the second negative case as much as the first: passing the grammar admits the artifact's shape and never certifies that the doctrine it expresses is complete, so a grammar pass that is read as coverage is rejected, not rewarded.

Formal statementauthority(d)  ⇒  dL(G)  ∧  obligations(d) ≠ ∅  ∧  anticlaim(d);   otherwise dProjA doctrine artifact carries authority only when an executable grammar accepts its shape and it presents its evidence obligations and its own scope boundary; an artifact failing any of these sits in the projection tier, which can be read but cannot govern.authority(d)the doctrine artifact d carries governing authorityda doctrine artifact (standard, contract, rule)L(G)the language an executable grammar G acceptsobligations(d)the result-record obligations the artifact must carryanticlaim(d)the artifact's declared statement of what it does not establishProjthe projection tier, below authority
GovernsWhether a doctrine artifact may govern, or is only a readable projection of one.
RequiresSign-off by an executable grammar plus carried result record obligations and a declared scope boundary, not well-formed prose.
RefusesProse claiming executable authority.

In practiceThe executable doctrine grammar component accepts a standard only when its shape parses and its result record obligations and scope boundary are present, and rejects a prose standard that asserts authority without that executable form.

Enforced inExecutable Doctrine Grammar Standards Meta Diagnostics

The tempting mistakeA persuasive standard written in prose is treated as binding because it reads authoritatively, with no grammar accepting its shape and no scope boundary or result record obligations carried.

GroundsP-12 P-15 P-17 P-18 P-19 P-20

Guarded byAP-10 AP-13 AP-17

Scope limitA grammar accepting an artifact's shape does not establish the doctrine it expresses is complete or correct; admitting the form is not certifying the coverage, and this reader page is itself a projection that cannot raise the authority of the source it explains.

Source JSON · Show relationships →

Reflexive accountability

The system holding itself to its own floor.

AX-12Reflexive accountability / no privileged meta-layerEvery claim Microcosm makes about itself, in a page, a validator, a result record, or a projection, passes the same admissibility floor it imposes on everything else.

In plain termsThe system holds its own statements about itself to the same standard it holds everyone else's. It gets no discount for being the one doing the checking.

AnalogyA referee cannot switch to an easier rulebook when the call is about their own team. The same rules apply to them.Microcosm's own claims about itselfis likethe referee judging their own teamthe same admissibility floor as external claimsis likethe single rulebook that applies to everyonethe pages that describe the system, held to the floor they describeis likethe referee's own match report, checked like any otherWhere the analogy breaksThe referee picture shows no special pleading; it does not say the system is therefore complete or correct, only that it cannot exempt itself.

Why it mattersIt lets the system state its own limits without that statement quietly becoming a new unchecked claim.

Potential misreadingThat applying the rule to itself makes the system trustworthy by default. It only removes the exemption; the limits remain, stated rather than hidden.

A system that exempts its own claims from its own floor is just asserting with extra steps. Microcosm removes the exemption: every claim it makes about itself, in a generated page, a validator, a result record, or a coverage projection, has to pass the same admissibility relation it imposes on any external claim. The support evaluator is itself subject to the support floor; this very page is a projection held below the source it describes and cannot raise that source's authority. Removing the escape hatch is what lets the system state its own limits without that statement quietly becoming a new unchecked claim.

Formal statement∀  aM. ∀  φ ∈ claims(a). adm(φ) = admext(φ)For every Microcosm artifact and every claim it carries, the claim is admitted under the same relation as an external claim.Mthe Microcosm artifacts, including its own pages and validatorsaany such artifactφa claim the artifact carriesclaims(a)the claims the artifact carriesadmthe admissibility floor from AX-1admext(φ)the same admissibility relation applied to an external claim
GovernsWhether the system's own outputs get a discount.
RequiresThat meta artifacts, pages, validators, records, and projections, meet the same evidence and refusal floor as everything else.
RefusesA meta-artifact exemption.

In practiceThe launch wording gate runs the same claim-language floor over Microcosm's own public copy that it imposes on any other shard, blocking overclaiming language in the system's own pages.

Enforced inRelease Public Wording Gate Executable Doctrine Grammar

The tempting mistakeA system publishes a self-assessment of "verified and complete" that would never pass the evidence floor it applies to the work it audits.

GroundsP-13 P-18 P-20

Guarded byAP-1 AP-3 AP-11 AP-14 AP-15 AP-16

Scope limitApplying the floor to its own artifacts does not make the system complete or correct. It only removes the special pleading; the limits remain, stated rather than hidden.

Source JSON · Show relationships →

The operating principles

Twenty principles, each an axiom turned into the move an agent makes before it mutates, validates, documents, routes, or publishes. They are grouped by the boundary where each one bites, and a principle inherits its authority only through the specific obligations of the axioms it descends from.

Claim boundary

Before a result is allowed to mean anything.

P-1Recompute, do not echoRecompute a verdict from lower-level evidence instead of repeating a fixture label, route status, or count, and keep a negative fixture where the cheap lie would slip through.

In plain termsTrust a result only after re-deriving it from the underlying evidence, and keep a deliberately wrong test case that the check is required to reject.

AnalogyA teacher re-works the exam answer from scratch instead of copying the answer key, and also keeps a wrong-answer version to confirm the marking actually catches mistakes.the evidence underneath the verdictis likethe exam paper itself, worked from scratchrecomputing the verdict from the evidenceis likere-working the answer instead of copying the keythe negative case the checker must rejectis likethe planted wrong answer the marking must catchWhere the analogy breaksThe re-marking picture shows recomputation plus a trap for false passes; it does not capture every kind of evidence a real check runs over.

Why it mattersWithout it, a label that says 'passed' gets repeated down the line and nobody ever re-derives whether it was true.

Potential misreadingThat re-checking once makes a result permanently safe. It only earns trust for that result, against that check.

P-1 is AX-1 turned into a habit a builder repeats before anything is allowed to mean something. Do not trust a fixture's own verdict, a route status, a count, or a public copy line as proof; recompute it from the evidence underneath and keep a negative fixture that fails when the cheap lie is tried. The negative fixture is the load-bearing half: a check that only ever sees the happy path proves nothing, because it never had the chance to reject. This is the principle that makes "green" mean recomputed rather than reported.

Formal statementtrust(φ)  ⇒  φ = K(B)  ∧  K(Bneg) = rejectTrust a verdict only when a checker recomputes it from the underlying evidence and that same checker rejects the negative fixture built to slip the cheap lie through.trust(φ)a builder is willing to trust the verdict on a claimφthe verdict being claimedK(B)the verdict a checker recomputes from the basisBthe lower-level evidence the checker runs overBnega negative fixture built so the cheap lie should failrejectthe checker's refusal on that negative fixture
GovernsThe claim boundary, before a result is allowed to mean anything.
RequiresRecomputation from lower-level evidence plus a negative fixture that the checker rejects.
RefusesEchoing a declared verdict, label, or count as if repetition made it true.

In practiceThe benchmark-integrity replay recomputes a score from the run rather than trusting the reported number, and keeps gaming attempts as negative cases that must be caught.

Enforced inAgent Sabotage Scheming Monitor Replay Agent Benchmark Integrity Anti Gaming Replay

The tempting mistakeA summary repeats a component's self-reported "passed" into a status board without ever recomputing it or keeping a case that would fail.

Grounded inAX-1

Scope limitRecomputing one verdict from evidence does not make the principle a witness for AX-1; it operationalises specific obligations and inherits no authority beyond them.

Source JSON · Show relationships →

P-2Lower claim strength to checker strengthHold a claim no stronger than what its named checker actually computes; a checker that decides one local contract cannot license prose claiming global authority.

In plain termsA statement can only be as strong as the exact thing the check actually settled. If a check confirms one small, local fact, the writing around it must not stretch that into a sweeping claim about the whole system.

AnalogyA blood test that measures one thing, like iron levels, tells you about iron. It does not let you write 'this person is in perfect health' on the chart.the claim's strength is capped at what the named check decidesis likethe iron test only supports a statement about ironprose overreaching past the check into system-wide authorityis likewriting 'perfectly healthy' off one narrow blood testWhere the analogy breaksThe blood-test picture shows that a result is limited to what was measured; it does not show how several separate checks are combined, where the overall ceiling drops to the weakest one. It is an illustration, not support that the rule holds everywhere.

Why it mattersIt stops a narrow, genuine check from being written up as a broad system-wide claim, so readers can size a claim to what was really tested.

Potential misreadingThat because the underlying check was real, any confident sentence built on it is also safe. The check sets a ceiling; words above that ceiling are not earned and do not prove the wider claim.

P-2 is the strength half of the admissibility floor: AX-1 caps a claim at the strength of the check that accepts it, and AX-5 makes that ceiling the meet of the parts, so the strongest honest claim equals the weakest component the checker actually settles. Its bite is distinct from "recompute, do not echo": even a genuinely recomputed verdict overclaims if the prose around it reaches past what the checker decided, for example a validator that confirms a record's shape being read as proof of the property the record names. The cover calculus enforces this by computing each scope limit from the specific grounding obligations, never from whole-axiom labels and never by hand-stamping; support for the principle is bounded by the covers of the obligations beneath it. This is the rule that keeps a local-contract checker, a registry, or a single witness route from being narrated into a system-wide guarantee.

Formal statementstrength(φ) ⊑ ⨅i strength(Ki(B))   where {Ki} = decided(φ)A claim's strength is bounded above by the meet of the strengths of exactly the checks that actually decide it; the ceiling is the weakest deciding component, not the most impressive one.strength(φ)the strength a claim is allowed to assertφthe claim being madeKia checker, validator, registry, or witness route that decides part of the claimBthe basis the deciding checks run overmeet: the weakest of the deciding componentsdecided(φ)the set of checks that actually settle the claim, excluding ones it merely names
GovernsThe strength boundary, where a claim is sized to the check that accepts it.
RequiresCapping a claim at the meet of what its named checker, validator, registry, or witness route actually computes, with the ceiling derived from the grounding obligations rather than asserted.
RefusesLetting a checker that decides only a local contract license prose that projects global or system-wide authority.

In practiceThe formal-math readiness gate computes how far its available evidence actually reaches and reports that boundary as the claim, refusing to narrate a local check into a proof of readiness.

Enforced inFormal Math Readiness Gate Release Public Wording Gate Agent Route Observability Runtime

The tempting mistakeA component validates that a result record has the expected fields, and a summary page reads that shape check as evidence the underlying property holds across the whole system.

Grounded inAX-1 AX-5

Scope limitHolding a claim to its checker's strength does not raise that checker, and the principle is not a witness for AX-1 or AX-5; it operationalises specific grounding obligations and inherits no support beyond the covers computed for them. The worked example illustrates the rule for a reader and never counts as support that the principle is obligation-backed or complete.

Source JSON · Show relationships →

P-3Concentrate trust in small checkersPrefer a small verifier, parser, or kernel you can rerun over broad narrative confidence; the producer may be large, but the deciding surface should stay small enough to inspect.

In plain termsPut your trust in one small, simple step that re-does the work and decides, while letting the big complicated thing that produced the answer stay outside that decision. The thing being judged should not get to be its own judge.

AnalogyAt a self-checkout, the small weighing plate re-weighs each item to confirm what was scanned. The shopper, who knows what is in the bag, is never the one who decides the bag is correct.the small checker that rereads and decidesis likethe weighing plate that re-checks each itemthe large producer kept outside the trusted decisionis likethe shopper, who is not allowed to confirm their own bagWhere the analogy breaksThe weighing-plate picture shows where the deciding power sits and that the producer is kept out; it does not show that a small checker is automatically a correct or complete one. A simple checker can still be wrong, and this is only an illustration.

Why it mattersKeeping the deciding part small means the part you actually have to audit and re-run stays small, even as the systems producing answers grow large and hard to inspect.

Potential misreadingThat a confident, capable producer can be trusted to vouch for itself. Once the thing being judged also decides, there is no real check left, only restated confidence.

P-3 is AX-2 turned into a building habit: the thing you trust should be small enough to read and rerun, while the thing that did the work may be as large and opaque as it likes. A big model, search, or pipeline emits a certificate; a small verifier, parser, harness, compiler route, or registry contract rereads that certificate and decides, and only the checker sits inside the trusted boundary. This connects directly to the claim and evidence model: a claim's strength is capped at the strength of the check that admits it, so shrinking the checker shrinks what you have to believe to believe the verdict. The load-bearing move is keeping the producer outside the boundary; once the thing being judged also gets to decide, the check has collapsed into the same narrative confidence it was meant to replace.

Formal statementtrust(φ)  ⇒  ∃  K, c. K(c) = accept  ∧  tcb(φ) = {K}  ∧  producertcb(φ)Trust a verdict only when a small checker rereads a certificate and accepts, the trusted base consists of that checker alone, and the producer that emitted the certificate sits outside that base.trust(φ)a builder is willing to trust the verdict on a claimφthe claim being trustedKthe small checker that decidescthe certificate the producer emitstcb(φ)the trusted base the claim rests on: the set of components you must believeproducerthe large component that emitted the certificate, kept outside the trusted baseis kept outside
GovernsWhere trust is concentrated, between the large producer and the small thing that decides.
RequiresA small checker that rereads a certificate and accepts, with the producer kept outside the trusted boundary.
RefusesTrusting a large producer's own confidence in place of a small, inspectable, rerunnable check.

In practiceThe certificate kernel lab keeps producers separate from the checker: a producer emits certificate material and a small kernel rereads and decides, so the authority lives in the part you can inspect and rerun rather than in the producer.

Enforced inCertificate Kernel Execution Lab Formal Math Lean Proof Witness Verifier Lab Kernel

The tempting mistakeA large model is trusted because it sounds sure of its answer, with no small separate checker rereading anything, so the producer is also the judge.

Grounded inAX-2

Scope limitConcentrating trust in a small checker does not make the principle a witness for AX-2, and a small checker is not automatically a correct or complete one. It operationalises specific obligations and inherits no authority beyond them; admission, support, and this reader illustration stay independent.

Source JSON · Show relationships →

P-8Refuse inadmissible computations with typed reasonsWhen a precondition fails, return a reasoned refusal rather than a fabricated statistic, safety verdict, or readiness status that keeps a path green.

In plain termsWhen a step cannot be done properly because something needed is missing, it should hand back a clear refusal that says why and shows the basis, not a made-up answer that lets things look finished.

AnalogyA pharmacist who is missing a required detail on a prescription hands it back with the reason written on it, instead of guessing a dose just to send the patient away with a filled bottle.return an Ok result only when the precondition holdsis likethe pharmacist dispenses only when the prescription is complete and validwhen the precondition fails, return a typed refusal carrying its reason and evidenceis likean incomplete prescription comes back with the specific missing detail noted on itdo not emit a meaningless value just to keep a green pathis likethe pharmacist does not invent a dose to avoid an empty-handed patientWhere the analogy breaksThis shows why a refusal that names its reason beats a fabricated answer; it does not establish that the refusal itself is correct or that the request was valid, only that an unfounded answer is withheld. A returned refusal is information, not a verdict on the underlying request.

Why it mattersIt keeps a system from emitting a forecast past its data, a confidence figure with nothing behind it, or a ready flag while a needed part is missing, all just to avoid showing red.

Potential misreadingThat returning some number is always better than returning nothing, even when the basis for that number does not exist.

P-8 is AX-7's typed-partiality law made into the habit a builder applies at every computation that can fail. A function whose precondition does not hold, or whose library or corpus is absent, must totalize into a refusal that names why and cites the evidence, instead of returning a meaningless statistic, a proof verdict, a safety judgement, or a public-readiness status just to avoid a red path. This bites because the cheapest way to look finished is to emit a number anyway: a forecast computed past its sample size, a confidence interval with no distribution behind it, a readiness flag asserted while the dependency is missing. It connects to the claim and evidence model because a refusal is the honest evidence value when the basis is not admissible; a fabricated green output is a claim with no checker under it, which is exactly the bottom-of-the-order assertion the rest of the doctrine refuses.

Formal statement(run(g, x) = Ok(y) ⇒ Pre(g, x))  ∧  (¬ Pre(g, x) ⇒ ∃  r, ε. run(g, x) = Refusal(r, ε))An Ok result certifies that the precondition held: a value may come out only when the computation had grounds to run. And when the precondition fails, the computation returns a typed refusal carrying some reason and its evidence, never a bare value.run(g, x)evaluating the partial computation g on input xga partial computation that can failxthe input to gOk(y)an admissible result value yPre(g, x)the declared precondition for running g on input x¬the precondition does not holdRefusal(r, ε)a typed refusal carrying reason r and evidence \epsilon
GovernsThe result boundary, where a computation that cannot proceed is tempted to return a number anyway.
RequiresReturning an Ok result only under a declared precondition, and a refusal carrying a reason and evidence when the precondition fails or a dependency is absent.
RefusesEmitting a meaningless statistic, proof authority, safety verdict, or readiness status to keep a green path when the basis does not admit one.

In practiceThe finance forecast evaluation spine returns a typed refusal when a forecast horizon reaches or exceeds the sample size or when the statistics dependency is unavailable, rather than reporting a loss differential the data cannot support.

Enforced inFinance Forecast Evaluation Spine Corpus Readiness Mathlib Absence Gate

The tempting mistakeA readiness gate reports a corpus as available and prints a green status while the underlying library is missing, turning an absent dependency into a silent overclaim.

Grounded inAX-7

Scope limitReturning a typed refusal in these cases does not make P-8 a witness for AX-7 or prove refusal-correctness across every partial computation. It operationalises the specific grounding obligations and inherits no authority beyond the bounded cases that actually refuse.

Source JSON · Show relationships →

Authority and mutation boundary

Before a change lands.

P-4Possession is not permissionA account secret, role name, or trusted session cannot authorise a change on its own; authority is dereferenced from proof, policy, and current world state.

In plain termsHolding a account secret, a role name, or being inside a 'trusted' session does not by itself give permission to make a change. Permission is worked out fresh for each specific action, from the rules and the current situation.

AnalogyKnowing someone's bank card number does not let money move. For each payment, the bank checks this card, this amount, and the live account state before it lets the transfer go through.the standing account secret or role name that is not authority on its ownis likemerely having the card numberauthority derived per action from policy and current world stateis likethe bank deciding each payment against this account, right nowWhere the analogy breaksThe bank-transfer picture shows that holding a account secret is not the same as being cleared to act; it does not capture everything weighed at decision time, such as the specific permissions, the rules, and the side-effect records. It is an illustration only.

Why it mattersIt closes the gap where a component that holds broad standing power is talked into using it for someone else, since each action still has to earn its own permission.

Potential misreadingThat a valid account secret is enough to act. The account secret is one input; the actual change still has to be cleared for that exact action against the current state.

P-4 is the authority leg of the claim model, the way P-1 is the evidence leg: before an effect lands, recompute whether it is authorized rather than reading authority off who is asking. Authorization for a subject and an effect comes from dereferenced proof references, the governing policy, rollback or result-record evidence, and current world state; standing account secrets, an admin role name, or trusted-session phrasing are ambient identity, which carries no authority by itself. This is the confused-deputy failure stated as a rule: a component holding a powerful capability must still derive permission for each effect, and tool authority is bounded by declared identity, scope, approval, and side-effect records, not by the tool merely being available. It bites because possession reads as permission almost everywhere, so a pipeline that trusts a present account secret passes its own path while granting reach nothing actually authorized.

Formal statementauth(u, e) = F(deref(tokens), policy, proofs, world);   identity(u)  ∧  deref(tokens) = ∅  ⇒  auth(u, e) ≠ grantAuthorization for a subject and an effect is the output of the derivation over the dereferenced tokens, governing policy, proof references, and world state; ambient identity whose tokens dereference to nothing grants nothing. The account secret is an input to the derivation, never a substitute for it.auth(u, e)a subject is authorized for an effectua subject requesting an effectethe effect or mutation it wants to landFthe function deriving authorization from the dereferenced tokens, policy, proofs, and world statederef(tokens)the capabilities the presented tokens actually dereference topolicythe governing policyproofsthe proof references and rollback or result-record evidenceworldcurrent world stategrantthe authorizer's grant of the effectidentity(u)the subject's ambient account secret or role name, insufficient on its own
GovernsThe authority boundary, before any effect or mutation is allowed to land.
RequiresDeriving authorization from dereferenced proof, policy, and world state, with tool effects bounded by declared identity, scope, approval, and side-effect records.
RefusesTreating a standing account secret, role name, admin phrasing, trusted session, or tool availability as authority on its own.

In practiceThe tool-authority replay binds each tool effect to a declared scope and approval and rejects an overbroad scope or an unapproved side effect, so reach is derived from declared authority rather than from the tool being callable.

Enforced inProof Derived Governed Mutation Authorization MCP Tool Authority Replay Tool Server Pressure Inventory

The tempting mistakeA mutation is allowed because the caller holds a valid admin account secret, with nothing dereferencing that account secret to the specific effect or checking it against policy and current state.

Grounded inAX-3

Scope limitDeriving authorization in these components does not make P-4 a witness for AX-3 or raise that axiom's support ceiling; it operationalises the specific obligations that authorization is derived, that standing account secrets are insufficient, and that tool effects require declared scope, and inherits no authority beyond them. The worked example is reader illustration and computes no support.

Source JSON · Show relationships →

P-10Do not land effects without compensationA write, launch step, or import needs ordered transaction evidence: it locks after durable records, recomputes after launch, and blocks a stale-parent or same-path conflict before committing.

In plain termsAn action only counts as done when there is a permanent written record of it, a clear way to undo it (or a stated point of no return), and a check that no two people changed the same thing at once on outdated information. Running successfully is not the same as having landed.

AnalogyA bank wire only counts as sent once the bank writes it into its permanent ledger, attaches a way to reverse or chargeback if needed, and confirms no second clerk moved the same account in the same moment off an out-of-date balance.the effect being treated as landedis likethe wire being treated as sentthe durable ordered recordis likethe entry written into the bank's permanent ledgera compensator, or a declared irreversible boundaryis likean attached reversal/chargeback path, or a stated point where it can no longer be pulled backcompare-and-swap on the expected parentis likeconfirming the account balance is still the one the clerk started from before applying the changesingle writer holding the pathis likeno second clerk touching the same account at the same momentWhere the analogy breaksThe wire picture shows that a single transfer can be recorded, reversed, and protected from a race; it does not show the bank's whole system is sound, and one clean transfer does not establish that every account or every transfer is safe.

Why it mattersWithout this, a step that crashes between starting and finishing can look complete while leaving a half-done effect that nobody can recompute or unwind, which is how doubled, lost, or unauthorised changes slip through.

Potential misreadingThinking that because an operation reported success it must therefore be safely and fully landed. The most dangerous moment is the gap between two steps, where a lock can launch before the permanent record is written.

P-10 is AX-9 turned into the discipline a builder runs before any effect is allowed to be real. A write, a launch step, a claim launch, a source import, or a rollback-shaped operation is not landed because it ran; it is landed only when ordered transaction evidence exists for it, when it carries a compensator or a declared irreversible boundary, when a compare-and-swap confirms the parent it expected has not moved, and when a single writer holds its path. This connects to the claim and evidence model because a landed effect is itself a claim about the world, and an effect with no compensation and no concurrency guard is a confident assertion that nobody can recompute or undo. It bites hardest in the gap between two steps: the moment a lock releases before the durable record is written, or two writers race the same path on a stale parent, is exactly where an unrecoverable, unauthorised, or doubled effect slips through.

Formal statementlanded(e)  ⇒  durable(e)  ∧  (comp(e) ∨ irrev(e))  ∧  (multi(e) ⇒ cas(parent(e)) ∧ |writers(path(e))| ≤ 1)An effect lands only if it is durable and declares a compensator or an irreversible boundary; and when it is multi-step, only under a compare-and-swap on its expected parent with at most one writer on its path.landed(e)the effect e is treated as landedean effectdurable(e)e is recorded durablycomp(e)a declared compensator that can reverse eirrev(e)a declared irreversible boundary for emulti(e)e is a multi-step effectcas(parent(e))a compare-and-swap on e's expected parent|writers(path(e))| ≤ 1at most one writer holds e's path
GovernsThe effect boundary, where an operation is about to be treated as landed and irreversible.
RequiresAn ordered durable record, a compensator or declared irreversible boundary, a compare-and-swap on the expected parent, and a single-writer hold on the path before the effect counts as landed.
RefusesTreating an operation as landed with the lock released before the durable record, a stale parent, or a second writer on the same path.

In practiceThe mission transaction work spine lands a multi-step effect only after the durable record is written, recomputes once the lock releases, and blocks a stale parent or a same-path conflict, so a half-applied write cannot be reported as complete.

Enforced inMission Transaction Work Spine Durable Agent Work Landing Replay Concurrency Mission Control

The tempting mistakeA launch step reports success after acquiring a lock but before the durable record is written, so a crash in the gap leaves an effect that looks landed with nothing to recompute or compensate it.

Grounded inAX-9

Scope limitOrdering one transaction and guarding one path does not establish the whole system is crash-safe or serialisable. P-10 operationalises specific AX-9 obligations on the effects it covers; it is not a witness for the axiom and inherits no authority beyond those obligations, and a passing guard on a named path says nothing about effects it never mediated.

Source JSON · Show relationships →

P-16Bind authority to transaction scopeMutation authority is the whole transaction, the proof-derived permission, the declared write scope, the parent state, the compensation, and the landing evidence, not merely who can touch a file.

In plain termsBeing allowed to change something is not one thing, like having access to a file. It is several conditions holding together for this exact change: worked-out permission, the agreed limits of what you may touch, the current state still matching what you expected, a way to undo, and a record that it landed.

AnalogyA bank wire is not sent just because you are a signatory. The transfer goes through only when the amount is within your approved limit, the account still shows the balance you expected, and there is a way to reverse it if it was wrong.proof-derived permission, not standing accessis likethe bank checking this transfer against your approved limits, not just that you are a signatorycurrent parent state matching what was expectedis likethe account still showing the balance you expected before the wire goes outcompensation, a way back from the effectis likea reversal path if the transfer turns out to be wrongWhere the analogy breaksThe wire picture shows that several conditions must hold together for one transfer; it does not establish that any given transfer is correct, and it does not capture the claimed write scope and landing evidence that the rule also requires.

Why it mattersIt closes the gap where someone with broad standing access is treated as authorized to make a change, even though nothing checked the specific change against its scope, the current state, and a way to undo it.

Potential misreadingThat having access means you are authorized to change something. Access is one input; permission still has to be worked out for this exact change, against the state you actually find.

P-16 turns AX-3 and AX-9 into a single rule about what makes a mutation legitimate. Authority to change something is not who holds a account secret or which tool happens to be reachable; it is a bundle attached to one transaction, derived permission from policy and proof and current world state, a declared write scope the effect must fall inside, the parent state the write expected to find, a compensator or a declared irreversible boundary, and the evidence that the change actually landed. The rule bites because the cheap path is the opposite of all five: act because you can touch the file, on whatever the head is, with no scope and no way to undo. It connects to the claim and evidence model directly, since each part of the bundle is a check that has to recompute rather than a account secret that gets waved through, and the same admissibility floor applies to a write request that applies to any other claim.

Formal statementauth(m, t) ⇔ derived(m)  ∧  effect(m) ∈ scope(t)  ∧  parentobs(t) = parentexp(m)  ∧  comp(m)  ∧  landed(m, t)A mutation m is authorized within transaction t exactly when its permission is derived rather than possessed, its effect falls inside the transaction's declared write scope, the observed parent state equals the parent the write expected, a compensator or declared irreversible boundary is present, and landing evidence exists for this transaction.auth(m, t)mutation m is authorized within transaction tma proposed mutation (write effect)tthe transaction the write is bound toderived(m)permission derived from policy, proof, and world state, not a standing account secreteffect(m)the write effect m would applyscope(t)the declared write scope of the transactionparentobs(t)the parent state actually observed for the transactionparentexp(m)the parent state the write expected (compare-and-swap base)comp(m)a declared compensator or irreversible boundarylanded(m, t)evidence that the effect actually landed for this transaction
GovernsThe authorization boundary, where a write is about to be allowed against a file or record.
RequiresBinding the write to this transaction as derived permission, declared scope, expected parent state, a compensator or boundary, and landing evidence together.
RefusesTreating reach or a standing account secret as authority, or writing on whatever the current state is without an expected parent, scope, or way to compensate.

In practiceThe proof-derived mutation authorization component admits a change only when the authority is derived from policy and proof references for that effect, and rejects a write that leans on a standing account secret, so permission is computed per transaction rather than possessed.

Enforced inProof Derived Governed Mutation Authorization Mission Transaction Work Spine MCP Tool Authority Replay

The tempting mistakeA write is allowed because the agent already holds a token and the file is reachable, landed against whatever the head is, with no declared scope and no compensator.

Grounded inAX-3 AX-9

Scope limitBinding one write to its transaction scope does not make P-16 a witness for AX-3 or AX-9, and the example does not establish that every write path in the system carries the full bundle; it operationalises specific grounding obligations and inherits no authority beyond them.

Source JSON · Show relationships →

P-18Require fan-in before activationA staged law, standard, or component stays inactive until its owner boundary, source row, generated parity, and validation record land together; partial admission remains residual pressure.

In plain termsSomething new does not start carrying authority just because a draft of it has appeared. All the required pieces, who owns it, the exact source entry, the matching generated copy, a passing check, and the recorded change of status, have to land together in one step. Until then it is still pending, not in force.

AnalogyA new bylaw is not in force the moment someone tables a draft. It takes effect only when it is voted in, signed, recorded in the register, and its status is formally changed in one sitting. A draft circulating in the room is still a proposal, not the rule.the required pieces landing in one governed transactionis likethe bylaw being voted, signed, registered, and status-changed in one sittinga staged item is not yet active authorityis likea tabled draft is still a proposal, not the rulepartial admission stays residual pressureis likea draft that passed some steps but was never recorded is held over, not enactedWhere the analogy breaksThe bylaw picture shows that authority needs all the steps to land together before it counts; it does not establish that an enacted rule is wise or correct, and it does not capture the blocked-record case where a partial item is explicitly held without losing its place.

Why it mattersIt stops a half-finished draft from being treated as the live rule, where some steps are done and the rest are assumed, so nobody is acting on something that never actually took effect.

Potential misreadingThat once the content is drafted and looks complete, it is in force. The content is only in force when ownership, source, generated copy, check, and status change all land together.

P-18 is the rule that stops a half-finished change from being treated as done. A staged law, standard, component, or generated view is not active authority until its owner boundary, its source row, its generated parity, its validation record, and its status change have all landed inside the same governed transaction, or until an explicit blocked record holds the frontier open instead. The hard case is the one builders trip over: a view generated from a source that another live owner is still holding dirty is still outside fan-in, because the basis under it can move before it lands, so the honest move is to request handoff, wait for the owner to land, or write the blocked record rather than treat the view as current. This connects the claim, evidence, and authority model at the moment of admission: derived authority must arrive as one compare-and-swap, single-writer transaction (AX-3, AX-9), carry its grammar and records (AX-11), and the system holds its own staged doctrine to the same gate (AX-12), so any component admitted before the others is residual pressure, not authority.

Formal statementactive(x)  ⇒  ⨅creq(x) landed(c, τ) = ⊤  ∧  single(τ);   else xR  ∨  blocked(x)A work item carries active authority only when every required dependency has landed under a single transaction; otherwise it stays as residual pressure or blocked.active(x)x carries active authorityxa work itemthe meet taken over the required dependenciesca required dependencyreq(x)the dependencies x requireslanded(c, τ)dependency c has landed in transaction tauτthe activating transactiontop: fully landedsingle(τ)a single transaction covers the fan-inRresidual pressure: not yet activeblocked(x)x is blocked
GovernsThe activation boundary, where a staged change is tempted to count as authority before all of it has landed.
RequiresOwner boundary, source row, generated parity, validation record, and status change all landing in one single-writer governed transaction, or an explicit blocked record that holds the frontier.
RefusesTreating a partially admitted change, or a view built on a source another owner still holds dirty, as active authority.

In practiceThe mission transaction spine lands a multi-step change as one saga with a compare-and-swap parent and a single-writer constraint, so a staged item counts as active only after the whole transaction commits rather than at the first partial step.

Enforced inMission Transaction Work Spine Concurrency Mission Control Proof Derived Governed Mutation Authorization

The tempting mistakeA generated card is treated as live the moment it renders, while the source it was built from is still held dirty by another owner and has not landed, so the basis under the card can still move.

Grounded inAX-3 AX-9 AX-11 AX-12

Scope limitRequiring the components to fan in before activation does not establish the staged change correct, complete, or safe; it only fixes when the change is allowed to count as authority. This object and its example are reader illustration and never compute support for the axioms that ground the principle.

Source JSON · Show relationships →

Source and projection boundary

Between a source and the views drawn from it.

P-5Cache by content, not by nameA reusable result must carry its content basis; any drift in source bytes, scoped files, or parent state cancels the reuse.

In plain termsA saved result can be reused only if it is tagged with the exact inputs it was made from, and those inputs still match. If the inputs have changed, you must redo the work; a matching name or label alone is never enough.

AnalogyA warranty repair is only valid for the exact unit whose serial number is on the claim. If a part with a different serial was swapped in, a matching model name on the box does not make the old warranty apply.reuse only when the stored content tag matches the current inputsis likethe warranty holds only when the serial number still matches the unita name or label match alone licensing reuseis liketrusting the model name on the box instead of the serialWhere the analogy breaksThe serial-number picture shows that identity must match the exact item, not just the label; it does not cover every kind of input drift the rule watches, such as changed source bytes, edited files, or a moved parent. It only illustrates the rule.

Why it mattersIt stops a stale or tampered result being served as fresh just because its name or path still looks familiar after the content underneath has moved.

Potential misreadingThat a matching name or path means the cached answer is still good. Only a match on the actual content the result was computed from licenses reuse; otherwise the work has to be redone.

P-5 turns content-addressed determinism into a habit a builder repeats before reusing any prior work. A stored result record, a coalesced command run, an imported source copy, or a resumed work-landing attempt may be reused only if it carries the digest of the exact content it was derived from; equal content basis permits reuse, and drift in the source bytes, the dirty scoped files, the parent commit, or the fixture input forces a recompute or a refusal. The bite is that a name, a path, or a label is a cheap stand-in for a basis: cache by name and you serve a stale answer the moment the content moves underneath the name. This connects straight to the claim and evidence model, because a reused verdict inherits its scope limit from the basis it was actually checked over, and reuse across drift silently widens that scope to content nothing ever verified.

Formal statementreuse(a, B')  ⇒  id(a) = H(B')  ∧  ¬ missing(B')   else recomputeA prior result may be reused for an incoming basis only when the result's stored content id equals the digest of that basis and the basis actually resolves; in every other case, recompute.reuse(a, B')a prior result is served for an incoming basis instead of recomputedaa prior result eligible for reuseB'the content basis of the incoming requestH(B')the digest over that content basisid(a)the content id the result was stored undermissing(B')the incoming basis cannot be resolved; bottom, licensing no reuse
GovernsThe reuse boundary, where a prior result is about to be served instead of recomputed.
RequiresA declared content basis carried as a digest with the result, equal-basis reuse only, and a recompute or refusal the moment the source digest, scoped files, parent commit, or fixture input drifts.
RefusesServing a cached result keyed on a name, path, or label after the content behind it has drifted.

In practiceThe source-import protocol brings material in by manifest and digest, so when the source bytes drift the imported copy is recomputed rather than reused under the same name.

Enforced inSource Projection Import Protocol Durable Agent Work Landing Replay

The tempting mistakeA resumed work-landing attempt reuses an earlier result because the task name matches, even though the parent commit and scoped files have changed underneath it.

Grounded inAX-4

Scope limitCarrying a content basis on the reuse paths shown here does not establish reuse is sound everywhere; one freshness-basis mismatch remains a declared open gap, and this card and its example are reader illustration that compute no support for the principle or its grounding axiom.

Source JSON · Show relationships →

P-9Preserve provenance across every boundaryEvery shard crossing from source, fixture, result record, or provider shape carries a provenance class and a ceiling; if a flow is only labelled at its endpoint, say so.

In plain termsA value carries a record of where it came from and how far it is allowed to be used, and that record must travel with it across every handoff. If something was only labelled clean at the final door, that has to be stated, not treated as if the label rode along the whole way.

AnalogyA shipped parcel carries a chain-of-custody log and a tamper seal applied at origin; if a clean sticker was simply slapped on at the loading dock at the end, the log must note that, because a sticker at the door is not the same as an unbroken seal carried the whole route.a value carries its provenance class across the boundaryis likethe parcel carries its origin-stamped custody log through every handoffthe scope limit is carried, not stamped at the endpointis likethe tamper seal is applied at origin and travels intact, not pressed on at the final dockan endpoint-only label must be recorded as merely declaredis likea sticker added only at the loading dock has to be logged as a door-label, not a carried sealWhere the analogy breaksThis shows why a label applied only at the end is weaker than a record carried the whole way; it does not establish that an origin seal guarantees the contents are correct, only that an end-of-line sticker proves less than a continuous record. A carried log is not the same as the goods being verified.

Why it mattersIt lets a clean-looking final copy still be treated as unverified, so trust depends on where a value came from and what was done to it, not on how it looks at the last step.

Potential misreadingThat a clean label at the final destination is enough, regardless of whether that label actually accompanied the value across the earlier boundaries.

P-9 is AX-8 turned into the discipline a builder runs at every boundary a value actually crosses: imported source, a fixture, a result record, public copy, a model-output data shape, or material adjacent to a private root. Each crossing must carry a provenance class and a scope limit with the value, because trust is a property of where something came from and what was done to it, not of where it lands. The honesty half is load-bearing and is what separates this from AX-8 stated abstractly: when a flow is only declared, or only labelled clean at the endpoint instead of having the label carried across, the principle requires you to record that gap rather than read the endpoint label as proof. This is the rule that lets a clean-looking final copy step still be treated as unverified, and it is why the system tracks how far a value may travel rather than only what it currently looks like.

Formal statement(xs)  ⇒  (prov(x) ⊑ policy(s)  ∧  carried(ceil(x)))  ∨  declared(xs)For any value x crossing into a sink s, either x's provenance sits within the sink's policy and its scope limit is carried across, or the crossing is explicitly recorded as only declared.xa value crossing a boundarythe value crosses into the sinksa sink (a public or privileged destination)provthe provenance class carried with xsits within what the sink policy admitspolicywhat the sink is allowed to admitceilthe scope limit carried with xcarriedthe scope limit is propagated across the crossing, not stamped at the endpointdeclaredthe crossing is recorded as only declared, not propagated
GovernsEvery boundary a value crosses, from imported source through to a public or privileged sink.
RequiresA provenance class and scope limit carried with the value across the crossing, and an explicit record when a flow is only declared or endpoint-labelled.
RefusesReading a clean endpoint label as proof when the label was stamped at the door rather than carried across the boundary.

In practiceThe prompt-injection replay carries the information-flow policy with the data, so untrusted instructions arriving at a tool call are caught at the boundary instead of being trusted for having reached a trusted endpoint.

Enforced inIndirect Prompt Injection Information Flow Policy Replay Source Projection Import Protocol

The tempting mistakeA public page prints a value lifted from a private-adjacent source because the final copy step looked clean, with no provenance carried across the copy.

Grounded inAX-8

Scope limitP-9 guides these flows only through source-derived edges; it is not a witness and does not raise the support ceiling of its grounding axiom. Catching labelled flows at named boundaries does not establish non-interference across the whole graph: general propagation is bounded by what is actually traced, and that debt is recorded rather than hidden.

Source JSON · Show relationships →

P-14Carry basis and provenance togetherBasis says which bytes were used; provenance says where they may flow and how strongly they may be claimed. A shard missing either side is only half routed.

In plain termsEvery piece of data must carry two things at once: a record of exactly which inputs it was built from, and a record of where it is allowed to go and how strongly it can be claimed. If either tag is missing, the data is not ready to be used.

AnalogyA blood sample reaching the lab needs both a label saying which patient and draw it came from and a handling tag saying what it may be tested for. A tube with only one of the two tags is set aside, not run.the content basis (which inputs the value was built from)is likethe label naming the patient and the draw the sample came fromthe provenance (where it may flow and how strongly it may be claimed)is likethe handling tag stating what the sample may be tested fora value missing either side is not fully routedis likea tube with only one tag is set aside rather than runWhere the analogy breaksThe two-label picture only shows that both tags must be present together; it does not establish that a fully labelled sample is correct or safe, and it does not capture how a flow tag tightens as data combines with other data.

Why it mattersIt stops data from being trusted on a partial paper trail, where you know what something is but not where it may go, or where it may go but not what it actually came from.

Potential misreadingThat one good label is enough. Knowing the source does not tell you where the value may travel, and a flow tag with no record of inputs is a tag attached to nothing.

P-14 joins the two halves the system tracks about any value that travels or gets reused: its content basis, the exact bytes or rows it was computed from, and its provenance, the trust class and ceiling that say where it may flow and how strongly it may be claimed. Carrying only the basis lets a value be cached and rederived correctly but says nothing about whether it is safe to expose; carrying only provenance labels its trust but loses the digest that detects when the underlying source drifts. The principle is that a shard missing either side is not fully routed, because reuse, freshness, and disclosure are three questions the system answers together rather than one at a time. It sits where caching meets information flow: a reused result record, a source import, or a work-landing attempt has to declare what it was built from and what it is allowed to become before anything downstream may trust it.

Formal statementrouted(v)  ⇒  basis(v) ≠ ∅  ∧  prov(v) ≠ ∅  ∧  (drift(basis(v)) ⇒ recompute(v))A value is fully routed only when it carries a non-empty basis and a non-empty provenance, and any drift in its basis forces a recompute.routed(v)v is fully routed: it carries both basis and provenance and recomputes on driftva reusable or travelling value (result record, import, work-landing)basis(v)the declared bytes or rows v was computed from, as a digestprov(v)v's provenance class and scope limitdriftthe basis digest no longer matches its sourcerecompute(v)v must be re-derived from source rather than reusedabsent: the half was never declared
GovernsThe boundary where a value is reused or crosses a flow, between what it was built from and where it may go.
RequiresBoth a declared content basis whose drift forces recompute and a provenance class with ceiling carried across every boundary, on the same value.
RefusesA shard that declares only its basis or only its provenance and is then treated as fully routed.

In practiceThe source-import protocol brings material in by manifest and digest, so the imported copy carries the content basis that detects source drift and the provenance label that bounds where it may flow, both on the same value before anything downstream reuses it.

Enforced inSource Projection Import Protocol Durable Agent Work Landing Replay Indirect Prompt Injection Information Flow Policy Replay

The tempting mistakeA reused result record carries a clean provenance label but no content digest, so it keeps being trusted after the source it was built from has changed underneath it.

Grounded inAX-4 AX-8

Scope limitCarrying both halves on the cases it governs does not witness the axioms it grounds, AX-4 and AX-8, or make either one strong. The principle operationalises specific obligations from those axioms and inherits no authority beyond them; the worked example is reader illustration and computes no support.

Source JSON · Show relationships →

P-15Keep projections below source authorityA generated doc, card, or paper module may expose a source truth but never upgrade it; recompute from source, or demote, when the basis, grammar, or status no longer supports the projection.

In plain termsA generated view can show what a source says, but it can never carry more authority than that source. If the source weakens, the view has to be recomputed or marked as lower.

AnalogyA photocopy of a contract can be read and shared, but it does not outrank the signed original. If the original is amended, the old copy stops being authoritative.the source truthis likethe signed original contractthe projection held at or below the sourceis likethe photocopy that can be read but cannot overrule the originalrecompute or demote when the source weakensis likethe old copy losing its standing the moment the original is amendedWhere the analogy breaksThe photocopy picture shows that a view cannot outrank its origin; it does not capture that the view's ceiling is set by several source properties at once, like freshness and provenance, not just by being a copy.

Why it mattersIt stops a polished public page or summary being treated as more trustworthy than the working source it was drawn from.

Potential misreadingThat a clear, confident-looking view must be reliable. Its reliability is capped by the source, however good the view looks.

P-15 is what stops the website you are reading from becoming an authority in its own right. A generated doc, a card, a route map, or a paper module may expose a source truth, but it can never raise that truth's strength. A projection's ceiling is bounded by the meet of its source's support, freshness, provenance, and grammar validity, so the moment any of those slips, the projection has to recompute from source or demote. This is the principle that lets the system publish freely without the act of publishing inflating what was published. It is also why this page repeatedly tells you what it cannot prove: the page is downstream of its source and inherits that source's limits.

Formal statementceil(proj) ⊑ support(src) ⊓ fresh(src) ⊓ prov(src) ⊓ grammar(src)A projection's ceiling is at most the meet of its source's support, freshness, provenance, and grammar validity; it can expose the source but never upgrade it.ceilthe strongest claim the projection may carryproja generated view (doc, markdown summary, route card, paper module)is at most as strong as, in the authority latticesupportthe source's evidence support levelsrcthe source the projection draws fromfreshthe source's freshness, whether its basis is still currentprovthe source's provenance class and scope limitgrammarthe source's grammar validity, whether it is in the executable grammarmeet: the weakest of the components
GovernsThe source-and-projection boundary, between a truth and the views drawn from it.
RequiresHolding a projection at or below its source's support, freshness, provenance, and grammar, and recomputing or demoting when any slips.
RefusesA generated page, card, or summary that claims more authority than the source it summarises.

In practiceThe source-import protocol brings material in by manifest and digest and never lets the imported copy outrank the original it was projected from.

Enforced inSource Projection Import Protocol World Model Projection Drift Control Room

The tempting mistakeA polished summary page is cited as the authority for a number, even after the source it was generated from has drifted underneath it.

Grounded inAX-4 AX-5 AX-11

Scope limitKeeping a projection below its source does not make the source correct. It only prevents the projection from inventing authority the source never had.

Source JSON · Show relationships →

Time and coverage boundary

Where a fact ages or a map runs out.

P-6Status fails closedMissing evidence, policy files, digests, or self-scans block or demote; a downstream projection can explain a pass but can never upgrade a blocked source truth.

In plain termsA finished thing is only as sound as its weakest part. If one part has no evidence behind it, the whole is treated as not-ready, not assumed fine. A later step can downgrade that verdict but cannot lift it unless fresh work earns the rise.

AnalogyA building cannot be signed off for occupancy until every trade (wiring, plumbing, fire safety) has passed; if the fire inspection was never done, the building stays unfit, and a later office walk-through can flag a new fault but cannot grant occupancy on its own.composite status is the meet of its partsis likethe building is fit only if every trade passes; the worst trade decides the wholea part with no evidence defaults to blockedis likea trade with no inspection on file counts as failed, not as quietly finea later stage may lower status but not raise it without a new derivationis likea later walk-through can downgrade the building but cannot grant occupancy without a fresh passing inspectionWhere the analogy breaksThis shows why an un-inspected part drags the whole down and why a downstream check cannot upgrade it; it does not establish that the building is actually safe, only that the sign-off chain has no gaps. One full chain of passes is not a promise that nothing was missed.

Why it mattersIt means a missing check or skipped scan cannot quietly pass as approval, so silence has a cost instead of being read as a clean result.

Potential misreadingThat an absent or unchecked part is harmless and can be treated as a pass, or that a downstream view can promote something that was blocked underneath it.

P-6 is AX-5 turned into the default a builder relies on when evidence is absent rather than negative. The status of a composite is the meet of its parts, so a single missing policy file, source digest, secret scan, negative case, or result self-scan pulls the whole verdict down to blocked instead of leaving a gap that silently reads as pass. The bite is in the asymmetry: a later stage may lower a status freely, but it cannot raise one without a fresh derivation, which is exactly why a downstream view can explain why something passed yet can never upgrade a source truth that was blocked underneath it. This is the principle that makes silence cost something, and it is what lets the claim and evidence model treat an unscanned or unproven input as the bottom of the order rather than a weak yes.

Formal statementstatus(c) = ⨅pparts(c) status(p)  ∧  ∀  pparts(c). (evidence(p) = ∅ ⇒ status(p) = ⊥)  ∧  (status'(c) ⊐ status(c) ⇒ ∃  d. derives(d, status'(c)))A composite's status is the meet of its parts' statuses; every part with no evidence sits at blocked; and a later status may exceed the earlier one only when some fresh derivation establishes the rise.statusthe status assigned to a composite or part, ordered with blocked at the bottomca composite whose status is being computedmeet: the weakest of the part statusespa part the composite is built fromparts(c)the parts the composite is built fromevidence(p)the admissible evidence held for that partno admissible evidence for that partblocked, the bottom of the status orderstatus'(c)a later status proposed for the same compositeclaims a strictly higher status thanda fresh derivationderives(d, status'(c))derivation d establishes the higher status
GovernsThe status boundary, where a composite verdict is assembled from parts and absence is tempted to read as pass.
RequiresTaking the composite status as the meet of its parts, defaulting any part with no evidence to blocked, and demanding a new derivation before any later stage raises a status.
RefusesA silent default pass: letting missing evidence, an absent scan, or a downstream view lift a blocked part to green without a fresh derivation.

In practiceThe formal-math readiness gate computes its verdict as the meet of its inputs, so when the corpus or a required check is absent it reports blocked rather than ready, and a later projection cannot lift that boundary to passing.

Enforced inFormal Math Readiness Gate Cold Evaluation Honesty Bundle Corpus Readiness Mathlib Absence Gate

The tempting mistakeA status board shows a component as green because no scan reported a problem, treating an absent check as a pass and letting a downstream summary stand in for evidence that was never produced.

Grounded inAX-5

Scope limitFailing closed on missing evidence does not establish any part is correct or that the composite is complete; it only fixes the default so absence lands at blocked rather than passing, and the example here illustrates that default without computing support for the principle or its grounding axiom.

Source JSON · Show relationships →

P-7Track known unknowns without claiming the unknown is mappedCoverage names its declared domains and its open gaps; it must not report unmapped space as safe, complete, or exhausted.

In plain termsA coverage report can only speak about the area it actually checked, and must name the area and the gaps it found. Anything outside that area is unknown, not declared safe, complete, or irrelevant.

AnalogyA library catalogue lists the shelves it has actually indexed; a book not in the catalogue might exist on an un-indexed shelf, so the catalogue saying nothing about it means not yet checked, not confirmed absent.coverage holds only over a declared finite domainis likethe catalogue speaks only for the shelves it has indexed, and those shelves are listeditems outside the domain are unknown, not proven-absentis likea title missing from the catalogue is not-yet-indexed, bounded evidence the library lacks itabsence of a finding is not a claim of safety or completenessis likean empty search result means this catalogue did not find it, not that it cannot exist anywhereWhere the analogy breaksThis shows why a blank result outside the indexed shelves means unknown, not absent; it does not establish that the un-indexed shelves are empty or full, only that the catalogue makes no claim about them. A clean catalogue is not a statement that the whole library was checked.

Why it mattersIt stops a tidy report with no findings from being read as everything is fine, when all it really showed is that nothing was looked at outside its declared scope.

Potential misreadingThat a report finding no problems means the unchecked area is clear, complete, or safe, rather than simply unexamined.

P-7 is AX-6 open-world epistemics turned into a reporting discipline. A coverage report may draw a closed-world conclusion only inside a declared finite domain; outside that boundary an item is unknown, and unknown is held distinct from proven-absent, so a silence in the records is never read as a fact about the world. This bites because the cheap move is to let blank space mean clear: a tidy report with no findings reads as everything is fine, when all it established is that nothing was checked there. It connects to the claim and evidence model directly, since a completeness statement is itself a claim that has to cite its declared loci and evidence rather than assert exhaustiveness, which is why unknown sits as its own coverage tag and is never collapsed into the bottom of the evidence order.

Formal statementcovers(r, d)  ⇒  declared(d)  ∧  (∀  xd. status(r, x) = unknown)  ∧  unknown ≠ ⊥If a report concludes coverage over a domain, that domain must be declared and finite; for anything outside it the report's status is unknown, and unknown is not the same as proven-absent.coversthe report concludes coverage over a domainra coverage reportdthe declared finite domain it coversdeclaredthe domain is explicitly declared and finitexan item, possibly outside the declared domainstatuswhat the report says about an itemunknownthe coverage tag for anything outside the declared domainthe bottom of the evidence order, i.e. proven-absent or false
GovernsThe coverage-and-completeness boundary, where a report is tempted to read its own silence as a clean result.
RequiresNaming the declared finite domain and the gaps actually found, and marking everything outside that domain unknown rather than safe, complete, or exhausted.
RefusesConverting absence of a finding into a claim that the unmapped space is safe, complete, exhausted, or irrelevant.

In practiceThe self-ignorance coverage ledger records what was checked, names the gaps it found as open items, and keeps a case that fails when missing coverage is read as a clean result, so a blank region cannot be reported as cleared.

Enforced inSelf Ignorance Coverage Ledger Doctrine Fact Claim Audit

The tempting mistakeA report scans a handful of components, finds nothing, and prints the whole area as clear, treating untouched space as evidence that nothing is wrong there.

Grounded inAX-6

Scope limitMarking the unmapped space unknown does not begin to map it. The gap stays open and the report stays bounded to its declared domain; this principle inherits no authority beyond the specific obligations it operationalises, and the example illustrates the rule without counting as support for it.

Source JSON · Show relationships →

P-11Bind volatile facts to refresh routesA live count or current state cites how it can be re-derived, or it stays out of durable prose as a dated snapshot.

In plain termsA number about something that keeps changing, like a current count or a readiness status, may only sit in a lasting document if it says when it was read and points to a way to work it out again. Otherwise it should be marked as a dated snapshot.

AnalogyA train departure board can post a time only because it shows when it last refreshed and recomputes from the live feed; a time painted permanently on the wall, with no refresh, stops being trustworthy the moment the schedule changes.a live count or readiness signalis likethe departure time shown for a trainthe read time carried with the valueis likethe 'last updated' stamp on the boardthe route that re-derives it from its basisis likethe board's link back to the live schedule feed it recomputes fromdemoting an unbound value to a dated snapshotis liketreating a time painted on the wall as a fixed past notice, not a live departure timeWhere the analogy breaksThe board only shows that a changing value needs a timestamp and a live source to stay honest; it does not show the posted time is correct right now, and seeing a refresh link does not mean the value has actually been recomputed since.

Why it mattersA frozen 'current' number quietly drifts from reality as the underlying thing grows or changes, so readers keep trusting yesterday's reading as today's truth with nothing pulling it back into line.

Potential misreadingAssuming a confident number in a document is current just because it sounds definite. The point that carries the weight is the route to recount it; without that, the figure is just a cached reading wearing the costume of a fixed fact.

P-11 is AX-10 turned into a writing discipline: a number about live state is a cached read, not a standing fact, and a cached read is only as trustworthy as its invalidation contract. So counts, "current" states, route totals, CI floors, and readiness signals are admissible in durable prose only when they carry the time they were read, the basis they came from, and a route that re-derives them; if any of those is missing, the honest form is a dated snapshot or no claim at all. This connects to the claim and evidence model because an unbound live value is the temporal version of an echoed label: it keeps asserting yesterday's reading as today's truth with nothing recomputing it. The route is the load-bearing half; without it a confident number silently drifts away from the basis it was supposed to track.

Formal statementdurable(v)  ⇒  ∃  t, B, ρ. carries(v, ⟨ t, B, ρ ⟩)   else demote(v)A volatile value may stand in durable prose only when it carries a read time, a basis, and a route that can recompute it; otherwise demote it to a dated snapshot or keep it out. Carrying the route makes the number checkable; it does not make it currently fresh.durable(v)the value v stands in durable proseva volatile value such as a count, current state, route total, CI floor, or readiness signaltthe time the value was read, carried as its as-of stampBthe basis the value was read fromρthe route that re-derives the value from the basiscarries(v, ⟨ t, B, ρ ⟩)the value is stamped with its read time, basis, and recompute routedemote(v)mark v as a dated snapshot or keep it out of durable prose
GovernsThe temporal boundary, where a live reading is tempted to harden into a standing fact.
RequiresA read time, a basis, and a recompute route carried with any live count or readiness signal, or demotion to a dated snapshot when one is missing.
RefusesA frozen live count or "current" state asserted in durable prose with no read time and no route to re-derive it.

In practiceThe doctrine fact-claim audit checks that public fact rows state the expected count, point at the live code they were read from, and only cite facts present in the fixture graph, so a volatile number without a recompute basis is blocked rather than printed as standing truth.

Enforced inDoctrine Fact Claim Audit Self Ignorance Coverage Ledger

The tempting mistakeA page states "47 components" as a flat fact, with no read time and no route to recount, so the number keeps asserting itself unchanged after the underlying set has grown.

Grounded inAX-10

Scope limitBinding a number to a refresh route does not make the principle a witness for AX-10, and it does not establish the cited value is currently fresh; it operationalises specific freshness obligations and gives the reader a way to recompute, leaving the live reading to be re-derived rather than trusted.

Source JSON · Show relationships →

P-19Classify residual pressure before wiringA missing neighbour is typed pressure, not an edge; it becomes an edge only when the current source row names the relation and the target resolves, and the same floor governs both directions between doctrine and the system.

In plain termsA missing link in the map is not an empty space to fill in; it is a noted gap with a type. You only draw the link once a current source actually names it and the target really exists.

AnalogyA transit map does not draw a line between two stations just because they sit near each other. The line goes in only when a real service runs it.the missing relation as typed residual pressureis likea known gap on the map, marked but not yet a linethe edge admitted only when a source names it and the target resolvesis likethe line drawn only when a real, scheduled service connects the stationsWhere the analogy breaksThe transit-map picture shows that a connection needs a real service, not nearness; it does not capture the typed record the gap carries while it waits, which is more than a blank.

Why it mattersIt keeps the system's own map honest as it grows, instead of inventing connections that make a diagram look complete.

Potential misreadingThat a plausible-looking connection is a real one. Nearness or a shared name is pressure to check, not a link.

P-19 is the discipline that keeps the system's own map honest as it grows. A missing neighbour in the lattice is a typed residual pressure, not a fact: before anyone wires it, classify the declared domain, the source row, the target resolution, the fillability, the evidence floor, and the scope boundary. A candidate route, a basename match, a singleton guess, or a stale projection row is still pressure; it becomes an edge only when a current source row names the relation and the target resolves under the builder. The same floor runs in both directions between the doctrine and the system it governs: a law constrains the system through source-derived edges, and the system can refine a law only through source-owned obligations, witnesses, negative cases, and unfinished-coverage rows. Neither direction is support proof, and neither is permission to launder pressure into an edge or to whiten a health card.

Formal statementeE  ⇒  source(e)  ∧  resolves(τ(e));   else eR  ∧  typed(e)An edge is admitted only when a current source row names it and its target resolves under the builder; naming alone does not force admission, and anything short of that is not absence but typed residual pressure in R, carrying its declared domain, evidence floor, and scope boundary until a source row resolves it.ea candidate relationEthe admitted edgessource(e)a current source row names the relationresolves(τ(e))the target resolves under the builderτ(e)the target the relation points atRthe typed residual-pressure set: pressure, not an edge yettyped(e)the residual carries a declared domain, source row, target, fillability, evidence floor, and scope boundary
GovernsThe time-and-coverage boundary, where the map is tempted to fill a gap it cannot yet justify.
RequiresClassifying a missing neighbour as typed pressure with a declared domain, source row, target resolution, and evidence floor before any wiring.
RefusesPromoting a guess, a basename match, or a generated hint into an edge, in either direction between doctrine and the system.

In practiceThe drift control room reports where a projection has wandered from its source as a typed pressure to re-derive, rather than quietly rewriting the edge to make the card look complete.

Enforced inWorld Model Projection Drift Control Room Self Ignorance Coverage Ledger

The tempting mistakeA builder adds a lattice edge because two ids share a basename, turning a naming coincidence into a claimed relationship.

Grounded inAX-5 AX-6 AX-11

Scope limitClassifying a residual does not resolve it. The gap stays open and computable until a source row names the relation; the classification just stops it from being faked.

Source JSON · Show relationships →

Doctrine and record boundary

Where doctrine governs its own records.

P-12Make doctrine executable before authoritativeA doctrine surface earns authority through grammar, required fields, result records, and validator coverage; prose can orient a reader but cannot become source authority.

In plain termsA written rule is only allowed to actually govern other parts of the system after it passes a machine check of its form and carries its required parts and its stated limits. Well-written words on their own can guide a reader but cannot rule.

AnalogyA 'this room meets code' notice on a door can only govern who is allowed in after it passes a coded building inspection with all required sign-offs and stated limits; a convincingly worded sign that no inspector ever ran against the code just orients people, it excludes entry.a doctrine surface the system may treat as a ruleis likethe 'meets code' notice on the doorpassing the executable grammaris likepassing the coded building inspectionthe required fields and result-record obligationsis likethe required sign-offs the inspection demandsthe declared scope boundaries, its stated boundsis likethe notice stating what it does and does not certifyprose held at projection, orients but does not governis likea nicely worded but uninspected sign that informs but cannot authorise entryWhere the analogy breaksThe inspection picture only shows a notice must clear a real check before it can govern; it does not show what the notice says is true, that the room is actually well-built, or that the building code itself is complete.

Why it mattersIt stops a persuasive paragraph from being treated as the law other parts must obey, which is exactly where confident but unchecked wording smuggles authority it never earned.

Potential misreadingBelieving that clear, authoritative-sounding writing is enough to make something a binding rule. Passing the form check means the rule is well-formed enough to carry authority, not that its content is correct.

P-12 is the discipline that decides when a piece of doctrine is allowed to govern rather than merely describe. A standard, a route contract, or a doctrine record earns authority only when an executable grammar accepts it and it carries the required fields, result-record obligations, and scope boundaries; well-written prose can orient a reader but cannot become the thing other components are checked against. This is the claim-and-evidence model pointed inward at the system's own laws: an authority-bearing surface is treated as a claim that has to clear an admissibility floor, so a confident paragraph sits at the bottom of that order until a grammar membership check and its obligations admit it. P-12 only operationalizes specific obligations of its grounding axiom; passing the grammar establishes that a surface is well-formed enough to carry authority, not that what it asserts is true or that the doctrine it belongs to is complete.

Formal statementauth(d)  ⇒  dL(G)  ∧  records(d)  ∧  anticlaims(d);   otherwise auth(d) ⊑ projA doctrine surface may carry authority only when an executable grammar accepts it and it carries result-record obligations and scope boundaries; otherwise its standing is bounded at projection, which orients but does not rule.da doctrine surface (standard, route contract, record)auth(d)the authority the surface is allowed to carryL(G)the language of the executable grammar that must accept itrecords(d)the result-record obligations the surface declaresanticlaims(d)the stated bounds on what it does not establishprojprojection standing: orients a reader, does not govern
GovernsWhen a doctrine surface is allowed to govern other components rather than only describe them.
RequiresGrammar membership plus declared required fields, result-record obligations, and scope boundaries before a surface carries authority.
RefusesLetting unstructured prose acquire governing authority without passing the executable contract.

In practiceThe executable doctrine grammar admits a standard as authority-bearing only when it parses under the grammar and carries its required fields, result-record obligations, and scope boundaries, so a doctrine surface that is only prose is held at projection instead of being allowed to govern.

Enforced inExecutable Doctrine Grammar Standards Meta Diagnostics Release Public Wording Gate

The tempting mistakeA persuasive markdown standard is treated as the rule other components must satisfy, even though nothing parses it against a grammar and it carries no result-record obligations or scope boundaries.

Grounded inAX-11

Scope limitPassing the grammar does not make a doctrine surface true, strong, or its doctrine complete, and it does not make this principle a witness for its grounding axiom; it admits the surface as well-formed authority and inherits no support beyond the specific obligations it operationalizes.

Source JSON · Show relationships →

P-13Apply the same floor to meta artifactsMicrocosm's own standards, modules, ledgers, and launch claims meet the same evidence, scope boundary, and refusal floors they impose on every other shard.

In plain termsWhen the system describes or assesses itself, that self-description has to clear exactly the same evidence and honesty standard it forces on everything else. The part that talks about the system gets no easier pass.

AnalogyA calibration lab's own measuring instruments have to pass the very same calibration check it certifies for its customers' equipment; the lab does not get to sign off its own gauges under a looser standard than it applies to everyone else's.the system's own meta artifacts describing itselfis likethe lab's own in-house measuring instrumentsthe evidence, scope boundary, and refusal flooris likethe calibration standard being appliedthe same floor applied to external work it auditsis likethe same standard applied to the customers' equipment the lab certifiesrefusing a meta-artifact exemptionis likerefusing to let the lab sign off its own gauges under a looser ruleWhere the analogy breaksThe calibration picture only shows the lab's own instruments face the same standard as customer equipment; it does not show the lab's instruments are actually accurate or its results correct, only that its self-checks were not waved through on a lighter rule.

Why it mattersSelf-referential copy is where overclaiming is easiest to hide, so removing the discount lets the system state its own limits in public without that statement quietly becoming a new unchecked claim.

Potential misreadingAssuming a system describing itself can be taken at its word, or that holding its self-claims to the standard makes the self-praise correct. Clearing the floor only removes the special pleading; it does not make the system complete or ready.

P-13 is AX-12 turned into a build habit: the standards, paper modules, ledgers, routes, generated views, and launch wording the system produces about itself must clear the same floor those same artifacts impose on any other shard. It bites because self-referential copy is where overclaiming is easiest to smuggle in; a page describing the system is still a claim, and a confident self-assessment that would never survive the evidence floor it applies elsewhere is exactly the special pleading this principle removes. It connects straight to the claim and evidence model: a meta artifact's wording is admissible only under the same recompute-or-demote check as external work, and the wording gate that polices other shards is pointed back at the system's own launch copy. Removing the exemption is what lets the system state its own limits in public without that statement quietly becoming a new unchecked claim.

Formal statement∀  aM. ∀  φ ∈ claims(a). floor(φ) = floorext(φ)For every meta artifact the system produces about itself and every claim that artifact carries, the claim must clear the same evidence, scope boundary, and refusal floor as an external claim.Mthe system's meta artifacts: its own standards, paper modules, ledgers, routes, generated projections, and launch wordingaany such meta artifactφa claim carried by the artifact aclaims(a)the claims that artifact a carriesfloorthe evidence, scope boundary, and refusal floor from AX-12floorextthe same floor applied to an external claim
GovernsThe meta boundary, where the system makes claims about itself and is tempted to discount them.
RequiresHolding standards, paper modules, ledgers, routes, generated views, and launch wording to the same evidence, scope boundary, and refusal floor imposed on any other shard.
RefusesA meta-artifact exemption, where the system's own copy gets a lighter floor than the work it audits.

In practiceThe launch wording gate runs the same claim-language floor over the system's own public copy that it imposes on any other shard, so overclaiming language in a self-description is blocked at launch rather than waved through.

Enforced inRelease Public Wording Gate Executable Doctrine Grammar Voice To Doctrine Self Improvement Loop

The tempting mistakeThe system publishes a self-assessment calling its own work verified and complete, in wording that would never clear the evidence floor it applies to the shards it audits.

Grounded inAX-12

Scope limitApplying the floor to the system's own artifacts does not make the system complete, correct, or launch-ready, and it does not make this principle a witness for AX-12. It operationalises specific AX-12 obligations and inherits no authority beyond them; the limits remain, stated rather than hidden.

Source JSON · Show relationships →

P-17Anchor graph mutations to unique source rowsBefore adding or removing a lattice edge, anchor the change to the unique source row, target id, and builder route that will consume it; a count delta or a nearby key is not a basis.

In plain termsBefore adding or removing a connection in a list of relationships, you must point to the exact source entry that names that relationship and the place that will use it. A nearby similar entry, or a count that went up by one, is not good enough to act on.

AnalogyBefore adding a connecting flight to a booking, the agent has to point to the exact scheduled service for that date and route. A flight that merely has a similar number, or the fact that the timetable lists one more service, does not justify booking the seat.the unique source row that names the relationis likethe exact scheduled service for that date and routea nearby repeated key or count delta is not a substituteis likea similar flight number or a timetable that lists one more service is not the bookingthe target id and builder route the edge will feedis likethe specific booking the connecting seat is attached toWhere the analogy breaksThe booking picture only shows that a connection must trace to one exact entry, not an approximate one; it does not establish that the entry itself is right, and it does not capture every check a real edge addition runs.

Why it mattersIn a list where many entries look alike, acting on a near-match or a changed total quietly wires up the wrong relationship, and the mistake is hard to find later.

Potential misreadingThat a close match or a count that moved confirms the right connection. Only the exact entry that names the relationship does; everything else is a guess that happens to look right.

P-17 governs the write side of the lattice: the moment an edge is added to or removed from a registry whose rows look alike, the mutation has to point at the one source row, target id, and builder route that will actually consume it. It bites because repeated registries are exactly where a builder is tempted to act on the cheap signal instead of the basis: a generated count went up, a nearby key has the same shape, a projection already shows the edge, so the edge must be real. P-17 composes three obligations to close that gap; the row's content basis must be declared and recomputed when it drifts, the mutation must declare its effect boundary and check the parent state it claims to write under a single owner, and the resulting edge must be admissible under the grammar with result records rather than asserted in prose. It connects to the claim and authority model directly: an edge is a claim about a relationship, so it inherits the floor that a claim is admissible only against a recomputed basis, and a generated view of the registry can expose that basis but never stand in for it.

Formal statementmutate(e)  ⇒  ∃!  r. row(e) = r  ∧  declared(basis(r))  ∧  parent(e) = cas(r)  ∧  grammar(e)An edge mutation is admitted only when exactly one source row carries it, that row's content basis is declared, the mutation writes against the row's current parent state, and the resulting edge is grammar-admissible.mutate(e)an edge is added to or removed from a registry of look-alike rowsethe lattice edge being added or removed∃!  rexactly one source rowrow(e)the source row that carries the edgedeclared(basis(r))the row's content basis is declared and recomputed on drift (AX-4)parent(e)the parent state the writer commits the edge againstcas(r)the row's current compare-and-swap parent state under a single writer (AX-9)grammar(e)the resulting edge is admissible under the executable grammar (AX-11)
GovernsThe mutation boundary, where an edge enters or leaves a registry of look-alike rows.
RequiresA unique source row with a declared content basis, a mutation scoped to that row's parent state under a single writer, and grammar admissibility for the resulting edge.
RefusesAnchoring an edge to a generated projection, a count delta, or a nearby repeated key instead of the row that owns it.

In practiceThe source-import protocol brings each relation in against a named manifest row and digest and writes it under a declared boundary, so an edge lands only where a current source row carries it rather than where a count or a similar key suggests it.

Enforced inSource Projection Import Protocol Mission Transaction Work Spine Concurrency Mission Control

The tempting mistakeA builder adds a lattice edge because the generated registry reports one more neighbour, treating the count delta as the basis rather than finding the source row that would justify the edge.

Grounded inAX-4 AX-9 AX-11

Scope limitAnchoring a mutation to its source row does not make the edge itself correct, nor does it make this principle a witness for AX-4, AX-9, or AX-11; it operationalises specific obligations of those axioms and inherits no authority beyond them. The example illustrates the rule for a reader and never counts as support that the obligations are covered.

Source JSON · Show relationships →

P-20Bind result records before record authorityA doctrine record is not active by projection alone; bind its validator records, evidence refs, omissions, and scope boundaries before its data or public copy counts as current.

In plain termsA record does not become the trusted version just because a readable copy of it exists. The evidence that its checks passed, the references to its evidence, what it leaves out, and how far it is allowed to claim all have to be attached to the record first.

AnalogyA medicine is not cleared for the shelf just because a printed information leaflet for it exists. The test results, the list of what was tested, the known side effects, and the approved use all have to be attached to that medicine before it can be dispensed.binding validator results to the record before it is authoritativeis likeattaching the test results before the medicine is clearedevidence refs and stated omissions on the recordis likethe list of what was tested and the known side effects travelling with the medicinethe scope limit bound on the recordis likethe approved use that limits what the medicine may be dispensed forWhere the analogy breaksThe medicine-clearance picture only shows that the supporting records must be attached before use; it does not establish that the underlying tests were good, and it does not capture that a readable leaflet, however well written, never raises what the medicine is cleared to do.

Why it mattersIt stops a nicely formatted record from being treated as the trusted source when the checks, evidence, and limits that would back it have not actually been attached.

Potential misreadingThat a clear, complete-looking record is therefore authoritative. The readable copy is a projection; authority comes only from the checks and limits bound to the record, not from how it reads.

P-20 is the discipline that stops a doctrine record from being trusted just because it exists on disk. A record being present as JSON, a markdown projection, a routing edge, or a line of public copy says nothing about whether it may be read back as current authority; authority is conferred only once the binding set is attached and recomputed: the validator result records, the evidence refs, the declared omissions, the scope boundaries, and the scope limit the record may carry. This is the admissibility floor from AX-1 applied to the system's own doctrine, and AX-12 is why there is no shortcut: a doctrine record is one of the system's own claims, so it passes the same gate it imposes on any external claim, with no meta-layer exemption. The body and the projections inherit nothing from sitting next to a confident heading; until the result records are bound, the record is a projection held below its source, which is exactly why the page you are reading keeps stating what it cannot yet treat as authoritative.

Formal statementauth(r)  ⇒  bound(r, rec)  ∧  bound(r, evid)  ∧  bound(r, omit)  ∧  bound(r, anti)  ∧  bound(r, ceil)A doctrine record may be read as current authority only when it carries its bound result records, evidence refs, declared omissions, scope boundaries, and scope limit; missing any of these, it stays a projection below its source.auth(r)reading the record back as current system authorityra doctrine record: its JSON, markdown, routing edge, or public copybound(r, rec)the validator result records are bound on the record (AX-11)evidthe evidence refs bound on the recordomitthe declared omissions bound on the recordantithe scope boundaries bound on the recordceilthe scope limit, the scope limit the record may carry (AX-12)
GovernsThe record-and-authority boundary, between a doctrine record existing and being read back as current authority.
RequiresBinding the validator result records, evidence refs, omissions, scope boundaries, and scope limit on a record before any of its projections is treated as current authority.
RefusesReading a record's JSON, markdown, routing edge, or public copy as authoritative on the strength of its existence, before the result records are bound.

In practiceThe launch wording gate runs the same claim-language floor over the system's own doctrine copy that it imposes on any other shard, so a record's public line cannot carry authority its bound checks do not support.

Enforced inRelease Public Wording Gate Executable Doctrine Grammar Doctrine Fact Claim Audit

The tempting mistakeA generated doctrine card is cited as the current authority for a rule because the JSON exists and the heading reads confidently, with no validator result records, omissions, or scope limit bound behind it.

Grounded inAX-11 AX-12

Scope limitBinding result records to a doctrine record does not make the record correct, witnessed, or complete; it only stops the record from carrying authority its bound checks do not support. The example illustrates the rule and never counts as support for it.

Source JSON · Show relationships →

Doctrine and the system refine each other

Doctrine constrains the system, and the system shows where the doctrine is underspecified. The two refine each other, and the return path is kept deliberately narrow.

Axioms reach the system through governance edges: they constrain component rows, ground principle commitments, and name the anti-principles that guard them. Governance edges do not by themselves compute support. The system reaches back only through source-owned change: a witness component, a negative case, an unfinished-coverage row, or a revised obligation can refine an obligation's grammar or an evidence ceiling, while a generated projection, a nearby example, or an attractive analogy cannot. A missing relation stays recorded pressure until the current source row names it, and feedback can refine how a law is expressed but can never silently un-admit it.

What doctrine refuses

The anti-principles are doctrine read in the negative, the named shortcuts the system refuses on sight. They are often the fastest way into the doctrine: if the axioms say what Microcosm is and the principles say what it does at a boundary, the anti-principles say what it will not let you get away with. Each card names the rejected shape and the axioms it guards.

Trusting the wrong thing

AP-1Fixture-label echoEchoing a fixture verdict, registry label, or model answer as truth instead of recomputing it from lower-level evidence.

In plain termsThe mistake of repeating a stored verdict, label, or model answer as if it were true, without re-deriving it from the underlying evidence.

AnalogyReading yesterday's 'sold out' sign on a shop and repeating it as today's truth, without checking whether the shelves were restocked overnight.the echoed verdict or labelis likeyesterday's sign you simply repeatthe missing recomputation from the evidenceis likethe shelf-check nobody actually didWhere the analogy breaksThe stale-sign picture shows label-echo; it does not name the deeper rule, which is that the underlying evidence, not the sign, is what a verdict has to be re-derived from.

Why it mattersIt is the most common way false confidence spreads: a single unverified label gets quoted as fact all the way downstream.

Potential misreadingThat a label being present means it was checked. The label is just text until something recomputes the verdict beneath it.

AP-1 is the failure AX-1 exists to refuse: taking a declared verdict at face value because it is written down. It is tempting because echoing is cheap and usually looks right, so a pipeline that repeats labels passes its own tests while proving nothing. The repair is not subtle: recompute the verdict from the evidence underneath and keep a negative fixture that fails when the echo is wrong. If you cannot recompute it, the honest output is a lower claim, not a confident repeat.

Formal statementemit(v)  ∧  ¬ ∃  K. K(B) = vEmitting a value v as a verdict while no checker recomputes v from the basis.emit(v)emitting v as a verdict by repeating itva declared label or verdictKa checker that would recompute itBthe basis it should derive from
GovernsThe claim boundary, where a label is mistaken for a derivation.
RequiresCatching the echo: a recomputed verdict and a negative fixture that fails.
RefusesRepeating a fixture verdict, registry label, markdown claim, or model answer as if repetition were proof.

In practiceA monitor replay deliberately feeds a mislabelled trace and confirms the recomputed verdict rejects it, so a wrong label cannot pass by being repeated.

Enforced inAgent Sabotage Scheming Monitor Replay Agent Benchmark Integrity Anti Gaming Replay

The tempting mistakeA dashboard shows a component as healthy because its own record said so, with no independent recomputation behind the green.

GuardsAX-1 AX-12

NegatesP-1 P-2 P-13 P-18 P-20

Scope limitGuarding against label echo is a floor under AX-1 and AX-12, not a positive proof that any specific claim is true.

Source JSON · Show relationships →

AP-2Producer trustTrusting a producer, persona, route, account secret, or prior success instead of a checker, proof, policy, or dereferenced capability.

In plain termsThe mistake of letting something through because of who sent it, what badge it carries, or that it worked last time, instead of independently checking that this request is actually allowed right now.

AnalogyA building guard waving someone through to a secure room because their face is familiar and they have an old pass, rather than checking the access system to confirm that person is cleared for that room today.trusting a claim because of its producer or account secretis likeletting the person in because the face is familiar and the pass looks rightthe independent checker or derived authority that should decide itis likelooking up the access system to confirm clearance for this room todaya prior green run or standing account secretis likethe old pass that worked last timeWhere the analogy breaksThis shows only that a familiar face is not the same as a confirmed permission. It does not establish the access system itself is correct, that every door in the building is checked this way, or that a confirmed person will behave well once inside.

Why it mattersIdentity is easy to fake or to go stale; a system that trusts the sender rather than re-checking the request looks fine until that sender is wrong or compromised, and by then nothing was actually guarding the door.

Potential misreadingThat a trusted name or a pass that worked before is a safe stand-in for checking. The check has to be made each time against what is actually allowed now.

AP-2 is the failure that AX-2 and AX-3 exist to refuse: granting trust because of who produced a claim or what badge they hold, rather than because something recomputed the claim or derived the authority. It bites because identity is cheap to read and usually correlates with correctness, so a system that trusts a known producer, a passing route, or a standing account secret looks fine right up until that producer is wrong or compromised, at which point nothing was actually checking. The repair splits trust from production: a small checker decides the claim over its certificate, and authority for an effect is derived from dereferenced tokens, policy, and proof references against current world state, never from ambient identity or a prior green run. This is the human-pressure analogue of the label echo in AP-1; here the unchecked thing is a source of authority rather than a written verdict.

Formal statement(trust(φ)  ∧  ¬ ∃  K. K(c) = accept)  ∨  (grant(s, e)  ∧  ¬ deref(auth(s, e)))Trusting a claim while no small checker accepts its certificate, or granting a subject an effect while authority for it was never derived by dereference from tokens, policy, and proof against world state.trust(φ)trusting claim varphi on the basis of its producer rather than a checkφa claim trusted on the basis of its producerKa small checker that would decide the certificatecthe certificate the checker should decidegrant(s, e)granting subject s the effect ederef(auth(s, e))authority derived by dereference from tokens, policy, and proof against world state
GovernsThe trust-and-authority boundary, where a producer's identity or a standing account secret is mistaken for a check or a derived right.
RequiresA small checker that decides the certificate, and authority for an effect derived by dereference from tokens, policy, and proof references against current world state.
RefusesTrusting a producer, persona, route, account secret, or prior success in place of a checker, proof, policy, or dereferenced capability.

In practiceThe tool-authority replay derives whether a call is permitted from the dereferenced capability and policy rather than from the caller's standing identity, so a known caller with no derived authority is refused.

Enforced inMCP Tool Authority Replay Proof Derived Governed Mutation Authorization Certificate Kernel Execution Lab

The tempting mistakeA mutation is allowed because the caller holds a long-lived account secret and the same route passed last time, with nothing dereferencing current authority or recomputing the claim behind it.

GuardsAX-2 AX-3

NegatesP-3 P-4 P-16 P-18

Scope limitRefusing producer trust at these witnesses is a floor under AX-2 and AX-3, not positive proof that any granted authority or accepted claim is correct. The example is reader illustration and computes no support; catching identity-based trust in named places does not establish that authority is correctly derived everywhere.

Source JSON · Show relationships →

AP-6Inadmissible number emissionEmitting a number or conclusion when the precondition fails or a dependency is missing, instead of a typed refusal that carries its reason and evidence.

In plain termsThe mistake of producing a number anyway when the thing it needs to be valid is missing, instead of clearly saying 'I cannot answer this and here is why'.

AnalogyA pharmacist guessing and dispensing a dose when the patient's weight, the one input the formula needs, is missing, instead of stopping and saying the dose cannot be worked out yet.a precondition that does not holdis likethe missing patient weight the dose formula requiresemitting a value anyway to keep goingis likeguessing and handing over a dose regardlessa typed refusal carrying its reason and evidenceis likea written note saying 'dose not computed: weight missing' instead of a numberWhere the analogy breaksThis shows only that a missing input should produce an explicit refusal, not a made-up answer. It does not establish that a dose computed with all the right inputs is correct, and a refusal is not itself a treatment.

Why it mattersA fabricated number looks just like a real one downstream, so a statistic computed outside its valid range slides into later steps that trust it, while an honest refusal stops the bad value at the door.

Potential misreadingThat returning some number is more helpful than refusing. A number produced when its inputs are missing is worse than a refusal, because it hides as a usable result.

AP-6 is the failure AX-7 exists to refuse: when a computation's precondition does not hold, or a library it needs is absent, the code returns a number anyway instead of a typed refusal that names why it could not answer. It is tempting because a refusal reads as a red path and a number keeps the pipeline green, so a finance statistic computed past its valid sample size, or a silent NaN, slides downstream wearing the same shape as a real result. In the claim model that emitted number is a bare assertion with no admissible basis: it sits at the bottom of the evidence order, but unlike an honest gap it hides as a value later steps will trust. The repair is to totalize the partial function, return Ok only under a declared precondition and otherwise a refusal carrying a reason and the evidence for it, so the absence of an answer becomes a checkable typed object rather than a fabricated one.

Formal statement¬ Pre(x)  ∧  emit(g(x)) = y  ∧  yRefusal(r, e)The precondition fails, yet the computation emits a value y instead of a refusal carrying a reason and its evidence.Pre(x)the declared precondition the computation needs to holdemit(g(x))emitting the partial computation's value as a resultg(x)the partial computation on input xyan emitted number or conclusionRefusal(r, e)a typed refusal carrying a reason r and evidence e
GovernsThe boundary where a partial computation must either answer under its precondition or refuse.
RequiresCatching the inadmissible value: a totalized result that returns Ok only under a declared precondition and otherwise a refusal carrying a reason and evidence.
RefusesEmitting a meaningless statistic, a silent NaN, or an out-of-domain conclusion just to keep a green path.

In practiceThe finance forecast evaluation component returns a typed refusal when a forecast horizon reaches or exceeds the sample size, or when the statistics dependency it needs is unavailable, rather than reporting a number computed outside its valid range.

Enforced inFinance Forecast Evaluation Spine Corpus Readiness Mathlib Absence Gate

The tempting mistakeA statistics routine returns a coefficient computed past its valid sample size, and a downstream summary reports it as a normal result because it arrived as a number and not as a refusal.

GuardsAX-7

NegatesP-8

Scope limitRefusing one inadmissible emission at a named site does not establish a computation total or its in-domain numbers correct. It keeps the absence of an answer honest; the value it does return is still only as strong as the basis and check beneath it, and this record and its example never count as support for that.

Source JSON · Show relationships →

AP-15Mechanism theaterBorrowing field vocabulary like proof, verifier, or world model when the public mechanism only validates the shape of a record.

In plain termsThe mistake of using strong words like 'verifier' or 'world model' for something that only checks the shape of a record, not the claim those words promise.

AnalogyCalling a quick glance at a passport photo a 'full background check'. The name promises far more scrutiny than the glance actually performs.the strong borrowed word (verifier, world model)is likethe label 'full background check'the mechanism that only validates a record's shapeis likethe quick glance at the photoWhere the analogy breaksThe passport-glance picture shows the name-versus-action gap; it does not list which words are over-strong here, which depends on what the specific mechanism really decides.

Why it mattersStrong vocabulary makes a shape check sound far more rigorous than it is, so readers trust it more than it has earned.

Potential misreadingThat an impressive name reflects an impressive check. The name has to be earned by what the mechanism actually decides.

AP-15 is the overclaim the system polices in its own packaging. It is mechanism theater: using heavy field words, proof, verifier, information flow, world model, benchmark integrity, when the public mechanism behind them only checks that a record has the right shape. It is tempting because the vocabulary impresses, and the gap between "checks a schema" and "proves a property" is invisible to a casual reader. The repair is to name what the mechanism actually computes, hold the claim to that, and reserve the strong words for the few places that earn them, such as a real verifier run.

Formal statementname ∈ {proof, verifier, …}  ∧  checks(shape)  ∧  ¬ checks(claim)Using a strong field name drawn from words like proof or verifier while the mechanism checks only the shape of a record and not the claim that name implies.namethe borrowed field wordproofa strong field word the name may borrow, such as proofverifiera strong field word the name may borrow, such as verifierchecks(shape)the mechanism validates only the form of a recordshapethe form of a record, which the mechanism does checkchecks(claim)the mechanism would decide the property the word impliesclaimthe property the word implies, which it does not check
GovernsThe boundary between what a mechanism is named and what it actually decides.
RequiresNaming the real computation and holding the claim to it, with strong words reserved for mechanisms that earn them.
RefusesDressing a shape check in proof, verifier, or world-model language.

In practiceThe Lean witness compiles a tiny public example through a real verifier and caps its own claim at that bounded scope, rather than calling a schema check a proof.

Enforced inFormal Math Lean Proof Witness Certificate Kernel Execution Lab

The tempting mistakeA record-shape linter is described as a "world-model verifier", implying it reasons about the world when it only validates a fixture's fields.

GuardsAX-1 AX-2 AX-12

NegatesP-1 P-2 P-3 P-13 P-18 P-20

Scope limitRefusing mechanism theater does not upgrade the mechanism. It keeps the words honest; the underlying check is still only as strong as what it computes.

Source JSON · Show relationships →

Counting as proof

AP-3Rank-as-product-scoreReading a count, a handle, a passing validator, or an evidence-class name as product maturity, launch-scope decision, or whole-system correctness.

In plain termsThe mistake of reading a single summary number, like how many checks passed, as if it told you the whole thing is finished or ready, when parts you never measured could still be failing.

AnalogyReading a station board that says forty trains ran on time and concluding the whole network is running well, when several lines simply have no data on the board and could be down.a count or tally read as the standing of the wholeis likethe forty-on-time number read as the whole network being finea part with no admissible witness that should pin the whole lowis likea line with no data on the board that could be downthe honest status being the weakest part, not the averageis likethe network is only as good as its worst line, not the on-time countWhere the analogy breaksThis shows only that a flattering tally can hide an unmeasured part. It does not establish the lines that do report are running well, and it does not establish anything about lines the board never covered.

Why it mattersCounting passing checks as a maturity score quietly treats anything unmeasured as if it passed, so a project can look launch-ready while a required piece was never even tested.

Potential misreadingThat more passing checks always means more readiness. Extra passes only help if they cover a part that had no coverage before; repeating the same passing check adds nothing.

AP-3 is the roll-up fallacy the system polices in its own progress reporting: treating a number that summarises many parts as a verdict on the whole. A count of passing checks, a list of registered handles, a green validator, or a strong evidence-class label is a projection over an eight-component ceiling vector, and a high reading on one component can hide an uncovered provenance, freshness, or coverage component underneath it. This bites because it inverts how a composite is supposed to score: the honest status of a whole is the meet of its parts, where any part with no admissible witness sits at blocked, so a flattering average or a raw tally quietly reads a fail-open default as a pass. The repair is the count-theater rule: more passing cases raise standing only by covering a previously uncovered required obligation, lifting a sub-maximal ceiling component, or adding a missing negative case; redundant cases under the same basis are inert, and a rank stays a display of the ceiling, never the authority itself.

Formal statementreport(n)  ∧  n = |{ pass }|  ∧  (∃  p. status(p) = ⊥)  ∧  status(whole) ⊐ ⨅p status(p)Reporting a tally of passing parts as the standing of the whole while some part has no admissible witness, so the claimed status rises above the meet of the parts that an uncovered part should pin to the bottom.report(n)reporting the count n as the standing of the wholena count, tally, or rank reported as maturitypassa passing part counted into the tallypa part of the composite (an obligation or component)blocked: a part with no admissible witnessstatus(whole)the claimed standing of the whole compositep status(p)the meet over parts, the weakest part's statusclaims a higher standing than
GovernsThe progress-and-readiness boundary, where a summary number is tempted to stand in for the standing of the whole.
RequiresScoring a composite as the meet of its parts, defaulting an unwitnessed part to blocked, and raising standing only by covering an uncovered obligation, lifting a sub-maximal component, or adding a missing negative case.
RefusesTreating counts, handles, passing validators, or evidence-class names as product maturity, launch-scope decision, or whole-system correctness.

In practiceThe coverage ledger projects how many declared parts are actually materialised and keeps a case that forbids reading an absent entry as covered, so a coverage tally is exposed as a bounded count rather than a completeness claim.

Enforced inSelf Ignorance Coverage Ledger Release Public Wording Gate

The tempting mistakeA progress page reports that ninety checks pass and calls the system launch-ready, with several required parts carrying no witness at all and the unwitnessed gaps averaged away instead of pinning the whole to blocked.

GuardsAX-5 AX-12

NegatesP-2 P-6 P-13 P-15 P-18 P-19 P-20

Scope limitRefusing rank-as-score does not raise the standing of any part or make the composite correct. It only keeps the number honest as a projection of the ceiling; the parts beneath it carry exactly the support they were already shown to have, and an uncovered part stays blocked rather than counted.

Source JSON · Show relationships →

AP-5Unknown-unknown exhaustivenessReading a missing witness as a settled negative outside a declared finite domain, so absence of proof is reported as proof of absence.

In plain termsThe mistake of treating a place where you found nothing as a settled finding that nothing is there, when you may simply not have looked, or not looked everywhere.

AnalogyA doctor reading a region of a scan as 'all clear' when that region was never actually imaged, so 'we saw no problem' gets reported as 'there is no problem'.a missing witness, an evidence gapis likethe region of the body that was never imagedreading that gap as a settled negativeis likereading the un-imaged region as 'all clear'closing as a negative only inside a declared finite domain where every case is checkedis likebeing able to say 'clear' only for the area actually scanned end to endWhere the analogy breaksThis shows only that 'we found nothing' is not the same as 'there is nothing'. It does not establish whether the un-imaged region is actually healthy or not, and it does not turn a properly scanned clear area into a guarantee.

Why it mattersAn unexamined gap quietly reads as reassurance, so a coverage map can look finished when it has only stopped looking, hiding risk exactly where no one checked.

Potential misreadingThat a blank or absence is the same as a confirmed 'nothing here'. Absence of evidence is unknown, not a settled negative, unless the whole area was genuinely covered.

AP-5 is the failure AX-6 exists to refuse: turning a gap in evidence into a positive verdict of nothing-there. A required obligation with no admissible witness is an open coverage gap, not a refutation; it can be closed as a negative only inside a declared finite domain where every case is enumerable. This bites because it is the comfortable direction to round: a quiet absence reads as reassurance, and a coverage map that prints absent as clear looks finished when it has only stopped looking. It connects to the claim and evidence model through a distinction the system holds by construction: a missing witness is unknown, which is held separate from a value at the bottom of the evidence order, and unknown is kept distinct from a fail-closed block where an in-domain obligation has no admissible witness; collapsing any of these into proven-absent launders an open gap into a certified claim it cannot support.

Formal statementassert(proven(¬φ))  ∧  ¬ proven(φ)  ∧  ¬ finite(D)Reporting the negation of a claim as established while the claim is merely unproven and the domain was never declared finite, so an open gap is laundered into a settled negative.φa claim whose proof is missingassert(proven(¬φ))reporting the negation as an established findingproven(φ)an admissible derivation exists for the claimfinite(D)D is a declared finite domain where closed-world coverage is validDthe domain the reasoning ranges over
GovernsThe coverage boundary, where a missing witness is tempted into a settled negative.
RequiresHolding an uncovered obligation as an open gap, and closing it as a negative only inside a declared finite domain.
RefusesTreating absence of evidence as evidence of absence outside a declared closed domain.

In practiceThe coverage ledger records what the system has not established as an open gap with a declared scope, and keeps a case that fails if a blank is read as a clean negative, so an unexamined area cannot be reported as proven-absent.

Enforced inSelf Ignorance Coverage Ledger Doctrine Fact Claim Audit

The tempting mistakeA coverage map shows an area as clear because no failing case was found there, with no declared finite domain behind the closure, so an unsearched region is printed as a settled negative.

GuardsAX-6

NegatesP-7 P-19

Scope limitHolding a gap open as unknown does not establish the missing claim either way; it keeps the absence from becoming a false negative, and it grants no support, completeness, or coverage beyond the declared finite domain it names.

Source JSON · Show relationships →

Basis and freshness

AP-4Cache-across-driftReusing a cached result keyed on a name, path, route, label, or producer after the content it was derived from has changed underneath.

In plain termsThe mistake of reusing a saved answer that is filed under a name or address, after the actual thing behind that name has been changed or replaced.

AnalogyTrusting a library catalogue card that says a title sits on shelf B, when the original book was quietly swapped for a different edition and the card was never updated.a cached result kept under a stable handleis likethe catalogue card filed under the title and shelf locationthe basis content that has drifted underneath the handleis likethe book on the shelf, swapped for a different editionkeying reuse on a digest of the content, not the nameis likechecking the actual book on the shelf matches before trusting the cardWhere the analogy breaksThis shows only that a stable label can outlive the thing it points to. It does not establish every card in the catalogue is being checked this way, and one caught mismatch says nothing about whether the rest of the shelves are current.

Why it mattersPipelines reuse saved results by name to stay fast, but if the underlying source was edited, the name keeps returning yesterday's answer and nobody notices the value is stale.

Potential misreadingThat an unchanged name means unchanged content. The name can stay identical while what it points to has been replaced underneath.

AP-4 is the failure the determinism and freshness floors exist to refuse: trusting a stable handle as if it still stood for stable content. It is tempting because the handle does not visibly change when the basis drifts, so a name lookup, a route, or a producer keeps returning yesterday's answer and the pipeline looks fast and consistent while quietly serving a stale value. This connects to the claim and evidence model directly: a cached result is a claim over a basis, and if its basis has moved, the certificate that once admitted it no longer holds, so the value has dropped to bottom evidence even though the label reads unchanged. The repair is content-addressed identity: derive the cache key from a digest of the basis, reuse only when that digest matches, and on drift recompute or refuse rather than serve the old value by its handle.

Formal statementreuse(a)  ∧  key(a) = handle  ∧  H(Bnow) ≠ H(Bcached)Reusing a cached result by a stable handle when the digest of its basis differs from the digest it was cached under.aa cached result being reusedreuse(a)result a is served from cachekey(a)the key the cache is addressed byhandlea name, path, route, label, or producer used as the keyHa content digest of a basisBnowthe current basisBcachedthe basis the result was derived from
GovernsThe reuse boundary, where a stable handle is mistaken for stable content.
RequiresKeying reuse on a digest of the basis and recomputing or refusing when that digest drifts.
RefusesServing a cached result by name, path, route, label, or producer after its basis content has changed.

In practiceThe source-import protocol keys imported material on a content digest and refuses to reuse a copy when the source digest no longer matches, so a drifted source cannot be served by its old path.

Enforced inSource Projection Import Protocol Durable Agent Work Landing Replay Doctrine Fact Claim Audit

The tempting mistakeA view keeps serving a number by its route because the route is unchanged, long after the source it was computed from has been edited underneath it.

GuardsAX-4 AX-10

NegatesP-5 P-11 P-14 P-15 P-17

Scope limitCatching one stale-by-handle reuse at one digest boundary does not establish every cache in the system tracks its basis. This object and its example are reader illustration; they never count as support or proof that freshness holds across the graph, and the source records the freshness component as an open gap rather than a closed one.

Source JSON · Show relationships →

AP-9Frozen live factFreezing a count, a "current" state, or any live value into durable prose with no recorded time, basis, or way to re-derive it.

In plain termsThe mistake of writing a moving number or a 'current' status into permanent text as if it were a fixed fact, with no note of when it was read, what it was read from, and no way to recompute it.

AnalogyPrinting a train's departure time onto a permanent sign instead of leaving it on the live board, so it keeps showing the old time long after the schedule changes.the live value (a count or current state)is likethe train's departure time, which keeps changingfreezing it into durable proseis likeprinting it onto a permanent signthe as-of time that should travel with itis likea timestamp saying when this time was accuratethe basis it was read fromis likethe underlying timetable the departure time came fromthe rederive route that recomputes itis likethe live board you could check to get the real current timeWhere the analogy breaksThis shows that a moving value frozen in permanent text drifts while the text stays put; it does not establish that any value left on the live board is itself currently correct, only that a printed sign loses the ability to be re-checked.

Why it mattersIt keeps readers from trusting a stale figure that reads exactly like a live one, long after the real number has moved.

Potential misreadingThat because the number was true the moment it was written down, it stays a reliable fact afterward.

AP-9 is the failure AX-10 exists to refuse: writing a live value into prose as if it were a fixed fact. A count, a "current" total, a readiness signal, or a route tally is a cached read of moving state, so the moment it lands in text without an as-of time, a named basis, and a way to recompute it, the page starts asserting something it can no longer check. It is tempting because the number is true at the instant it is written, and the freshness contract feels like clutter next to a clean figure. The bite is that the value drifts while the prose does not, and a stale figure reads exactly like a live one; under the claim and evidence model the figure has quietly become a bare assertion, admissible only at the bottom of the evidence order because nothing can rederive it. The honest forms are the ones P-11 names: carry the freshness fields, keep the value out of durable prose, or mark it explicitly as a dated snapshot.

Formal statementdurable(φ)  ∧  live(φ)  ∧  ¬ ∃  a, b, r. carries(φ, ⟨ a, b, r ⟩)A live-state value is frozen into durable prose while no as-of time, basis, and rederive route travel with it.φa value written into durable textdurable(φ)the value is frozen into durable proselive(φ)the value is a read of moving state (a count, a current total, a readiness signal)athe as-of time the read was takenbthe basis the value was computed fromrthe route that recomputes itcarries(φ, ⟨ a, b, r ⟩)the value carries its as-of time, basis, and rederive route
GovernsThe time-and-freshness boundary, where a moving value is written down as if it were fixed.
RequiresCatching the freeze: a live value must carry an as-of time, a basis, and a rederive route, stay out of durable prose, or be marked a dated snapshot.
RefusesFreezing a count, a "current" state, or a live total into prose with no as-of, basis, or way to re-derive it.

In practiceThe fact-claim audit treats a volatile count written without a freshness contract as a blocking condition rather than a fact, so a frozen live number is caught instead of trusted because it once was true.

Enforced inDoctrine Fact Claim Audit Live Source Drift Bundle

The tempting mistakeA page states "the system has 77 components" as a flat fact; the figure was right when typed, but nothing records when it was read or how to recompute it, and it keeps reading as current long after it drifts.

GuardsAX-10

NegatesP-11

Scope limitBlocking unbound live values does not establish a freshness contract is in place everywhere, nor that any carried as-of value is current. It is a floor under AX-10 and P-11; it catches the frozen figure, it does not certify that the figures still bound to a basis are fresh.

Source JSON · Show relationships →

AP-12Synthetic system substitutionStanding a real claim on a synthetic fixture when real material was available, so a fabricated input carries weight the real basis never granted.

In plain termsThe mistake of building a real conclusion on a made-up stand-in input when genuine, shareable material was right there to use, so the fake input quietly lends the conclusion strength it never earned.

AnalogyA lab keeps a bag of practice 'dummy' blood for training, but when a real patient test is needed the technician uses a dummy bag instead of the available real sample and reports the result as a genuine reading.the synthetic fixture standing in for real materialis likethe practice dummy blood bagthe available real materialis likethe real patient sample that was on handthe real claim that inherits unearned strengthis likethe result reported as a genuine patient readingWhere the analogy breaksThis shows only that a stand-in must not be passed off as the real input when the real input was available; it does not say practice dummy bags are useless, and it does not establish that the real sample, once used, would give a correct or complete reading.

Why it mattersReaders can tell whether a stated result rests on something real and shareable or on a convenient placeholder, so they can judge how much to lean on it.

Potential misreadingThat a stand-in is fine because it looks identical to the real thing on the page. The tempting wrong belief is that looking the same means it can carry the same weight.

AP-12 is the failure AX-1, AX-4, and AX-8 jointly refuse: substituting a synthetic fixture for available real material and then letting a real claim ride on it. A synthetic stand-in has no derivation from anything real (so AX-1's checker has nothing to recompute), it is not the content hash of any real basis (so AX-4 cannot tell when it has drifted from the thing it stands for), and it carries no real provenance (so AX-8's label is fabricated at the door rather than propagated). It is tempting because a synthetic fixture is convenient and looks identical to a real one on the page, and the system itself admits synthetic fixtures for shape and negative cases; the line AP-12 polices is narrower, when real material exists, a synthetic substitute must not silently inherit a real basis's strength.

Formal statement∃  φ. basis(φ) = Bsyn  ∧  avail(Breal)  ∧  H(Bsyn) ≠ H(Breal)  ∧  strength(φ) ⊐ ⊥A claim is grounded on a synthetic basis while a real basis was available, the stand-in's content hash differs from the real basis's hash (it was not derived from the real material), and the claim is still allowed to carry more than bottom strength.φa claim that carries real weightbasis(φ)the basis the claim is grounded onBsynthe synthetic fixture it is grounded onavail(Breal)the real material was available to readBrealthe real material that was availableH(Breal)the content hash of that real basisstrength(φ)the evidence strength the claim is allowed to carrybottom: the strength a fabricated input may carry
GovernsThe basis boundary, where a claim is grounded on a real or a fabricated input.
RequiresGrounding a load-bearing claim on available real material, or holding the claim at bottom and labelling the input synthetic when only a fixture stands in.
RefusesSubstituting a synthetic fixture for available real material and letting the claim inherit a strength the real basis never granted.

In practiceThe source-import protocol brings real material in by manifest and digest so a real claim is grounded on content-addressed real input, rather than a synthetic stand-in fabricated in its place.

Enforced inSource Projection Import Protocol Corpus Readiness Mathlib Absence Gate

The tempting mistakeA readiness claim is grounded on a synthetic corpus fixture and reported as real coverage, even though the actual corpus was available to read.

GuardsAX-1 AX-4 AX-8

NegatesP-1 P-2 P-5 P-9 P-14 P-15 P-17

Scope limitRefusing synthetic substitution does not make the real basis correct, complete, or strong, and it does not forbid synthetic fixtures where they are declared as such. It only stops a fabricated input from carrying a real basis's weight; this example is reader illustration and never counts as support for the rule.

Source JSON · Show relationships →

Source, projection, and flow

AP-7Public/private membrane breachLetting untrusted, private, provider, prompt, or raw-voice material reach a public or privileged sink without a carried provenance label and a declared sanitizing transform.

In plain termsThe mistake of letting private or untrusted material reach a public or high-trust place just because the last step looked clean, without a label saying where it came from and without running it through a stated cleaning step first.

AnalogyWaving a shipment through customs because the final truck looked ordinary, even though no declaration form rode with the goods and no inspection was actually performed.the private or untrusted value entering a flowis likethe goods arriving at the borderthe public or high-trust place it reaches (the sink)is likeentry into the country past customsthe provenance label that must travel with the valueis likethe declaration form stating where the goods are fromthe declared cleaning step the value must pass throughis likethe actual inspection that clears the goodsthe clean-looking final step that hides the breachis likethe ordinary truck that makes everyone wave it throughWhere the analogy breaksThis shows the crossing must be gated by what travels with the goods, not by how the truck looks; it does not establish that checking goods at one border post keeps every border in the country clean, and one clean shipment does not mean the whole supply chain is safe.

Why it mattersIt is how a system can publish from private-adjacent sources at all without leaking secrets, account secrets, or planted instructions onto a public page.

Potential misreadingThat if the last copy step looks tidy and nothing obviously private is visible, the material is safe to publish.

AP-7 is the failure AX-8 exists to refuse: a value crosses into a public or privileged sink carrying trust it never earned. It bites because the final step usually looks clean, so a pipeline that copies a private-adjacent body, a model-output data, a prompt instruction, or source notes into a published page passes its own checks while leaking, since nothing recomputed where the value came from or what was done to it on the way. The repair follows the boundary model directly: a provenance class and ceiling must travel with the value, and untrusted material may reach the sink only through a declared transform whose output the sink's policy admits, never a clean label stamped on at the door. This is the membrane that lets the system publish from private-adjacent source at all, because the act of crossing is gated by carried provenance rather than by how the endpoint happens to look.

Formal statement(xs)  ∧  label(x) ⊐ policy(s)  ∧  ¬ ∃  T. (xTs  ∧  declared(T)  ∧  label(T(x)) ⊑ policy(s))A flow carries x into a sink s while x's carried provenance label sits above what the sink's policy may admit, and the flow passes through no declared sanitizing transform whose output label the sink's policy admits.xan untrusted, private, provider, prompt, or raw-voice value entering a flowsa public or privileged sinklabel(x)x's carried provenance class and ceilingpolicy(s)what the sink is allowed to admitsits above the ceiling the sink admitsTa declared sanitizing transformdeclared(T)T is a declared sanitizing transform whose output the sink's policy admits
GovernsThe boundary where material and its trust label cross into a public or privileged sink.
RequiresCarrying a provenance class and ceiling with the value, and routing untrusted material through a declared transform the sink's policy admits before it crosses.
RefusesUntrusted, private, provider, prompt, account secret, or raw-voice material reaching a privileged or public sink on a clean-looking final step, with no provenance carried and no declared transform applied.

In practiceThe prompt-injection replay carries an information-flow policy with the data, so an untrusted instruction arriving at a tool call is caught at the boundary instead of trusted for having reached a trusted endpoint.

Enforced inIndirect Prompt Injection Information Flow Policy Replay Source Projection Import Protocol

The tempting mistakeA public page prints a value lifted from a private-adjacent source because the final copy step looked clean, with no provenance carried across the copy and no sanitizing transform between the source and the page.

GuardsAX-8

NegatesP-9 P-14

Scope limitGuarding the membrane at named endpoints is a floor under AX-8, not a positive proof of non-interference across the whole graph; endpoint catches are not general propagation, and the example illustrates the boundary rather than computing any support for it.

Source JSON · Show relationships →

AP-13Generated-result record source inversionTreating a generated result record as if it were hand-authored source, severing it from the basis that produced it.

In plain termsThe mistake of treating an auto-generated summary record as if it were the hand-written original, then editing or quoting that summary as the source while the real source it was built from is left behind and no longer matches.

AnalogyScribbling a correction onto a library's catalogue card and then citing the card as the book, when the card was only ever copied from the book and the book itself still says something different.the generated record derived from a sourceis likethe catalogue card copied from the bookthe hand-authored source it should defer tois likethe actual book on the shelfediting or citing the record as originis likewriting on the card and citing the card as the bookWhere the analogy breaksThis shows only that a copied card must stay below the book and be redone from it, never used as the origin; it stops there and does not establish that the book itself is correct or up to date.

Why it mattersIt keeps a generated view from quietly outranking the thing it was built from, so a reader knows which artifact is the real origin and which is just a downstream copy.

Potential misreadingThat whichever copy is already sitting in front of you, with a confident verdict on it, is the thing to edit and cite. The tempting wrong belief is that the handy artifact is the source.

AP-13 is the lineage confusion that AX-4 and AX-11 exist to refuse: mistaking a generated result record for the hand-authored source it was derived from. A generated record is a function of a basis, so its identity is the hash of that basis, and its authority can never exceed the basis it recomputes from; the moment it is read as source, it is cut loose from that basis, so drift no longer forces a recompute and a hand-edit to the record becomes an orphan with nothing underneath it. It is tempting because a generated record often looks authored, carries a confident verdict, and is the artifact already on disk, so the cheaper move is to cite it or edit it in place rather than fix the source and regenerate. The repair is to keep the kinds apart by construction: source is hand-authored and content-addresses its outputs, a generated record stays below its basis and is rebuilt from it, and a parity check refuses the record whenever it has drifted from the source it claims to project.

Formal statementgenerated(r)  ∧  r = f(B)  ∧  treated(r)  ⇒  rejectA generated artifact, derived from a basis by a builder, is rejected when it is treated as if it were hand-authored source.generated(r)r is a generated artifactra generated artifact such as a result record or projectionfthe generator from basis to artifactBthe content basis r is derived fromtreated(r)r is treated as hand-authored source
GovernsThe boundary between a generated record and the hand-authored source it derives from.
RequiresKeeping a generated record bound to its basis by hash and rebuilt from source, so it is recomputed rather than edited or cited as origin.
RefusesTreating a generated result record as hand-authored source.

In practiceThe source-import protocol brings material in by manifest and content digest, so each imported copy stays bound to the original it was derived from and a basis change forces a recompute rather than letting the copy stand in as source.

Enforced inSource Projection Import Protocol Durable Agent Work Landing Replay Standards Meta Diagnostics

The tempting mistakeA generated result record is edited directly and then cited as the origin for a verdict, while the source it was built from is left behind and no longer matches it.

GuardsAX-4 AX-11

NegatesP-5 P-12 P-14 P-15 P-17 P-18 P-19 P-20

Scope limitKeeping generated records bound to their basis does not make either the record or the source correct, and this example illustrates the rule without supporting it. Refusing the inversion only preserves lineage; it does not establish that the basis it points back to is itself true or complete.

Source JSON · Show relationships →

AP-16Receiver inflationDisplaying a declared, inferred, or generated downstream target as an observed runtime effect, with nothing witnessing that the effect actually reached the receiver.

In plain termsThe mistake of showing an action's intended destination as if the action had already landed there, when nothing has actually checked that it reached the receiving end.

AnalogyMarking a parcel 'Delivered' the instant it leaves the depot, just because the destination address is known, with no one at the doorstep confirming it actually arrived.the declared downstream target shown as an observed effectis likethe 'Delivered' status set the moment the parcel leavesthe missing witness at the receiveris likeno one at the doorstep confirming arrivalthe honest display: target marked declared and unobservedis likea truthful 'In transit, not yet confirmed at address' statusWhere the analogy breaksThis shows only that arrival must be confirmed at the receiving end before it is displayed as done; confirming one parcel's arrival does not establish that every parcel that went out arrived, and it does not say the address was the right one.

Why it mattersA reader can tell apart 'this was sent toward a known target' from 'this was confirmed to have landed', instead of mistaking an intention for a witnessed result.

Potential misreadingThat because the destination is known in advance, showing it as reached is as good as confirming it. The tempting wrong belief is that knowing where something is headed is the same as seeing it arrive.

AP-16 is the failure AX-8 exists to refuse, applied to effects rather than labels: presenting the intended receiver of an action as if it were the witnessed result. A pipeline declares that a value reached a sink, that a write landed in memory, or that a route was taken, and the page renders that declared target as an observed runtime effect, when nothing carried the effect relation across the steps between source and receiver. It is tempting because the downstream target is usually known in advance, so showing it costs nothing and almost always looks right, while the gap between an intended reach and a witnessed one is invisible to a reader. The repair is the same shape AX-8 imposes on provenance: the effect relation has to be carried and observed at the receiver, not asserted from the sending side, and absent that witness the honest display is a declared target marked as unobserved, held below the strength a real observation would carry.

Formal statementshows(effect(s, r))  ∧  ¬ ∃  w. witness(w, sr)Displaying an effect of a source s on a downstream receiver r as observed, while no witness establishes the effect relation from s to r.shows(effect(s, r))the page displays the effect of s on r as an observed runtime resultsthe source asserting it had a downstream effectrthe receiver: the declared, inferred, or generated downstream targeteffect(s, r)the claim that s actually reached or changed r at runtimewa witness of the effect relation, traced across the steps from s to rwitness(w, sr)a witness establishing the effect relation from s to r, observed at the receiversrthe effect relation, the flow from source to receiver that must be observed
GovernsThe receiver boundary, where an intended or generated downstream target is tempted to display as a witnessed runtime effect.
RequiresCatching the inflation: a witness of the effect relation observed at the receiver, or the target shown as declared and unobserved rather than as an effect.
RefusesRendering a declared, inferred, or generated downstream target as an observed effect with no evidence that the effect relation held.

In practiceThe work-landing replay confirms an agent action actually persisted at its destination before showing it as landed, so a declared target cannot display as a completed effect by intention alone.

Enforced inDurable Agent Work Landing Replay Agent Route Observability Runtime

The tempting mistakeA status surface shows a memory write as applied at the receiver because the sending step was issued, with nothing observing that the write actually landed there.

GuardsAX-8 AX-12

NegatesP-9 P-13 P-14 P-18 P-20

Scope limitCatching one inflated receiver display is a floor under AX-8 and AX-12, not a positive proof that any effect was achieved. Observing the relation at named receivers does not establish that every declared effect downstream held; the unobserved targets stay marked, not blessed.

Source JSON · Show relationships →

AP-17Projection-as-sourceLetting a generated page, card, or summary override the executable contract it was supposed to summarise.

In plain termsThe mistake of letting a generated page or summary overrule the real contract it was only meant to describe.

AnalogyTreating a news article about a law as if it were the law itself, and acting on the article when the two disagree.the generated projectionis likethe news article about the lawthe source contract it summarisesis likethe actual text of the lawWhere the analogy breaksThe article-versus-law picture shows a summary cannot outrank its source; it does not capture that the summary must also be recomputed and demoted when the source it describes drifts.

Why it mattersA readable summary is easy to trust, so letting it win over the source quietly replaces the real rule with a description of it.

Potential misreadingThat the clearest version is the authoritative one. The source stays authoritative; the summary only points at it.

AP-17 is the inversion P-15 exists to prevent: a projection quietly becoming the authority. It happens when a markdown page, a generated card, an atlas row, or a compact summary is cited as the source of truth, overriding the executable contract it was generated from. It is tempting because the projection is the readable thing, so people reach for it, and over time the source it came from is forgotten. The repair is to keep the projection below its source by construction: recompute from the contract, and demote the projection the moment its basis drifts.

Formal statementauth(proj) ⊐ auth(src)  ⇒  rejectIf a projection's authority would exceed its source's, reject it: a generated view can expose source authority but never raise it.auth(proj)the authority the projection claimsauth(src)the authority the executable contract holdsproja generated page, card, or summarysrcthe executable contract it summarisesclaims more authority thanrejectthe refusal the anti-principle requires
GovernsThe source-and-projection boundary, where a summary is tempted to outrank its origin.
RequiresRecomputing the projection from its contract and demoting it when its basis drifts.
RefusesTreating a markdown page, generated card, or compact summary as the source it merely describes.

In practiceThe doctrine projection builder regenerates the readable instances from the routing and markdown sources and checks parity, so the generated copy can never become the authority.

Enforced inWorld Model Projection Drift Control Room Source Projection Import Protocol

The tempting mistakeAn edit is made to a generated reference page and treated as canonical, while the contract it was built from is left behind and contradicts it.

GuardsAX-4 AX-11

NegatesP-5 P-12 P-14 P-15 P-17 P-18 P-19 P-20

Scope limitRefusing projection-as-source does not validate the source. It only keeps authority pointed at the executable contract rather than its readable shadow.

Source JSON · Show relationships →

Authority, effect, and the meta-layer

AP-8Blind irreversible mutationPerforming an irreversible mutation with no compensator, no rollback record, no compare-and-swap guard, and no declared irreversible boundary.

In plain termsThe mistake of making a real, hard-to-undo change while assuming it can always be taken back, when nothing was set up to take it back and nothing checked the situation had not already moved.

AnalogySending a bank transfer with no way to recall it and without first checking the account balance had not already changed since you looked.the irreversible effect being writtenis likethe money leaving your accountthe compensator or declared irreversible boundaryis likeeither a recall option or an upfront note that this transfer cannot be reversedthe compare-and-swap check against the expected parent stateis likeconfirming the balance still matches what you saw before you authorise the sendtwo writers racing on the same pathis liketwo people moving money from the same account at onceWhere the analogy breaksThis shows the obligation to set up a recall path and a balance check before sending; it does not establish that every transaction in the bank is reversible or race-free, only that these specific steps were put in place for this send.

Why it mattersIt stops a change from silently overwriting someone else's concurrent work or landing half-done with no recorded way to undo it.

Potential misreadingThat because the normal case completes fine, you can always undo a change later if something goes wrong.

AP-8 is the failure AX-9 exists to refuse: writing a real effect into the world while assuming it can always be taken back, when nothing was put in place to take it back. It bites because the happy path looks identical whether or not a guard exists; the gap only appears when two writers race, a parent state has already moved, or a step half-lands and there is no recorded way to undo it. The repair is to make every effect declare its own reversibility up front: a compensator or an explicitly named irreversible boundary, multi-step effects landing under compare-and-swap against an expected parent, and same-path writes held to a single writer. This connects to the evidence model through provenance and freshness rather than through a label: a write is only safe to treat as landed when the state it assumed is still the state it is acting on, and a record of how to reverse it travels with the effect rather than being assumed after the fact.

Formal statementeffect(e)  ∧  (¬ ∃  c. compensates(c, e))  ∧  ¬ irrev(e)  ∧  ¬ cas(e, parent)An effect e is landed while no compensator reverses it, no irreversible boundary is declared for it, and no compare-and-swap guards it against the parent state having advanced.effect(e)e is a real effect being written to the worldean effect being written to the worldca compensator that would reverse the effectcompensates(c, e)c is a compensator that reverses effect eirrev(e)an explicit declaration that the effect cannot be undonecas(e, parent)a compare-and-swap guard checking the parent state has not advanced under e
GovernsThe effect boundary, where a mutation is treated as safely landed.
RequiresCatching the blind write: a compensator or a declared irreversible boundary, compare-and-swap against the expected parent for multi-step effects, and a single writer per path.
RefusesWriting an irreversible effect with no compensator, no rollback record, no compare-and-swap or world-version guard, and no declared irreversible boundary.

In practiceThe work-landing replay refuses to advance when the expected parent has moved under it and when the head was not advanced as recorded, so a multi-step effect cannot land blindly over a state that has already changed.

Enforced inMission Transaction Work Spine Durable Agent Work Landing Replay Concurrency Mission Control

The tempting mistakeA step writes directly over a shared path on the assumption the prior state still holds, with no compare-and-swap and no way to reverse it, so a concurrent write is silently overwritten.

GuardsAX-9

NegatesP-10 P-16 P-17 P-18

Scope limitGuarding the named landing paths against blind writes does not establish every effect in the system is reversible or race-free. It holds the specific obligations AX-9 names, compensator-or-boundary, compare-and-swap, single-writer, over the surfaces that bind them, and the example illustrates that floor rather than counting as support for it.

Source JSON · Show relationships →

AP-10Prose-as-executable-authorityGranting executable authority to prose doctrine that is not accepted by the grammar and carries no result-record obligation or scope limit.

In plain termsThe mistake of treating a confidently written paragraph as a binding rule, when the system never accepted it through its formal checks and it never says what evidence it owes or where it does not apply.

AnalogyTreating a hand-written 'this person may enter' note taped to a door as real access, when it was never entered into the building's access system and never says which areas or hours it covers.the prose doctrine claiming to governis likethe hand-written note on the doormembership in the executable grammaris likebeing registered in the building's access systemthe result-record obligations it must declareis likestating what proof of access it must showthe stated scope limit (what it does not establish)is likenaming which areas and hours the pass does not coverWhere the analogy breaksThis shows that an unregistered note is only a readable claim, not real access; it does not establish that a pass which is registered is therefore correct or sufficient, only that an unregistered one should not open doors.

Why it mattersIt stops a pile of confident-sounding paragraphs from accumulating as if they were enforced rules nothing can actually check.

Potential misreadingThat a clearly and authoritatively worded statement is, by virtue of how it reads, a rule the system enforces.

AP-10 is the failure AX-11 exists to refuse: letting a sentence govern because it sounds authoritative. A standard, a policy line, or a doctrine page may bind behaviour only when an executable grammar accepts it and it carries result-record obligations and a stated scope limit; prose on its own is a readable view, not a rule. It is tempting because writing a confident paragraph is cheap and reads like governance, so a system accumulates prose that nothing can recompute and mistakes that pile for an enforced contract. The repair is to make the artifact pass the grammar and attach what evidence it must produce and what it does not establish, otherwise holding it at the strength of a projection rather than an authority.

Formal statementauthority(d)  ∧  (dL(G)  ∨  ¬ obligations(d)  ∨  ¬ anticlaim(d))  ⇒  rejectIf an artifact is granted governing authority while it is not accepted by the doctrine grammar, or carries no result-record obligations, or carries no scope limit, reject the authority and treat the prose as a projection.da doctrine artifact (standard, policy, page) claiming to governauthority(d)d is treated as a binding rule, not a readable viewL(G)the language of artifacts the executable doctrine grammar acceptsobligations(d)d declares the result records it must produceanticlaim(d)d states its scope limit, what it does not establish
GovernsThe boundary between doctrine that governs and prose that only reads as if it does.
RequiresRefusing authority to any doctrine that is not accepted by the grammar or lacks declared result-record obligations and a stated scope limit, holding it as a projection instead.
RefusesGranting executable authority to prose doctrine without grammar membership, result-record obligations, and a scope limit.

In practiceThe executable doctrine grammar accepts a standard as authority only when it parses in the grammar and carries its obligation and scope-limit fields, and keeps a negative case where a prose-only standard that overclaims completeness is rejected rather than admitted.

Enforced inExecutable Doctrine Grammar Standards Meta Diagnostics

The tempting mistakeA confidently worded policy paragraph is cited as the binding rule for a behaviour, although nothing parses or checks it and it never says what it does not cover.

GuardsAX-11

NegatesP-12 P-15 P-17 P-18 P-19 P-20

Scope limitRejecting prose-as-authority is a floor under AX-11, not a positive proof that any admitted standard is correct or complete. It keeps unparsed prose from governing; a standard that does pass the grammar is still only as strong as the obligations it actually carries, and this example illustrates the rule without counting as support for it.

Source JSON · Show relationships →

AP-11Meta-artifact exemptionExempting the system's own pages, validators, result records, or generated projections from the same evidence floor it imposes on everything else.

In plain termsThe mistake of letting the system's own pages, checkers, result records, or generated views skip the very evidence test it makes everything else pass, just because it is the system talking about itself.

AnalogyA testing lab that strictly retests every sample sent in from outside, but lets its own internal samples through on the lab's say-so without running the same test.the system's own pages, checkers, records, and projectionsis likethe lab's own internal samplesthe evidence floor it imposes on external claimsis likethe same test run on every outside sampleaccepting a self-claim without that flooris likepassing the internal sample on the lab's own wordthe support evaluator that must meet the floor it computesis likethe lab's own quality check still having to be tested itselfWhere the analogy breaksThis shows that the same test must apply to the lab's own samples, removing the self-discount; it does not establish that passing that test makes any sample clean, only that the lab cannot exempt itself from running it.

Why it mattersIt lets the system state its own limits honestly instead of having a flattering self-assessment quietly become a new unchecked claim.

Potential misreadingThat a claim is more trustworthy because the system is reporting on itself, so it deserves a lighter check than outside claims.

AP-11 is the escape hatch AX-12 exists to close: a self-claim that gets a discount because the system is talking about itself. It is tempting because the floor is demanding and the meta-layer feels trusted, so a generated page, a validator's own verdict, a result record, or a coverage projection slips through asserting "verified and complete" without passing the admissibility relation it imposes on external work. It bites hardest at the support evaluator, which must itself meet the support floor it computes, and at this very page, which is held below the source it describes and cannot raise that source's authority. The honest move is to route every self-claim through the same gate, so the system can state its own limits without that statement quietly becoming a new unchecked claim.

Formal statement∃  aM. ∃  φ ∈ claims(a). accept(φ)  ∧  ¬ admext(φ)Some claim carried by one of the system's own artifacts is accepted even though it would not be admitted under the same relation an external claim must pass.Mthe system's own artifacts: its pages, validators, records, and projectionsaany such artifactφa claim carried by the artifact about the systemclaims(a)the claims the artifact carries about the systemacceptthe claim is let throughadmextthe admissibility floor applied to an external claim
GovernsThe reflexive boundary, where a claim the system makes about itself is tempted to skip its own gate.
RequiresRouting every self-claim, in a page, validator, result record, or projection, through the same admissibility and refusal floor imposed on external claims.
RefusesA self-assessment of verified, complete, or launch-ready that would never pass the floor the system applies to the work it audits.

In practiceThe launch wording gate runs the same claim-language floor over the system's own public copy that it imposes on any other source, so overclaiming language in the system's own pages is blocked rather than waved through as a trusted self-statement.

Enforced inRelease Public Wording Gate Executable Doctrine Grammar

The tempting mistakeA generated page reports the system as verified and complete because its own coverage projection said so, with nothing recomputing that self-claim against the floor the system imposes on external work.

GuardsAX-12

NegatesP-13 P-18 P-20

Scope limitRefusing the meta exemption does not make the system witnessed, complete, or correct. Admission, support, and this refusal are independent; closing the escape hatch only removes the special pleading, and the worked example illustrates the rule without counting as support for any claim that the system actually meets its own floor everywhere.

Source JSON · Show relationships →

AP-14Public-authority inflationLetting public documentation imply a hosted service, external service access, source-file mutation, financial or trading decisions, deployment posture, affiliation or endorsement, or private-system equivalence the public artifact never actually holds.

In plain termsThe mistake of letting a public page's wording imply powers the system does not have, such as being a hosted, ready product, having an outside partner, changing its own source, making financial decisions, or being the same thing as the larger private system, when nothing behind the page backs any of that.

AnalogyLabeling a local prototype as a live production endpoint. The label may help a reader see what the prototype resembles, but it cannot grant the uptime, permissions, or partnerships that only the real production system carries.the public page implying an authorityis likethe 'production endpoint' label on the prototypethe inflated set of unbacked powersis likethe uptime, permissions, and partnerships the prototype does not actually havedemoting the claim to its bounded scope when no witness backs itis likerelabeling it an honest 'local prototype' until a real deployment existsWhere the analogy breaksThis shows only that a label must not promise a status nothing backs; it does not say the prototype is bad, and removing the inflated label does not settle whether the system could be deployed either way.

Why it mattersA reader can trust that what a public page says about itself, like being hosted or ready or affiliated, is limited to what the system can actually back, not free-floating prose.

Potential misreadingThat impressive-sounding wording is harmless because it costs nothing and usually looks right. The tempting wrong belief is that stating a power is the same as holding it.

AP-14 is the inflation the evidence floor exists to refuse: a public page quietly granting itself an authority it cannot back. The danger is that all seven implied authorities (a hosted service, access to an external service, permission to mutate the source, financial or trading decisions, deployment posture, an affiliation or endorsement, or equivalence with the whole private system) are stated for free in prose, while the witness that would actually hold each one is absent. The failure is the unbacked implication, not the implication itself: a backed authority may be stated at its bounded scope. It bites across three floors at once: AX-5, because an in-scope claim with no admissible witness must fail closed rather than read as granted; AX-8, because a public-authority implication is private-adjacent material that may reach a public sink only through a declared transform, not by being asserted at the page; and AX-12, because the system's own copy is held to the same evidence floor it imposes on any other work. The repair is to state only the authority a witness backs, and to demote or refuse the public claim the moment the witness is missing.

Formal statementimplies(d, α)  ∧  α ∈ Λ  ∧  ¬ witness(d, α)  ⇒  demote(d, α)  ∨  refuse(d, α)If a public artifact lets a reader infer an authority from the inflated set and no admissible witness backs that authority, the claim is demoted to its bounded scope or refused. The bad thing is the unbacked implication, not implication itself.da public doctrine artifact or docimplies(d, α)d lets a reader infer authority alphaαan implied authorityΛthe inflated-authority set: hosted service, external service access, source-file mutation, financial or trading decisions, deployment posture, affiliation or endorsement, or private-system equivalencewitness(d, α)an admissible witness backs d's claim to authority alpha
GovernsThe boundary between what a public page implies and what authority the system actually holds.
RequiresStating only the authority an admissible witness backs, and demoting or refusing the public claim when the witness is absent.
RefusesLetting public copy imply a hosted service, external service access, source-file changes, financial or trading decisions, deployment posture, affiliation or endorsement, or private-system equivalence that nothing holds.

In practiceThe launch wording gate scans the system's own public copy for launch-grade language and blocks a line that would imply hosting, readiness, or whole-system launch the system does not hold, so the claim is demoted to its bounded scope rather than published.

Enforced inRelease Public Wording Gate Public Reveal Walkthrough Cold Reader Route Map

The tempting mistakeA landing page reads as a ready, hosted product backed by an affiliated provider, when the system is a public reconstruction that hosts nothing, calls no provider, and makes no claim of affiliation.

GuardsAX-5 AX-8 AX-12

NegatesP-2 P-6 P-9 P-13 P-14 P-15 P-18 P-19 P-20

Scope limitBlocking inflated public-authority language does not establish that any specific authority is in fact held; it only refuses the unbacked implication. The example is reader illustration and never counts as support that the system is hosted, deployed, affiliated, or deployment-posture.

Source JSON · Show relationships →

Read the reference

This page gives you the stance; the reference pages give you the objects in full. The Doctrine reference lays out every axiom, principle, anti-principle, concept, and mechanism as a card you can open, with its obligations, witnesses, and relations. The Evidence and authority page shows how each component is backed, and how an evidence rank measures how independently a check can disagree with the thing it checks. The paper modules carry the long-form explanations behind the components. A good cold reading leaves you knowing what the system will refuse, which is what matters most before you trust any of it.