Guarantee lane: open-candidate honesty, anchored baseline, FrontierAccepted, closure door, v2 split (post-merge verdict)

DESIGN.md

@@ -48,7 +48,7 @@ Minimization holds only if each fact lives in exactly one place. The recurring v
 
 ## 4. The closed, grounded substrate (what makes §2–§3 decidable)
 
-You can unify and decompose *mechanically* only in a closed, grounded system — so the substrate is built for it. A program is a dependency graph over two primitives (`Node` + `Edge`) and a closed vocabulary (6 connectives + 5 behaviors); surface syntax is sugar that adds no power. Execution is **bounded and forward** (cyclic relations via acyclic encodings, never cyclic values; recursion is sugar over `Loop`), so decidability and termination *fall out* rather than being separately proved. **Grounding is intersubjective** — point at a shared framework, not an internal taxonomy — and in a closed system **a heuristic is never necessary**: the richer source always exists or can be written. This is *why* the structure is acyclic — a DAG in the substrate, serial reasoning in this document (recursively, per the preamble): intersubjective agreement holds only **across time** (§1), which demands claims that stay stable under it, so each is written syllogistically — a consequence-chain you can re-interrogate and that never wavers (algebra), never a cycle that could quietly redefine itself.
+You can unify and decompose *mechanically* only in a closed, grounded system — so the substrate is built for it. A program is a dependency graph over two primitives (`Node` + `Edge`) and a closed vocabulary (6 connectives + 6 behaviors — `Value`, `Transform`, `Branch`, `Loop`, `Bind`, `Match`, per `v2.std.node.Behavior`; an earlier revision said 5, corrected against the live coproduct 2026-07-31 because the closed vocabulary is the denominator the decidability argument divides by); surface syntax is sugar that adds no power. Execution is **bounded and forward** (cyclic relations via acyclic encodings, never cyclic values; recursion is sugar over `Loop`), so decidability and termination *fall out* rather than being separately proved. **Grounding is intersubjective** — point at a shared framework, not an internal taxonomy — and in a closed system **a heuristic is never necessary**: the richer source always exists or can be written. This is *why* the structure is acyclic — a DAG in the substrate, serial reasoning in this document (recursively, per the preamble): intersubjective agreement holds only **across time** (§1), which demands claims that stay stable under it, so each is written syllogistically — a consequence-chain you can re-interrogate and that never wavers (algebra), never a cycle that could quietly redefine itself.
 
 Because the substrate is closed and grounded, the wins of §2 fall out for free: operations come from *inhabitance* (no per-type ops); and emission, ingestion, and coercion are **one** total decision procedure run in different directions (the epistemic chain *is* the emission algorithm — N models, not N×M adapters; every refusal a located, typed mismatch).
 
@@ -61,7 +61,7 @@ Because the substrate is closed and grounded, the wins of §2 fall out for free:
 
 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-or-unverified language capability names the capability as its trigger (the live one: **unforgeable construction** for carrier-borne invariants — `sole_constructor` is the existing candidate wall, a cross-module construction refusal with its own `SoleConstructorViolation` diagnostic and sealed-record specimen, but its completeness for generic refinement carriers, all construction forms, and the compiler-module check exemptions is **unverified** — the ceiling is an audit finding, not a declared absence; an earlier revision of this paragraph claimed no such capability exists, refuted by review 2026-07-31); 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, at a declared subject grain** — 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, **measured against a declared boundary** (source→interpretation, source→each emission target, phase-carrier→phase-carrier are different paths with independently different rungs: the interpreter refuses a mislabeled call that the emitter reorders into positional leftovers); a class's current rung is the **minimum across its in-scope paths**, or one row per structurally distinct path — citing the strongest path while another stays silent is inflation, and a type name, diagnostic variant, inert lens, or plan establishes nothing. **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 — production handling only, never the evidence** — a climb deletes the redundant lower-rung *production* 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), but the class's discriminating RED and positive control **remain enrolled as the executing evidence that the higher rung stays real** — deleting them would recreate specification-without-execution one rung up; an expecting-red probe that greens when its wall lands flips to a permanent regression control, it does not retire (correction per review 2026-07-31: an earlier revision would have deleted the evidence with the machinery). 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-path disposition **derived** from executed measurements — no stored rung field exists, so a transcribed rung is unrepresentable rather than lens-caught — with ceiling + typed reason, next trigger, consumer-in-`Accepted`; corrected per review 45367, which caught this clause reading as a stored per-class rung column), grounding the enforcement-intent thread below rather than minting a second registry beside it.
+**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-path disposition **derived** from executed measurements — no stored rung field exists, so a transcribed rung is unrepresentable rather than lens-caught — with ceiling + typed reason, next trigger, consumer-in-`Accepted`; corrected per review 45367, which caught this clause reading as a stored per-class rung column; the dispositions include `FrontierAccepted`, the typed-located-counted diagnostic whose phase result is still `Accepted` — distinct from silent below-floor AND from a refusal, per the 2026-07-31 post-merge verdict, whose live specimens are the open candidates' `MethodExistenceUndecided` and `GroundingNotDerived`), grounding the enforcement-intent thread below rather than minting a second registry beside it.
 
 ## 5. Fail-closed (§1's safety axis — harm reduction)