Compiler guarantee recovery — gap analysis vs the recovered THESIS.md tiers (docs + doc-graph binds)

DESIGN.md

@@ -25,6 +25,8 @@ Three things follow, in order:
 - **From A2 and A3 — grounding is intersubjective.** Because time is the *only* assumed-shared value, a fact is grounded only by pointing at a shared, time-stable framework (§4), never an internal taxonomy.
 - **At the limit — reduce intersubjectivity to physics.** The deepest such framework — the efficient, time-bound description of interactions that satisfies a goal — is **physics** (A1–A2 turned on grounding itself). So the aim, at its limit, is to *reduce intersubjectivity to physics*: replace convention with necessity until nothing arbitrary survives. This is the deep reason §3 models the universal frameworks and real upstream rather than re-coining them — a nickname is convention standing where physics was available.
 
+The safety axis carries its own measure, used throughout: **safety is measured by how far each error class has climbed from runtime harm toward structural impossibility** — the guarantee ladder; §4b defines the ladder, its ceilings, and its evidence rules.
+
 ## 2. Minimize redundancy (the master move for cost and complexity)
 
 Redundant work — **duplicated, unnecessary, or irrelevant** — loses on all three of §1's quantities at once: it costs more to run, it widens the surface where harm hides, and it adds complexity to maintain. So a perfectly DRY process is, *by the meaning of redundant*, the minimal/efficient one; minimizing redundancy is therefore the master move for §1's cost and complexity axes (the safety axis is §5). Through §1's time lens this is *why* DRY matters at all: redundant work **defers** cost into the future — it shoves a problem onto a later fixer, or builds a process destined to be thrown out — so DRY is the refusal to spend someone's future time to buy the author's present convenience; it values time **holistically**, across every party and all of it, not just the here-and-now. Redundancy is removed along exactly two directions — not separate "DRY rules," but one move seen two ways:
@@ -53,6 +55,14 @@ Because the substrate is closed and grounded, the wins of §2 fall out for free:
 - *e.g.* `dag/std/algebra.dag` derives `Int.add` from `Int` inhabiting a ring (ops aren't listed per type); idempotency dissolved from an `idempotent: Bool` flag into the `EffectShape` variant; termination is *checked, not discovered* — `DescentEvidence = Strict | NonIncreasing | DescentUnknown` inhabits a `BoundedLattice` with bottom = fail-closed.
 - *e.g.* **one grammar, read in both directions** (§2 horizontal, not an adapter pair): ingest selects a production *forward* to fold surface syntax into a core `Node`; emit (`serialize_target ∘ translate`) selects from the *same* `target_model_edge_translation_rules` rows *backward* — the structural inverse, not a second emitter — so a new target language is rows authored in `extdeps/languages/`, never an edit to the fold (N rows, not N×M parser/emitter pairs). Coercion is that same move turned sideways: whether one model inhabits another is a homomorphism check (`coercion_fold` via `find_witness`), the same epistemic chain the emitter walks. One procedure asked in three directions, not three procedures.
 
+## 4b. Safety: the guarantee ladder (every error class climbs from runtime harm toward unwritability)
+
+**Placed here because it is what §4's decidability buys, before §5 legislates the floor (operator directive 2026-07-31; worked examples and the rung census live in the recovery analysis linked below).** Safety is not the presence of diagnostics or the absence of crashes — it is the reduction of the state space in which a program can silently do the wrong thing. Every discovered error class sits on one ordered ladder and is obligated to climb it: **mitigatable** (the failure occurs; harm is contained by total operations, typed outcomes, bounds, rollback, isolation) → **mechanically preventable** (a generated test, lens, or gate reliably exposes and blocks it — but the invalid state remains writable, and safety depends on that mechanism executing and staying enrolled) → **structurally guaranteed** (the source can still describe the invalid state, but no `Accepted` program contains it: the compiler derives a proof or refusal from modeled structure) → **structurally impossible** (the invalid state has no constructor or representation in the canonical model — validation is unnecessary because the bad state cannot be written, and a refusal at the source boundary is then a symptom of the carrier's shape, not a separate check). The higher rung subsumes the lower — construction over proof, proof over validation, validation over mitigation; §5's construction-before-validation preference is this ladder's top two rungs, and its fail-closed doctrine is the law of the floor. Below the floor sits **silent wrongness, which is not a rung: it is outside the ladder and forbidden outright** (§5). Adjacent — and deliberately **not a fifth rung** — is **outside the modeled guarantee**: external reality, undecidable properties, undeclared intent. That column is observed, refused, or mitigated at a declared boundary, never fabricated (§5), and keeping it off the ladder prevents "we do not model this" from masquerading as a weak implementation that should climb.
+
+Every class carries an **attainable ceiling — derived, not aspirational**: a decidable, fully modeled class may reach structural impossibility; a decidable class missing its authority is §5's *wall after grounding*; a class blocked on a missing language capability names the capability as its trigger (the live one: **unforgeable construction** — the top rung for every carrier-borne invariant — waits on reference-level constructor visibility, there being no private/sealed/opaque in the language today, so every proof-carrier is presently forgeable); an undecidable property honestly remains a ratchet or validator; an external fact remains a boundary obligation. **Below ceiling is a correctness gap, never optional elegance** — this clause is what keeps §6's purity trap from pricing out mandatory walls, the exact failure mode by which the recovered guarantee decayed unnoticed. Four meta-obligations make the ladder operational: (1) **rung honesty** — the reported rung must equal the rung established by executed evidence, a discriminating RED refused on the real acceptance path plus an accepted positive control; a type name, diagnostic variant, inert lens, or plan establishes nothing, and **rung inflation** (a carrier named for the top rung while occupying the bottom; a status ledger's "DONE") is the fabricated-plausible-output failure applied to the compiler's self-description — worse than sitting low, because an inflated class never ranks for climbing. (2) **no untracked stall** — a class below its ceiling must name its next-rung trigger, separating *cannot climb further* from *can climb after one grounding* from *can climb now but unbuilt*; only the first is permanent. (3) **no silent regression** — a change may lower a rung only by declaring previous rung, temporary rung, reason, bounded population, and restoration trigger; a compatibility exemption is not bootstrap glue, it is a visible safety regression with a finite runway. (4) **dissolution on climb** — a climb deletes the redundant lower-rung machinery it obsoletes (§2/§3: the proof that makes a state unwritable replaces the validator of the writable form, never accumulates beside it) unless that machinery independently guards an external boundary. Every newly discovered error class — incident, review finding, runtime exception, falsifier divergence — files or updates one row: invalid state, harm, distinguishing facts, rung found at, ceiling with reason, next trigger. That is how "any class we find climbs" is a repository rule rather than a cultural preference.
+
+**The floor first, the differentiator above it.** gunbc must first hold the ordinary compiler floor — names resolve, applications bind in exact bijection, values inhabit declared types, fields exist, closed variants eliminate exhaustively — and a failure there is a **below-baseline safety regression**, never compensated by higher-order capability. The differentiating claim begins above that floor: because the substrate carries causal, cardinality, algebraic, effect, ownership, cost, and realization facts structurally, the same ladder applies to classes ordinary compilers leave to tests, review, profiling, or production postmortems — a possibly-empty collection flowing into a nonempty consumer, recursion without a descent proof, a non-idempotent effect under automatic retry, a computation exceeding its declared complexity bound, operations whose declared algebra shows cancellation or duplication, a partially applied infrastructure change without convergence, a realization that does not preserve modeled behavior. The promise is **not** that every property becomes impossible; it is that every modeled class climbs to the highest honest rung its facts and decidability permit, with the ceiling and the residual risk explicit. Stated beside the ladder so a low ceiling is never mistaken for a gap: the compiler does not invent unstated intent (declared bound violated → refusal; declared algebra proves equivalence → derive; undeclared preference → never fabricated); does not prove unmodeled external reality (observe → typed evidence → admit or refuse → mitigate); does not lift arbitrary predicates to proof (the closed decidable cardinality fragment climbs where a general `fn(T) -> Bool` refinement cannot); and richer type names are not safety (a brand, wrapper, or `Validated<T>` is cosmetic until construction and acceptance enforce the distinction). Runtime mechanisms — typed refusal, totality, rollback, budgets — remain real and necessary at honest boundaries; they must only never be mislabeled as construction. The rung census over the recovered claims, the worked floor/differentiating/boundary examples, and the climb plan: → [compiler-guarantee recovery gap analysis](docs/plans/compiler-guarantee-recovery-gap-analysis.md); its Stage 1 lands the executable claims carrier (per-class current rung, measured evidence, ceiling with reason, next trigger, consumer-in-`Accepted`), grounding the enforcement-intent thread below rather than minting a second registry beside it.
+
 ## 5. Fail-closed (§1's safety axis — harm reduction)
 
 Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded "forever" ≠ an "unknown" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion<Nat>` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches "never"). The word **"never" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — "done" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.)