PREFIX dissolution lens L1.1-L1.12 acceptance keys by briansrls · Pull Request #3318 · gunb-ai/gunbc

briansrls · 2026-05-18T19:01:27Z

SG-0 hand-path delta: +1

SG-0 pairing: (c) Net add is one EXPECTED_HAND_AUTHORED_TEST row for the v4 coverage lens ratchet (v4_lens_coverage_dag_smoke_test.rs) plus the matching INVARIANTS.md §P5(b) receipt row. Dispatch posture: retire this host check when the v4 coverage lens runs as .dag / generated coverage per ROADMAP T-PB-B (pb_rust_tests_outside_residual_zero); dispatch evidence: gunbc#3318 (this PR).

Summary

Extends docs/design-dissolution-lens.md with L1.7-L1.12 definitions so the Wave-2 batch has a complete L1.1-L1.12 design surface.
Adds DissolutionLensKey and twelve acceptance data rows to src/v4/lens/coverage.dag, giving the PREFIX batch a substrate coverage target rather than a prose-only checklist.
Adds a parse-level integration ratchet for the coverage rows and SG-0 census receipts for the v4 lens smoke/ratchet tests.

Test plan

cargo fmt --check -p v3-compiler — passed.
cargo test -p v3-compiler v4_lens_coverage --test integration — passed.
cargo test -p v3-compiler sg0_census --test integration — passed.

Notes

v4_lens_coverage_dag_smoke_test stays parse-level because the current single-file v4 smoke harness does not bundle sibling std/lens imports for coverage.dag; the ratchet specifically asserts the L1.1-L1.12 acceptance data rows exist.

…— coordi

briansrls

Review metadata

Provider / model: codex / unknown
Commit: feca0cbd · Trigger: schedule
Thinking: 191s wall

BLOCKING (1)

Root Cause

src/v4/lens/coverage.dag The L1.1-L1.12 acceptance universe is still hand-authored from docs/design-dissolution-lens.md because registered dissolution-lens declarations cannot be enumerated yet → derive the keys from that registry now or mark the hand-authored key coproduct as 🟡 with its dissolution trigger.

ROADMAP — Verified

T-PB-B/pb_rust_tests_outside_residual_zero: The new hand-Rust test has a matching INVARIANTS P5 receipt and PR-body append deferring it to the concrete T-PB-B row.

⚠️ One substrate coproduct disposition is materially misclassified.

…— coordi

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 084fb009 · Trigger: schedule
Thinking: 126s wall

Non-blocking — Strengths

src/v4/lens/coverage.dag The substrate coproduct is now explicitly bounded as a hand-authored acceptance-key scaffold rather than presented as terminal domain structure.

ROADMAP — Verified

T-PB-B/pb_rust_tests_outside_residual_zero: The new hand-Rust coverage ratchet has the required SG-0 pairing: PR-body append, INVARIANTS P5 row, and EXPECTED_HAND_AUTHORED_TEST census entry.

✅ No blocking concerns in the changed lines.

…— coordi

briansrls · 2026-05-18T21:23:02Z

Dashboard nudge (draft / “mark ready or close”) — response from lane coordinator

#3318 remains draft intentionally, not abandoned. witty-cat-59 directive (HOLD / TRACK-NOT-FINALIZE): do not finalize or lock Wave-2 dissolution acceptance witnesses against moving #3313 taxonomy until #3313 stabilizes and #3240 ratifies; scaffold/tracking only (warm-koi-304 lane owner).

Action: not running gh pr ready from fierce-cat-31 — that would contradict operator posture. Parent/dashboard: please stop nudging “ready” for this PR until the HOLD lifts; treat draft + green CI as the expected state.

— sent from fierce-cat-31

…cal L1.x keys Bundles three changes operator-routed via witty-cat-59 as the #3313 stabilization trigger: 1. **L1.11 plausible-fallback** — drop the "return type is not Outcome<_>" carve-out that was a false negative on `fn(...) -> Outcome<T>; None => Produced { value: ... }`. Replaces with a structural FailClosedDiagnostic registry declaring Outcome::Rejected as the registered fail-closed constructor. The lens fires on RHS Ctors that are not registered as fail-closed, covering both the F10 bare-return case AND the Outcome-wrapped fabricated-success case the prior signature missed. or_default-style total-by-design helpers escape via a structural PlausibleFallbackExemption row, same shape as L1.8 WrongHomeExemption and L1.9 VacuousArmExemption — no comment anchors. 2. **L1.12 parallel-authority** — reframe so lexical-name collision is the *trigger* (not the conclusion), with four resolution paths the lens checks against the substrate: (1) same-concept-with-alias (CanonicalConcept row + alias edge) → passes (2) same-concept-without-alias (CanonicalConcept row but no alias) → fires (the original duplicate-authority case) (3) distinct-concepts (ConceptDisambiguation row marks them as legitimately different) → passes (4) silence (no row in either registry) → **fires as unresolved-duplicate** The prior formulation only fired on (2) and missed (4) — the F9 motivating case where Bool was declared in two files with no CanonicalConcept row anywhere. The substrate must take a position on every cross-file lexical collision; silence fails closed. 3. **§5.1 Canonical L1.x acceptance-key names** — new subsection enumerating the stable canonical key names downstream consumers (e.g. coverage.dag's dissolution_l1_* rows) must use. The lens suite is the single authority; downstream key sets are projections. Includes explicit migration notes: - `dissolution_l1_6_emit_template` → retired, no L1.6 key - `dissolution_l1_10_string_escape_hatch` → split into `dissolution_l1_10_a_template_hole` AND `dissolution_l1_10_b_canonical_carrier` This is the #3313-stabilization step in #3322's closeout register (item 7). On land: - warm-koi-304's #3318 (held-at-track-not-finalize) can rebase against the stable §5.1 enumeration - batch-(d) remains held until A1 invariant placement PR lands too Routed via witty-cat-59 (program-coordination); follow-up PR owned by sunny-wolf-435 as #3313 author per #3322 closeout-register row 7. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 83e7c917 · Trigger: schedule
Thinking: 279s wall

✅ No blocking concerns in the changed lines; targeted cargo verification could not run because Cargo was not permitted to write its registry cache.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: e9e3eab9 · Trigger: schedule
Thinking: 235s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new hand-authored Rust ratchet is paired with the SG-0 census row, INVARIANTS P5(b) receipt, and PR-body append naming the generated-coverage dissolution lane.

✅ No blocking issues found in the changed lines; targeted cargo verification was blocked by Cargo registry cache permissions.

… — bundled with canonical-B Operator-authorized 2026-05-18 (via PM sunny-wolf-435): v3 is FROZEN 2026-05-15 and not in the v2->v4 bootstrap chain; its interim isolated compile_to_dag smoke ratchets are dead weight and incompatible with the decl-ref canonical-B grounding. P5 = dissolution, not deactivation: fully delete, don't disable. Dissolved (each: .rs + integration.rs mod + INVARIANTS §P5(b) row + sg0_census EXPECTED_HAND_AUTHORED_TEST row): v4_extdeps_cpp_abi / cpp / typescript / machine_code / lean + v4_std_fact_density INVARIANTS §P2 narrative updated to record the dissolution + name the replacement gate. RETAINED (verify-don't-trust the relayed list): v4_lens_cost — the PM list named "v4_lens_coverage" (held PR #3318, absent here); the branch instead has v4_lens_cost, a distinct P9/T-12 cost-lens authority ratchet (not a decl-ref-blocking extdeps parse smoke). Held pending explicit PM confirm rather than exceeding authorized invariant-surface scope. Replacement gate (no coverage loss): CI v4: job `v2-compiler compile --source-root src/v4` — v2->v4 bootstrap-viability per STRUCTURE.md, the authoritative v4 parse check. Verified: v2 v4: 0 diagnostics (72 modules, decl-ref B all 6); v3 sg0_census 17 passed/0 failed (census + integration consistent). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: fix-language-files * WIP: fix-language-files * ledger reconciliation: retire D2a bare-alias + {spelling}-GroundingMap across extdeps/languages (A-vs-B = B / ruled-B) Supersedes the disposition rows that framed the now-rejected hollow grounding shape as canonical, so two contradictory dispositions do not stand against the landed ruled-B exemplar: - DECISIONS.md CppBool: 🟢 GREEN terminal → 🟡 deferred to feature:t4-cpp-scalar-ladder (bool lands structurally as CppScalar.BoolScalar; hollow alias was never a real 🟢). - DECISIONS.md rust.dag/RustNever + python singleton row: bare alias / {spelling}-GroundingMap retired; grounding is a fold-discharged structural coincidence (RustScalar.NeverScalar/BoolScalar, PythonNumericTower.BoolLevel); GroundingMap home moot. - INVARIANTS §P2 receipt: GroundingMap twin retired from every extdeps/languages slice (machine_code already; now rust/cpp/lean); only the lean.dag/machine_code Symbol twin remains P2-staging. Anchors the canonical single-valued/uninhabited exemplar at docs/modeling/grounding-worked-examples.md §0. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * correct §0 + ledger over-claim: bare classifier tag is NOT the machine-readable grounding edge Addresses the PR #3338 exploratory review note (dead RustBool/RustNever names in §0) and an operator-flagged accuracy defect: §0 and the ledger rows asserted RustScalar.BoolScalar / PythonNumericTower.BoolLevel as "structural grounding," but a bare nullary classifier variant has no fold-traversable edge to std Bool/Never — by the machine-readable- inhabitance bar that is "basically nil," the same hollow class as the retired {spelling} GroundingMap. §0 now separates the two artifacts: (1) the classifier fact (present, honest surface enumeration — same as machine_code/ptx carry); (2) the machine-readable grounding edge (NOT present in any extdeps slice; exemplar = std/logic.dag's real bool_boolean_algebra instance) — and flags A-vs-B (deletion-only + deferred fold, vs. author the real grounding instance now) as the OPEN operator-owned canonical-B call. Substrate-feature determination holds under both readings (no Class-5 gap #3 dependency either way). File Status lines + DECISIONS.md CppBool / RustNever / python-singleton rows reworded to match — no claim that the bare tag is the grounding. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * DECISIONS.md:123 — explicit single-authority for retired TsBoolean=Bool Blocking inline review (typescript.dag:3): the per-file TS findings row scoped remaining scaffolds to "Non-Bool D2a(1)" (so not contradictory) but did not explicitly record the Bool D2a(1) alias as retired, leaving single-authority implicit. Now states TsBoolean=Bool is retired (ruled-B), not in the remaining-scaffold set, and points to the TS-D2 § as the single disposition authority. The TS-D2 § + the 902 bullet were already reconciled in 8128a59 (relay arrived post-fix). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * INVARIANTS §P2: scope the GroundingMap→resolver.dag "moot" wording to the removed twin only cursor/composer-2 exploratory note (review 14422): "the GroundingMap→ resolver.dag trigger is moot" was easy to misread as cancelling D4 / shared resolver.dag work entirely. Reworded: the per-file-twin *relocation* obligation is obsolete *for the removed twin shape* (twin deleted, not relocated); explicitly does not cancel/supersede/bear on any independent shared-resolver.dag / D4 work. Non-blocking clarity fix. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * canonical-B LANDED: decl-ref shared-authority bool grounding across all 6 (v2-verified) Implements reading B via the v2-verified decl-ref form `data <lang>_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` (references the single std/logic.dag authority — M2-clean) in rust / cpp / go / lean / python / typescript. Rust `!` = `type RustNever = Never` (direct primitive identity). Python carries the int-subtype build-up note (PythonNumericTower.BoolLevel) — first iteration. Verified against the REAL bootstrap gate (v2-compiler compile --source-root src/v4, ci.yml v4: job): 72 modules resolved, 0 diagnostics. Parse/resolve-verified; v2-run T-22-deferred (not execute-verified — claimed no further). Doc §0 reframed: dropped "quirked"; one universal grounding discipline (reference the shared authority for what the spec shares, build up from primitives where the spec deviates); bool-vs-int level spectrum; honest v2 scope. DECISIONS.md (CppBool 🟡→🟢-grounded, LeanScalar, TS-D2 §, line 123, python, rust/RustNever) + INVARIANTS §P2 flipped from "open canonical-B call" to LANDED. Frozen v3-smoke incompatibility is a tracked governance followup (v3 not in bootstrap chain), not edited here. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * dissolve 6 frozen v3 extdeps/std parse-ratchets (operator-authorized) — bundled with canonical-B Operator-authorized 2026-05-18 (via PM sunny-wolf-435): v3 is FROZEN 2026-05-15 and not in the v2->v4 bootstrap chain; its interim isolated compile_to_dag smoke ratchets are dead weight and incompatible with the decl-ref canonical-B grounding. P5 = dissolution, not deactivation: fully delete, don't disable. Dissolved (each: .rs + integration.rs mod + INVARIANTS §P5(b) row + sg0_census EXPECTED_HAND_AUTHORED_TEST row): v4_extdeps_cpp_abi / cpp / typescript / machine_code / lean + v4_std_fact_density INVARIANTS §P2 narrative updated to record the dissolution + name the replacement gate. RETAINED (verify-don't-trust the relayed list): v4_lens_cost — the PM list named "v4_lens_coverage" (held PR #3318, absent here); the branch instead has v4_lens_cost, a distinct P9/T-12 cost-lens authority ratchet (not a decl-ref-blocking extdeps parse smoke). Held pending explicit PM confirm rather than exceeding authorized invariant-surface scope. Replacement gate (no coverage loss): CI v4: job `v2-compiler compile --source-root src/v4` — v2->v4 bootstrap-viability per STRUCTURE.md, the authoritative v4 parse check. Verified: v2 v4: 0 diagnostics (72 modules, decl-ref B all 6); v3 sg0_census 17 passed/0 failed (census + integration consistent). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * dissolve v4_lens_cost ratchet (7th) — operator-extended authorization Operator extended the v3-ratchet dissolution authorization 2026-05-18 (via PM sunny-wolf-435) to v4_lens_cost_dag_smoke_test.rs (P9/T-12 cost-lens single-authority ratchet), on the same dead-weight logic as the other 6. Same shape: .rs + integration.rs mod + INVARIANTS §P5(b) row + sg0_census EXPECTED_HAND_AUTHORED_TEST row removed; §P2 narrative updated (7 total dissolved; retained-clause replaced). Replacement gate (no coverage loss): src/v4/lens/cost.dag's own structural authority + the v2-bootstrap-viability parse check. Verified: v3 sg0_census 17 passed/0 failed (census + integration consistent); v2 v4: 72 sources, 0 diagnostics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * DECISIONS.md:123 — reconcile stale D2a(2) GroundingMap clauses with landed ruled-B ts_bool_grounding Blocking inline review (DECISIONS.md:123): the TS ledger row still said "D2a(2) GroundingMap remains 🟡 operator-pending ... no local GroundingMap or ts_*_grounding rows may be declared" AND (tail) "D2a(2) rows are blocked only by the shared GroundingMap authority decision" — both contradict this PR landing ts_bool_grounding, leaving two authoritative states under P2. Reconciled: the {spelling}-GroundingMap shape is RETIRED under ruled-B (no pending shared-P2-home — removed, not relocated; cf. INVARIANTS §P2). Local GroundingMap type + {spelling}-style ts_*_grounding:GroundingMap{} rows stay forbidden (the hollow form); the ruled-B decl-ref ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra is a distinct sanctioned shape (declared this PR, P2/E-6 staging) with the TS-D2 § as single-authority disposition. Tail clause superseded likewise. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: fix-language-files * E-6 conformance: formalize <lang>_bool_grounding as E-6 bounded-exception (codex RC 14452 — valid) codex/codex-default REQUEST_CHANGES (review 14452) is correct: adding a consumer-less target-spec `data <lang>_bool_grounding` row is, by itself, an E-6 ("No Target-Spec Field Without A Same-PR Consumer") concern — honest "staging" wording alone does not cure it. But E-6's own text has a **bounded exception (clause (b))**: a consumer-less target-spec field MAY land if it "sits behind a named scaffold marker with a dissolution trigger" naming the lane that wires consumption (same sanctioned pattern as the existing SourceSpecReadFact P2-staging precedent). So the fix is NOT revert (honors operator's "land canonical-B in #3338") and NOT the unbuilt consumer — it is formalizing the rows as the E-6 bounded exception: - Each of the 6 `data <lang>_bool_grounding` decls now carries the inline named scaffold marker `🟡 feature:canonical-b-grounding-consumer` + explicit dissolution trigger (B1-CANON canonical/content_hash fold + coercion zip-fold; DECISIONS.md B1 · T-9/C1 consume the row). - INVARIANTS §P2 + grounding-worked-examples.md §0 restate this as an E-6 clause-(b) bounded exception (named scaffold + trigger), not speculative metadata. Comment/prose-only (.dag `//` lines + docs) — parse-inert; prior v2 `v4:` 0-diag verification (data rows already present) holds; no test files touched. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * cursor 14459 (both NON-BLOCKING, valid): fix v4_lens_cost over-claim + Practice-9 de-prose Finding 1 (P0 honesty — INVARIANTS §P2): the v4_lens_cost dissolution wording over-claimed "no coverage loss / dead weight same logic as the other 6". Verified false: v4_lens_cost_owns_llvm_instruction_cost_table was a STRUCTURAL single-owner regression-guard (exactly one parsed llvm_instruction_cost under v4.lens.cost, zero under llvm_ir.dag) — a distinct class the whole-tree v2 parse gate does NOT substitute (the 6 were parse smokes; that one was a structural predicate). Reworded: property holds structurally on main (cost.dag:39, none in llvm_ir.dag) but its regression-guard is removed with no equivalent — NAMED tracked coverage gap (scaffold feature:p9-llvm-instruction-cost-single-owner), explicitly not "no coverage loss". 6-parse-smoke "no coverage loss" via the v2 v4: gate stays (true; scoped to them). Finding 2 (Practice 9 de-prose): the multi-line spec narration + 5-line E-6 scaffold comment + long // Status: lines I added to the 6 .dag read as parallel prose authority. Collapsed each to the terse contract: one // Anchor: + one-line scaffold tag that still carries the E-6 named marker (feature:canonical-b-grounding-consumer) + dissolve trigger + ledger pointer (E-6 clause (b) still satisfied); // Status: lines shortened to terse classification + ledger pointer. Spec/E-6 detail now lives only in DECISIONS.md/§0 (single authority, no parallel prose). Comment/prose-only (.dag // + INVARIANTS); parse-inert — prior v2 v4: 0-diagnostic verification holds; no test files touched. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…cal L1.x keys (#3334) * design-dissolution-lens: propose L1.7–L1.12 from 2026-05-18 ingest Adds six proposed Layer-1 lenses derived from the 2026-05-18 review ingest against `main@e7b8a8d` (corroborated against worktree HEAD). Each section follows the existing L1.x format (signature / decidability / verdict / escape / kills) and includes concrete code-level match cases + clean-shape examples, so the structural signature is reviewable without chasing repo paths. - L1.7 Off-substrate-fact — prose-asserted facts (F3 lattice, F4 width, F11 opacity). Generalizes the standing "machine-readable inhabitance" ruling. - L1.8 Wrong-home — orphan operations (F5 `nat_compare` in float.dag). Mechanizes MODELING M9. - L1.9 Vacuous-arm — exhaustive-but-empty match (F1 `ComputationNode { behavior: _ } => true`). - L1.10 String-escape-hatch — typed-model bypass via String (F6 `ShellCommand { command: String }` vs typed `process.Command`). Generalizes L1.6. - L1.11 Plausible-fallback — fabricated-sibling fallthrough (F10 `DELETE None => CreateEffect`). - L1.12 Parallel-authority — unmarked duplicate concept homes (F9 `dsl/std` vs `src/v4/std`; D2-resolver provisional + planned-absent). Each carries `Status: proposed` in the section header. Slipped-by ledger (§8) gains corresponding rows pinned to current main file locations so the evidence is grep-anchored per §3 methodology. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 F9 snippet: show existing classification tags, sharpen authority gap cursor/composer-2 review noted that the F9 "Concrete match" block implied both `dsl/std/types.dag` and `src/v4/std/logic.dag` were bare, when both files actually carry annotations above their `type Bool` line (legacy-scanner anchor prose in dsl/std/types.dag:163-172; 🟢 coproduct-dissolution classification tag at src/v4/std/logic.dag:13). The lens's case is sharper, not weaker, once the existing tags are visible: they classify the finding shape (dissolution status, scanner anchor) but neither *designates authority* between the two parallel declarations. L1.12 specifically requires a designator that picks a canonical winner, which is the gap classification tags don't fill. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.7 / L1.8 / L1.12: tighten hard-gate semantics per codex review Addresses three BLOCKING findings on the L1.7–L1.12 proposal: L1.7 — width discharge must be recursive. The previous signature/clean shape allowed a `Word64 { bytes: List<Byte> where len(_) == 8 }` that bottomed out at an unconstrained `Byte`, so an arbitrary-bit-count `Byte` still inhabited a "well-formed" `Word64`. Signature now requires a recursively-discharged refinement chain down to a fixed-cardinality leaf or primitive bit; clean-shape example shows the full Word64 → Byte → Bit chain and structurally distinct Float32/Float64 exponent/significand widths instead of a shared `FloatBody`. L1.8 — primary-concept selector replaces the argument-files heuristic. Previous signature ("every argument's type lives in file X") missed witness-target homing (a `meet` field of `Lattice<T>` belongs with T, not with whichever file declared its argument types). New four-rule structural cascade in priority order: (1) declared witness target → algebra's type parameter is the home; (2) same-type closure (`fn(T,T)→T` etc.) → T is the home; (3) upstream argument+return convergence on file X → X is the home; (4) no single owner → cross-cutting, lens does not fire. L1.12 — escape valve must be structural, not prose. The previous "// Authority: canonical | historical" comment markers were prose- as-authority — exactly the shape L1.7 exists to kill. The lens is now self-consistent: only structural shapes discharge it — alias/import identity from historical to canonical, a `data ... : HistoricalDeclaration` row in a retirement ledger read as data, or deletion+migration in the same change. Comment markers explicitly do not satisfy the escape, by construction. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.9 / L1.10 / L1.12: remove naming heuristics; substrate-declared facts only Addresses three BLOCKING findings from codex review on cfbc247: L1.9 — replace function-name suffix vocabulary with intra-match asymmetry. The previous signature gated on `*_well_formed` / `*_valid` suffixes — naming as a structural fact, which violates P1 ("heuristics are never structurally necessary"). New signature is purely structural: a single match where ≥1 arm has a trivial-literal RHS AND ≥1 sibling arm does non-trivial structural work. The discipline-role is inferred from the fact that the author already wrote real work for some variants, which makes the trivial siblings a vacuum. The F1 node_locally_well_formed case still fires (TypeNode arm calls edges_conform, ComputationNode arm returns true). L1.10 — replace hardcoded `command`→Command / `path`→Path / `url`→Url field-name table with a substrate-declared canonical-carrier registry. A typed carrier declares `data X: CanonicalCarrier<X> = { supersedes_string: { in_role: <role-tag> } }`; the lens reads the registry. Adding a new typed carrier is now a `data` row in `extdeps/`, not an edit to the lens definition. The lens carries no domain names. L1.12 — split planned-absent-import out of the duplicate-authority lens. They are different failure shapes: duplicate `type T` in two files is a duplicate-authority finding; a dangling import path is an unresolved-reference / fail-closed P3 finding. Collapsing them under one verdict reports the wrong root cause. L1.12 narrows to duplicate-declaration; planned-absent moves to an L0.8-extended row in the slipped-by ledger. The D2-resolver concrete-match block is retitled as a cross-reference note explaining why it does *not* collapse into L1.12. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.10 / L1.12: close opt-in bypass, broaden type-decl signature codex review on 3fb3e4d raised two valid findings: L1.10 — the role-tag refinement created an opt-in opportunity for authors to bypass the typed-carrier rule by omitting the tag. The escape "no role-tag refinement, passes" was convention-level enforcement, not API-level. New signature drops the role-tag mechanism entirely. The CanonicalCarrier registry declares a `supersedes_string_at_field_named` set (substrate data); the lens fires on any String field whose name appears in any in-scope registry entry, unconditionally. The author cannot bypass by omitting an annotation because there is no annotation — the trigger is the field name they chose plus the registry-declared coverage. Legitimate raw-string exemptions move to structural Exemption rows in the same registry, read as data. L1.12 — the prior signature said "type T = ..." literally, which only matches the alias/sum form. The slipped-by ledger row claims coverage of duplicate machine-word homes, but `type Word64 { bytes: List<Byte> }` is record form and would have escaped the literal signature. Broadened to "any `type T` declaration form" — sum/alias, record, unit, generic — with explicit enumeration of the covered forms so the signature unambiguously matches the cases in the section's own examples and ledger. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.1–L1.6: add Concrete match + Clean shape code examples The original L1.1–L1.6 sections describe each lens by signature / decidability / verdict / escape / kills, but did not show what the matching code or the discharging code actually look like. Adds the same "Concrete match" + "Clean shape" example blocks the proposed L1.7–L1.12 sections use, so each lens is concretely readable without chasing the referenced PRs. - L1.1: basic discriminant shape (`nat_is_zero`) + the laundered constant-algebra fold (`free_monoid_is_empty`-via-fold). - L1.2: (a) struct-of-functions (`ListMap<A,B>` wrapper) and (b) N near-identical single-field structs (`{ spelling: String }` ×N). - L1.3: declared-but-never-inhabited type (`ParseError` with no constructor, no `data`, no alias, no field). - L1.4: `Outcome<T>` clone (`NormalizeChildrenResult`), with the three-variant `Cached | Produced | Rejected` shape as the escape. - L1.5: clean recursion mirroring data shape (`ci_member` over List) and the short-circuit `match acc { Rejected => propagate; Ok => continue }` ladder (resolve/normalize walkers). - L1.6: type-construction template tables (`list_template: "Vec<{0}>"`) vs. structural target-type modeling. No signature, verdict, or escape semantics changed; this commit only adds illustrative code blocks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * A0 umbrella + cross-cutting themes + L1.6→L1.10 merge Implements the consolidation feedback as a middle path: tightens the conceptual scaffolding without dismantling the lens catalog. - §1: introduces A0 ("every semantic fact must have exactly one structural witness") as the umbrella invariant, with A1 retained underneath as the operation-specific specialization. Explicitly framed as operationalizing modeling-discipline.md Practice 10, not as a parallel rulebook, to avoid the L1.12-class parallel-authority hazard of duplicating Practice 10's principles here. - §5.0 (new): adds the three-levels framing (Invariant / Theme / Lens), the lens → theme(s) catalog (derive / witness / canonical-home / fail-closed), and the explicit disclaimer "themes are explanatory tags only — they do not define CI gates, test-corpus boundaries, or implementation passes; the mechanically enforced unit remains the L1.x lens signature." Per the §3 methodology, each lens's signature must be the smallest structural pattern that catches its finding's class with zero false positives, so theme-sharing alone does not collapse machinery. - L1.6 → L1.10 merge: the only mechanical merge in this rev, because the prior doc already stated that L1.10 generalizes L1.6. L1.10 is renamed "Textual-bypass lens" with two sub-signatures: L1.10.a TemplateHole — registry-free, catches `{0}`/`{1}` positional-placeholder string literals used as emitters L1.10.b CanonicalCarrier — substrate-declared registry, catches String fields whose name appears in a CanonicalCarrier coverage set L1.6 section becomes a one-paragraph pointer to L1.10.a, preserving anchor compatibility. The slipped-by ledger's F6 row is repointed to L1.10.b and a new F8 row is added for L1.10.a. L1.2/L1.3/L1.4, L1.8/L1.12, and L1.9/L1.11 are intentionally not merged — their detection machines are mechanically distinct (different signatures, decidability arguments, escape valves) and the operator TDD-pairs directive requires distinct test corpora per lens. They share themes in the §5.0 catalog without sharing implementation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * A0 tightening: witness-path / lens-family / Practice-10 ratification Five sharpening edits from operator review of the A0/themes pass: 1. A0 rephrased: "exactly one structural witness" → "exactly one canonical structural witness *path*". Alias / re-export edges, retirement-ledger rows, and derived operations reading the same witness all point at one authority; they are the path, not a multiplicity that violates A0. 2. §2 "one substrate gap" claim updated. The original sentence was true for the L1.1/L1.5 seed findings but too narrow for A0's broader territory. Now distinguishes the seed gap (no derived discriminant/catamorphism → workers hand-roll them) from the general gap (missing witness table / authority map / refinement edge / diagnostic carrier → workers encode locally in prose / names / strings / duplicate homes / plausible defaults). 3. L1.10 explicitly renamed "Textual-bypass lens family" with an "Exception to §5.0" note: L1.10.a TemplateHole and L1.10.b CanonicalCarrier are the mechanical units, sharing a finding family and reporting label but keeping separate signatures, decidability arguments, escapes, and test corpora. Resolves the tension between §5.0 ("the mechanically enforced unit is the L1.x signature") and L1.10's two-detector structure. 4. L1.6 stub retitled "Deprecated alias — see L1.10.a `TemplateHole`" so old test names and slipped-by references remain traceable. 5. §8 trailing prose fixed: "all four are burn-down substrate PRs" was true when the ledger had four rows; now it has the four seed rows plus the ingest extension. Reframed as "Pattern from the seed PR rows" with an explicit note that the ingest rows extend the ledger to A0's broader territory. 6. A0/A1 ratification sentence made authority-chain explicit: "Once ratified into Practice 10, A0/A1 become citable hard rules; this doc remains the enforcement mechanism." Avoids the rulebook-ish phrasing that suggested A0/A1 were independently citable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * §10 Dependency model — lenses are pipeline stages, not infrastructure Adds a new §10 (renumbering audit to §11) answering the "how does this run / is it parallelizable / how much work" questions operationally. The core framing: there is no "lens framework" separate from the compiler pipeline. Lenses are .dag stages that declare consumes: edges against the existing parse/resolve/infer producers, and the compiler's stage-ordering schedules them automatically. - §10.1: shared-indices taxonomy — maps each shared structural fact (AST, symbol resolution, variant lists, inhabitance edges, witness registries, refinement clauses, import graph, fail-closed return- type carriers) to the existing pipeline stage that produces it and the lenses that consume it. Most of what lenses need is already computed; lenses just query. - §10.2: three small derived stages cover what the existing pipeline doesn't yet expose — match_arm_shape (reusable by L1.1, L1.9, L1.11, L0.7, L0.13), closed_vocab_scan (L1.7), concept_home (L1.8). Each is a single deterministic fold; reusable across multiple lenses by design. - §10.3: a lens is just another .dag stage with declared dependencies. Adding a lens = land a stage; the existing compiler stage-ordering handles scheduling. No new framework. - §10.4: per-file and per-lens parallelism fall out of the dependency graph automatically; affected_set integration scales CI cost with PR size, not corpus size. - §10.5: summary of operational properties — one dependency model across pipeline + lenses, lens addition = stage land, index addition = small derivation stage shared by all lenses that need it, self-application clean (the compiler enforces the discipline it follows). This is the L1.12-class self-consistency check: a separate "lens framework" with its own dependency model would itself be parallel authority, which the lens suite exists to kill. The dependency-model section makes explicit that the lens framework reuses the pipeline's existing modeling — one dependency system for everything. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-dissolution-lens: stabilize #3313 — L1.11/L1.12 fixes + canonical L1.x keys Bundles three changes operator-routed via witty-cat-59 as the #3313 stabilization trigger: 1. **L1.11 plausible-fallback** — drop the "return type is not Outcome<_>" carve-out that was a false negative on `fn(...) -> Outcome<T>; None => Produced { value: ... }`. Replaces with a structural FailClosedDiagnostic registry declaring Outcome::Rejected as the registered fail-closed constructor. The lens fires on RHS Ctors that are not registered as fail-closed, covering both the F10 bare-return case AND the Outcome-wrapped fabricated-success case the prior signature missed. or_default-style total-by-design helpers escape via a structural PlausibleFallbackExemption row, same shape as L1.8 WrongHomeExemption and L1.9 VacuousArmExemption — no comment anchors. 2. **L1.12 parallel-authority** — reframe so lexical-name collision is the *trigger* (not the conclusion), with four resolution paths the lens checks against the substrate: (1) same-concept-with-alias (CanonicalConcept row + alias edge) → passes (2) same-concept-without-alias (CanonicalConcept row but no alias) → fires (the original duplicate-authority case) (3) distinct-concepts (ConceptDisambiguation row marks them as legitimately different) → passes (4) silence (no row in either registry) → **fires as unresolved-duplicate** The prior formulation only fired on (2) and missed (4) — the F9 motivating case where Bool was declared in two files with no CanonicalConcept row anywhere. The substrate must take a position on every cross-file lexical collision; silence fails closed. 3. **§5.1 Canonical L1.x acceptance-key names** — new subsection enumerating the stable canonical key names downstream consumers (e.g. coverage.dag's dissolution_l1_* rows) must use. The lens suite is the single authority; downstream key sets are projections. Includes explicit migration notes: - `dissolution_l1_6_emit_template` → retired, no L1.6 key - `dissolution_l1_10_string_escape_hatch` → split into `dissolution_l1_10_a_template_hole` AND `dissolution_l1_10_b_canonical_carrier` This is the #3313-stabilization step in #3322's closeout register (item 7). On land: - warm-koi-304's #3318 (held-at-track-not-finalize) can rebase against the stable §5.1 enumeration - batch-(d) remains held until A1 invariant placement PR lands too Routed via witty-cat-59 (program-coordination); follow-up PR owned by sunny-wolf-435 as #3313 author per #3322 closeout-register row 7. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 wording: "three resolutions" → "four outcomes (three passing + silence)" cursor/composer-2 review noted editorial inconsistency: the text said "exactly one of three resolutions" but the list enumerated 1-4 with silence as case (4). Corrected to "one of four outcomes — three passing resolutions plus a fail-closed silence case" so the prose matches the structural enumeration that follows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12: close the decision table — five outcomes, all in-table Reviewer (briansrls 2026-05-18T23:26Z) flagged that the prior wording said "three passing resolutions" but the enumerated 1-4 list had only TWO passing (alias, ConceptDisambiguation) and TWO firing (same-concept-without-alias, silence). The HistoricalDeclaration retirement-ledger and deletion/migration paths from the Escape section were "outside the stated decision table" — a P2 decidable-single- authority violation. Fix: restructure the enumeration to cover ALL mechanically-distinct outcomes inline, so the decision table is closed: (1) Same-concept-with-alias → passes (2) Same-concept-with-retirement-record → passes (new: was in Escape) (3) Distinct concepts (ConceptDisambiguation) → passes (4) Same-concept-without-alias-or-retirement → fires (original duplicate-authority case) (5) Silence → fires (unresolved-duplicate) Three passing + two firing = the arithmetic now matches. Deletion / migration is explicitly noted as "not a fifth resolution" — it removes the trigger condition entirely (no lexical collision), so the lens never engages, which is mechanically distinct from a resolution. The Escape section is collapsed to a pointer at outcomes (1)/(2)/(3) to avoid duplicating the decision-table content. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 Decidable bullet: include HistoricalDeclaration registry Closes the residual gap on the wrap BLOCKING review: outcome (2) "Same-concept-with-retirement-record" consults a HistoricalDeclaration registry row, but the prior Decidable bullet listed only CanonicalConcept + structural-alias + ConceptDisambiguation. Now every registry the 5-outcome decision table consults is named in the decidability statement explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.11 Verdict: per-case fix guidance (bare-return vs Outcome-wrapped) cursor/composer-2 review caught a contradictory-guidance bug: the new L1.11 bullets explicitly include the Outcome-wrapped case (fn(...) -> Outcome<T>; None => Produced { value: ... }) as firing, but the Verdict still said "lift the return type to Outcome<T> and return Rejected" — which doesn't address the case that's already Outcome-wrapped. Split the fix into two case-specific guidances: - Bare-return case: lift return type to Outcome<T>, return Rejected. - Outcome-wrapped case: replace Produced ctor with Rejected { diagnostic: DerivationUnknown } on the missing-info arm. Same underlying fix shape (escalate missing info through the registered fail-closed-diagnostic variant) — just two distinct starting points depending on which form of fabricated-success the lens caught. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12: restore concept-level detection via two-trigger union (lexical OR CanonicalConcept co-membership) codex review (REQUEST_CHANGES) caught a real semantic weakening in the prior "lexical collision is the trigger" rewrite: two parallel homes for ONE concept with DIFFERENT names would slip past the lens entirely, contradicting P2 / Practice 5's concept-level single-authority demand. Fix: restore concept-level detection by adding Trigger B (concept- graph) alongside the existing Trigger A (lexical). The lens fires on parallel authority detectable in EITHER way: - **Trigger A (lexical):** cross-file `type T` declarations sharing a simple name. (Existing; catches the F9 motivating case.) - **Trigger B (concept-graph):** two `type T1` / `type T2` declarations in different files that are co-members of a `CanonicalConcept` row, regardless of whether their lexical names match. (NEW; catches the same-concept-different-name case the prior rewrite missed.) Either trigger enters the same 5-outcome resolution table. Per-outcome under Trigger B: - (1) alias / (2) retirement-record / (4) no-resolution apply cleanly to both triggers - (3) ConceptDisambiguation under Trigger B would CONTRADICT the CanonicalConcept co-membership row — registry-inconsistency, caught by L0-class checks, not L1.12 - (5) silence is NOT reachable under Trigger B (the trigger IS a registry row's presence); only reachable under Trigger A Also added an explicit Decidability Boundary note: the lens cannot catch the case where two homes use different names AND no CanonicalConcept row registers them as the same concept. That's a P2 violation but mechanically undetectable from parsed substrate alone — closing it requires either operator judgment or a future structural-similarity-fold primitive. Per §3 methodology, lens signatures catch their class with zero false positives; Trigger B's CanonicalConcept-driven gate is the structural surface decidable today. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…— coordi

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 26052347 · Trigger: schedule
Thinking: 243s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new hand-authored Rust parse ratchet is paired with the SG-0 census row, the INVARIANTS P5(b) receipt, and the PR-body append naming the generated-coverage retirement lane.

✅ No blocking issues found in the changed lines.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: e3347bca · Trigger: schedule
Thinking: 261s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new hand-authored Rust smoke test is paired with the SG-0 census row, INVARIANTS P5(b) receipt, and PR-body append naming the generated coverage retirement lane.

✅ No blocking concerns in the changed lines.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 69465d9c · Trigger: schedule
Thinking: 257s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new hand-authored Rust smoke test is paired with the SG-0 census row, the INVARIANTS.md P5(b) receipt, and the PR-body append naming the generated coverage retirement lane.

✅ No blocking concerns in the changed lines.

# Conflicts: # src/v4/DECISIONS.md

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 7d01e71d · Trigger: schedule
Thinking: 182s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new Rust coverage ratchet is paired with the SG-0 census row, INVARIANTS P5(b) receipt, and PR-body SG-0 deferral naming the generated coverage retirement lane.

✅ No blocking concerns in the changed lines.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 1b57cec5 · Trigger: schedule
Thinking: 343s wall

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new Rust ratchet is paired with the SG-0 census line, INVARIANTS P5(b) receipt, and PR-body append naming generated .dag coverage as the retirement lane.

✅ No blocking concerns in the changed lines.

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 1a75f0d0 · Trigger: schedule
Thinking: 211s wall

✅ No blocking concerns in the changed lines.

* design-dissolution-lens: propose L1.7–L1.12 from 2026-05-18 ingest Adds six proposed Layer-1 lenses derived from the 2026-05-18 review ingest against `main@e7b8a8d` (corroborated against worktree HEAD). Each section follows the existing L1.x format (signature / decidability / verdict / escape / kills) and includes concrete code-level match cases + clean-shape examples, so the structural signature is reviewable without chasing repo paths. - L1.7 Off-substrate-fact — prose-asserted facts (F3 lattice, F4 width, F11 opacity). Generalizes the standing "machine-readable inhabitance" ruling. - L1.8 Wrong-home — orphan operations (F5 `nat_compare` in float.dag). Mechanizes MODELING M9. - L1.9 Vacuous-arm — exhaustive-but-empty match (F1 `ComputationNode { behavior: _ } => true`). - L1.10 String-escape-hatch — typed-model bypass via String (F6 `ShellCommand { command: String }` vs typed `process.Command`). Generalizes L1.6. - L1.11 Plausible-fallback — fabricated-sibling fallthrough (F10 `DELETE None => CreateEffect`). - L1.12 Parallel-authority — unmarked duplicate concept homes (F9 `dsl/std` vs `src/v4/std`; D2-resolver provisional + planned-absent). Each carries `Status: proposed` in the section header. Slipped-by ledger (§8) gains corresponding rows pinned to current main file locations so the evidence is grep-anchored per §3 methodology. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 F9 snippet: show existing classification tags, sharpen authority gap cursor/composer-2 review noted that the F9 "Concrete match" block implied both `dsl/std/types.dag` and `src/v4/std/logic.dag` were bare, when both files actually carry annotations above their `type Bool` line (legacy-scanner anchor prose in dsl/std/types.dag:163-172; 🟢 coproduct-dissolution classification tag at src/v4/std/logic.dag:13). The lens's case is sharper, not weaker, once the existing tags are visible: they classify the finding shape (dissolution status, scanner anchor) but neither *designates authority* between the two parallel declarations. L1.12 specifically requires a designator that picks a canonical winner, which is the gap classification tags don't fill. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.7 / L1.8 / L1.12: tighten hard-gate semantics per codex review Addresses three BLOCKING findings on the L1.7–L1.12 proposal: L1.7 — width discharge must be recursive. The previous signature/clean shape allowed a `Word64 { bytes: List<Byte> where len(_) == 8 }` that bottomed out at an unconstrained `Byte`, so an arbitrary-bit-count `Byte` still inhabited a "well-formed" `Word64`. Signature now requires a recursively-discharged refinement chain down to a fixed-cardinality leaf or primitive bit; clean-shape example shows the full Word64 → Byte → Bit chain and structurally distinct Float32/Float64 exponent/significand widths instead of a shared `FloatBody`. L1.8 — primary-concept selector replaces the argument-files heuristic. Previous signature ("every argument's type lives in file X") missed witness-target homing (a `meet` field of `Lattice<T>` belongs with T, not with whichever file declared its argument types). New four-rule structural cascade in priority order: (1) declared witness target → algebra's type parameter is the home; (2) same-type closure (`fn(T,T)→T` etc.) → T is the home; (3) upstream argument+return convergence on file X → X is the home; (4) no single owner → cross-cutting, lens does not fire. L1.12 — escape valve must be structural, not prose. The previous "// Authority: canonical | historical" comment markers were prose- as-authority — exactly the shape L1.7 exists to kill. The lens is now self-consistent: only structural shapes discharge it — alias/import identity from historical to canonical, a `data ... : HistoricalDeclaration` row in a retirement ledger read as data, or deletion+migration in the same change. Comment markers explicitly do not satisfy the escape, by construction. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.9 / L1.10 / L1.12: remove naming heuristics; substrate-declared facts only Addresses three BLOCKING findings from codex review on cfbc247: L1.9 — replace function-name suffix vocabulary with intra-match asymmetry. The previous signature gated on `*_well_formed` / `*_valid` suffixes — naming as a structural fact, which violates P1 ("heuristics are never structurally necessary"). New signature is purely structural: a single match where ≥1 arm has a trivial-literal RHS AND ≥1 sibling arm does non-trivial structural work. The discipline-role is inferred from the fact that the author already wrote real work for some variants, which makes the trivial siblings a vacuum. The F1 node_locally_well_formed case still fires (TypeNode arm calls edges_conform, ComputationNode arm returns true). L1.10 — replace hardcoded `command`→Command / `path`→Path / `url`→Url field-name table with a substrate-declared canonical-carrier registry. A typed carrier declares `data X: CanonicalCarrier<X> = { supersedes_string: { in_role: <role-tag> } }`; the lens reads the registry. Adding a new typed carrier is now a `data` row in `extdeps/`, not an edit to the lens definition. The lens carries no domain names. L1.12 — split planned-absent-import out of the duplicate-authority lens. They are different failure shapes: duplicate `type T` in two files is a duplicate-authority finding; a dangling import path is an unresolved-reference / fail-closed P3 finding. Collapsing them under one verdict reports the wrong root cause. L1.12 narrows to duplicate-declaration; planned-absent moves to an L0.8-extended row in the slipped-by ledger. The D2-resolver concrete-match block is retitled as a cross-reference note explaining why it does *not* collapse into L1.12. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.10 / L1.12: close opt-in bypass, broaden type-decl signature codex review on 3fb3e4d raised two valid findings: L1.10 — the role-tag refinement created an opt-in opportunity for authors to bypass the typed-carrier rule by omitting the tag. The escape "no role-tag refinement, passes" was convention-level enforcement, not API-level. New signature drops the role-tag mechanism entirely. The CanonicalCarrier registry declares a `supersedes_string_at_field_named` set (substrate data); the lens fires on any String field whose name appears in any in-scope registry entry, unconditionally. The author cannot bypass by omitting an annotation because there is no annotation — the trigger is the field name they chose plus the registry-declared coverage. Legitimate raw-string exemptions move to structural Exemption rows in the same registry, read as data. L1.12 — the prior signature said "type T = ..." literally, which only matches the alias/sum form. The slipped-by ledger row claims coverage of duplicate machine-word homes, but `type Word64 { bytes: List<Byte> }` is record form and would have escaped the literal signature. Broadened to "any `type T` declaration form" — sum/alias, record, unit, generic — with explicit enumeration of the covered forms so the signature unambiguously matches the cases in the section's own examples and ledger. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.1–L1.6: add Concrete match + Clean shape code examples The original L1.1–L1.6 sections describe each lens by signature / decidability / verdict / escape / kills, but did not show what the matching code or the discharging code actually look like. Adds the same "Concrete match" + "Clean shape" example blocks the proposed L1.7–L1.12 sections use, so each lens is concretely readable without chasing the referenced PRs. - L1.1: basic discriminant shape (`nat_is_zero`) + the laundered constant-algebra fold (`free_monoid_is_empty`-via-fold). - L1.2: (a) struct-of-functions (`ListMap<A,B>` wrapper) and (b) N near-identical single-field structs (`{ spelling: String }` ×N). - L1.3: declared-but-never-inhabited type (`ParseError` with no constructor, no `data`, no alias, no field). - L1.4: `Outcome<T>` clone (`NormalizeChildrenResult`), with the three-variant `Cached | Produced | Rejected` shape as the escape. - L1.5: clean recursion mirroring data shape (`ci_member` over List) and the short-circuit `match acc { Rejected => propagate; Ok => continue }` ladder (resolve/normalize walkers). - L1.6: type-construction template tables (`list_template: "Vec<{0}>"`) vs. structural target-type modeling. No signature, verdict, or escape semantics changed; this commit only adds illustrative code blocks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * A0 umbrella + cross-cutting themes + L1.6→L1.10 merge Implements the consolidation feedback as a middle path: tightens the conceptual scaffolding without dismantling the lens catalog. - §1: introduces A0 ("every semantic fact must have exactly one structural witness") as the umbrella invariant, with A1 retained underneath as the operation-specific specialization. Explicitly framed as operationalizing modeling-discipline.md Practice 10, not as a parallel rulebook, to avoid the L1.12-class parallel-authority hazard of duplicating Practice 10's principles here. - §5.0 (new): adds the three-levels framing (Invariant / Theme / Lens), the lens → theme(s) catalog (derive / witness / canonical-home / fail-closed), and the explicit disclaimer "themes are explanatory tags only — they do not define CI gates, test-corpus boundaries, or implementation passes; the mechanically enforced unit remains the L1.x lens signature." Per the §3 methodology, each lens's signature must be the smallest structural pattern that catches its finding's class with zero false positives, so theme-sharing alone does not collapse machinery. - L1.6 → L1.10 merge: the only mechanical merge in this rev, because the prior doc already stated that L1.10 generalizes L1.6. L1.10 is renamed "Textual-bypass lens" with two sub-signatures: L1.10.a TemplateHole — registry-free, catches `{0}`/`{1}` positional-placeholder string literals used as emitters L1.10.b CanonicalCarrier — substrate-declared registry, catches String fields whose name appears in a CanonicalCarrier coverage set L1.6 section becomes a one-paragraph pointer to L1.10.a, preserving anchor compatibility. The slipped-by ledger's F6 row is repointed to L1.10.b and a new F8 row is added for L1.10.a. L1.2/L1.3/L1.4, L1.8/L1.12, and L1.9/L1.11 are intentionally not merged — their detection machines are mechanically distinct (different signatures, decidability arguments, escape valves) and the operator TDD-pairs directive requires distinct test corpora per lens. They share themes in the §5.0 catalog without sharing implementation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * A0 tightening: witness-path / lens-family / Practice-10 ratification Five sharpening edits from operator review of the A0/themes pass: 1. A0 rephrased: "exactly one structural witness" → "exactly one canonical structural witness *path*". Alias / re-export edges, retirement-ledger rows, and derived operations reading the same witness all point at one authority; they are the path, not a multiplicity that violates A0. 2. §2 "one substrate gap" claim updated. The original sentence was true for the L1.1/L1.5 seed findings but too narrow for A0's broader territory. Now distinguishes the seed gap (no derived discriminant/catamorphism → workers hand-roll them) from the general gap (missing witness table / authority map / refinement edge / diagnostic carrier → workers encode locally in prose / names / strings / duplicate homes / plausible defaults). 3. L1.10 explicitly renamed "Textual-bypass lens family" with an "Exception to §5.0" note: L1.10.a TemplateHole and L1.10.b CanonicalCarrier are the mechanical units, sharing a finding family and reporting label but keeping separate signatures, decidability arguments, escapes, and test corpora. Resolves the tension between §5.0 ("the mechanically enforced unit is the L1.x signature") and L1.10's two-detector structure. 4. L1.6 stub retitled "Deprecated alias — see L1.10.a `TemplateHole`" so old test names and slipped-by references remain traceable. 5. §8 trailing prose fixed: "all four are burn-down substrate PRs" was true when the ledger had four rows; now it has the four seed rows plus the ingest extension. Reframed as "Pattern from the seed PR rows" with an explicit note that the ingest rows extend the ledger to A0's broader territory. 6. A0/A1 ratification sentence made authority-chain explicit: "Once ratified into Practice 10, A0/A1 become citable hard rules; this doc remains the enforcement mechanism." Avoids the rulebook-ish phrasing that suggested A0/A1 were independently citable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * §10 Dependency model — lenses are pipeline stages, not infrastructure Adds a new §10 (renumbering audit to §11) answering the "how does this run / is it parallelizable / how much work" questions operationally. The core framing: there is no "lens framework" separate from the compiler pipeline. Lenses are .dag stages that declare consumes: edges against the existing parse/resolve/infer producers, and the compiler's stage-ordering schedules them automatically. - §10.1: shared-indices taxonomy — maps each shared structural fact (AST, symbol resolution, variant lists, inhabitance edges, witness registries, refinement clauses, import graph, fail-closed return- type carriers) to the existing pipeline stage that produces it and the lenses that consume it. Most of what lenses need is already computed; lenses just query. - §10.2: three small derived stages cover what the existing pipeline doesn't yet expose — match_arm_shape (reusable by L1.1, L1.9, L1.11, L0.7, L0.13), closed_vocab_scan (L1.7), concept_home (L1.8). Each is a single deterministic fold; reusable across multiple lenses by design. - §10.3: a lens is just another .dag stage with declared dependencies. Adding a lens = land a stage; the existing compiler stage-ordering handles scheduling. No new framework. - §10.4: per-file and per-lens parallelism fall out of the dependency graph automatically; affected_set integration scales CI cost with PR size, not corpus size. - §10.5: summary of operational properties — one dependency model across pipeline + lenses, lens addition = stage land, index addition = small derivation stage shared by all lenses that need it, self-application clean (the compiler enforces the discipline it follows). This is the L1.12-class self-consistency check: a separate "lens framework" with its own dependency model would itself be parallel authority, which the lens suite exists to kill. The dependency-model section makes explicit that the lens framework reuses the pipeline's existing modeling — one dependency system for everything. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-dissolution-lens: stabilize #3313 — L1.11/L1.12 fixes + canonical L1.x keys Bundles three changes operator-routed via witty-cat-59 as the #3313 stabilization trigger: 1. **L1.11 plausible-fallback** — drop the "return type is not Outcome<_>" carve-out that was a false negative on `fn(...) -> Outcome<T>; None => Produced { value: ... }`. Replaces with a structural FailClosedDiagnostic registry declaring Outcome::Rejected as the registered fail-closed constructor. The lens fires on RHS Ctors that are not registered as fail-closed, covering both the F10 bare-return case AND the Outcome-wrapped fabricated-success case the prior signature missed. or_default-style total-by-design helpers escape via a structural PlausibleFallbackExemption row, same shape as L1.8 WrongHomeExemption and L1.9 VacuousArmExemption — no comment anchors. 2. **L1.12 parallel-authority** — reframe so lexical-name collision is the *trigger* (not the conclusion), with four resolution paths the lens checks against the substrate: (1) same-concept-with-alias (CanonicalConcept row + alias edge) → passes (2) same-concept-without-alias (CanonicalConcept row but no alias) → fires (the original duplicate-authority case) (3) distinct-concepts (ConceptDisambiguation row marks them as legitimately different) → passes (4) silence (no row in either registry) → **fires as unresolved-duplicate** The prior formulation only fired on (2) and missed (4) — the F9 motivating case where Bool was declared in two files with no CanonicalConcept row anywhere. The substrate must take a position on every cross-file lexical collision; silence fails closed. 3. **§5.1 Canonical L1.x acceptance-key names** — new subsection enumerating the stable canonical key names downstream consumers (e.g. coverage.dag's dissolution_l1_* rows) must use. The lens suite is the single authority; downstream key sets are projections. Includes explicit migration notes: - `dissolution_l1_6_emit_template` → retired, no L1.6 key - `dissolution_l1_10_string_escape_hatch` → split into `dissolution_l1_10_a_template_hole` AND `dissolution_l1_10_b_canonical_carrier` This is the #3313-stabilization step in #3322's closeout register (item 7). On land: - warm-koi-304's #3318 (held-at-track-not-finalize) can rebase against the stable §5.1 enumeration - batch-(d) remains held until A1 invariant placement PR lands too Routed via witty-cat-59 (program-coordination); follow-up PR owned by sunny-wolf-435 as #3313 author per #3322 closeout-register row 7. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 wording: "three resolutions" → "four outcomes (three passing + silence)" cursor/composer-2 review noted editorial inconsistency: the text said "exactly one of three resolutions" but the list enumerated 1-4 with silence as case (4). Corrected to "one of four outcomes — three passing resolutions plus a fail-closed silence case" so the prose matches the structural enumeration that follows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12: close the decision table — five outcomes, all in-table Reviewer (briansrls 2026-05-18T23:26Z) flagged that the prior wording said "three passing resolutions" but the enumerated 1-4 list had only TWO passing (alias, ConceptDisambiguation) and TWO firing (same-concept-without-alias, silence). The HistoricalDeclaration retirement-ledger and deletion/migration paths from the Escape section were "outside the stated decision table" — a P2 decidable-single- authority violation. Fix: restructure the enumeration to cover ALL mechanically-distinct outcomes inline, so the decision table is closed: (1) Same-concept-with-alias → passes (2) Same-concept-with-retirement-record → passes (new: was in Escape) (3) Distinct concepts (ConceptDisambiguation) → passes (4) Same-concept-without-alias-or-retirement → fires (original duplicate-authority case) (5) Silence → fires (unresolved-duplicate) Three passing + two firing = the arithmetic now matches. Deletion / migration is explicitly noted as "not a fifth resolution" — it removes the trigger condition entirely (no lexical collision), so the lens never engages, which is mechanically distinct from a resolution. The Escape section is collapsed to a pointer at outcomes (1)/(2)/(3) to avoid duplicating the decision-table content. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12 Decidable bullet: include HistoricalDeclaration registry Closes the residual gap on the wrap BLOCKING review: outcome (2) "Same-concept-with-retirement-record" consults a HistoricalDeclaration registry row, but the prior Decidable bullet listed only CanonicalConcept + structural-alias + ConceptDisambiguation. Now every registry the 5-outcome decision table consults is named in the decidability statement explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * L1.11 Verdict: per-case fix guidance (bare-return vs Outcome-wrapped) cursor/composer-2 review caught a contradictory-guidance bug: the new L1.11 bullets explicitly include the Outcome-wrapped case (fn(...) -> Outcome<T>; None => Produced { value: ... }) as firing, but the Verdict still said "lift the return type to Outcome<T> and return Rejected" — which doesn't address the case that's already Outcome-wrapped. Split the fix into two case-specific guidances: - Bare-return case: lift return type to Outcome<T>, return Rejected. - Outcome-wrapped case: replace Produced ctor with Rejected { diagnostic: DerivationUnknown } on the missing-info arm. Same underlying fix shape (escalate missing info through the registered fail-closed-diagnostic variant) — just two distinct starting points depending on which form of fabricated-success the lens caught. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * L1.12: restore concept-level detection via two-trigger union (lexical OR CanonicalConcept co-membership) codex review (REQUEST_CHANGES) caught a real semantic weakening in the prior "lexical collision is the trigger" rewrite: two parallel homes for ONE concept with DIFFERENT names would slip past the lens entirely, contradicting P2 / Practice 5's concept-level single-authority demand. Fix: restore concept-level detection by adding Trigger B (concept- graph) alongside the existing Trigger A (lexical). The lens fires on parallel authority detectable in EITHER way: - **Trigger A (lexical):** cross-file `type T` declarations sharing a simple name. (Existing; catches the F9 motivating case.) - **Trigger B (concept-graph):** two `type T1` / `type T2` declarations in different files that are co-members of a `CanonicalConcept` row, regardless of whether their lexical names match. (NEW; catches the same-concept-different-name case the prior rewrite missed.) Either trigger enters the same 5-outcome resolution table. Per-outcome under Trigger B: - (1) alias / (2) retirement-record / (4) no-resolution apply cleanly to both triggers - (3) ConceptDisambiguation under Trigger B would CONTRADICT the CanonicalConcept co-membership row — registry-inconsistency, caught by L0-class checks, not L1.12 - (5) silence is NOT reachable under Trigger B (the trigger IS a registry row's presence); only reachable under Trigger A Also added an explicit Decidability Boundary note: the lens cannot catch the case where two homes use different names AND no CanonicalConcept row registers them as the same concept. That's a P2 violation but mechanically undetectable from parsed substrate alone — closing it requires either operator judgment or a future structural-similarity-fold primitive. Per §3 methodology, lens signatures catch their class with zero false positives; Trigger B's CanonicalConcept-driven gate is the structural surface decidable today. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * docs(design): read/edit pipeline — node-centric agent surface (design spec) Frames the substrate's read/edit surface for arbitrary code at the Node level — not the file level. Files are a delivery / persistence mechanism modeled via extdeps/file_system.dag; the language doesn't couple to them. Reads target Nodes (and scopes within Nodes); writes are structural Edits to Nodes; Node-to-File binding is its own concern, modeled alongside Node, not inside it. Operator-stated motivation (2026-05-19): the mechanical part of shifting bits isn't the hard part — the INTERFACE is. This doc captures the design intent + worked examples + open interface questions, especially for LLM/agent consumers. Doc structure: - §0-1: framing — why node-centric, not file-centric (3 reasons: files decoupled from concepts; edits should be structural; agent reasoning is at concept level) - §2: read interface — apply_lens(lens, scope, mode) per QRY-1 ratification (2026-05-15); no separate query subsystem; lens catalog + composition - §3: write interface — Path/Edit/Diff per #3162 ratification; apply_diff fold semantics (all-or-nothing fail-closed) - §4: read → edit pipeline — six-step closed loop (Read → Diagnose → Propose → Gate → Apply → Re-emit). Files only re-enter at Re-emit; they're a downstream effect of substrate state. - §5: three worked examples — (A) bare-alias refactor to canonical-B (same shape as #3338); (B) rename a concept across the corpus via CanonicalConcept registry cascade; (C) TestClaim breakage diagnosis + fix - §6: six open interface questions — higher-order Edit combinators, composition under overlap, intent-shaped declarations (generalized Track 2), LLM-targeted diagnostic shape, workflow-as-data for the agent loop, structural provenance traces - §7-8: scope clarifications + status Status: design spec; mechanical primitives exist, T-23 realizes them; the six open interface questions are where the substantive interface design work lives. No implementation prescribed. This is operator-requested framing work, not action work. Each open question becomes its own follow-up doc / PR when picked up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * WIP: PM * design-read-edit-pipeline: fix two P2 / THESIS-narrowing findings from openai-pro RC openai-pro (gpt-5-5-pro) review on f15b2b0 flagged two valid issues: **Finding 1: affected_set as implicit third scope (P2 violation).** §2 said "frontier is itself a scope" and §5/§6 examples passed `affected_set(dag, diff)` as `NodeScope(affected)`, but the ratified SectionRef is two-branch only (DeclarationScope | NodeScope). Treating `Witness<ReExecFrontier>` as a NodeScope-compatible value is an implicit coercion the typed surface doesn't model — violates P2 illegal-states-unrepresentable. Fix: clarify §2 that the frontier is a SET of declaration/node refs the caller folds over by re-applying the lens at each member's existing DeclarationScope/NodeScope. Rewrite all five affected worked-example sites (Examples A + 6.3 + 6.6) to fold over `affected.frontier.for_each(ref => apply_lens(_, ref, Enforce))` instead of passing `NodeScope(affected)`. SectionRef stays two-branch; gating over the affected frontier is composition, not a new scope shape. **Finding 2: workflow/agent_loop.dag conflicts with THESIS narrowing (LOCKED DESIGN DECISIONS).** §7.5 proposed extending self-application to `workflow/agent_loop.dag`, but THESIS retracted meta-process / work-direction modeling on 2026-05-15; self-application is narrowed to gunbc's own build/CI pipeline (workflow/{bootstrap, ci} only). The reviewer correctly noted my open question would reopen exactly the surface THESIS removed. Fix: reframe the open question per the reviewer's "out-of-scope / user-program workflow" option. The agent loop is a USER PROGRAM composing substrate primitives (apply_lens, apply_diff, affected_set, emit) — not an extension of gunbc's workflow/ surface. Renamed §7.5 from "Workflow-as-data for the agent loop" to "Agent-loop composition at the user-program level" and explicitly stated `workflow/agent_loop.dag` is not the right place; THESIS narrowing stands. The substantive open question (what user-program-side carriers ship with gunbc as conveniences vs are user-program-authored) is preserved without reopening the locked surface. §6.6 (CLI-driven concept declaration hero case) cross-reference also updated to call it out as a user-program composing primitives, not gunbc self-application. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: honest accounting of Node→File binding gap openai-pro BLOCKING inline at line 33 (sha c431266) flagged that the doc overclaimed file_system.dag's coverage: it models POSIX file operations (open/read/write/close) but does NOT yet carry a Node→File rendering binding as a first-class substrate fact. The relationship is currently emergent from the emit stage, not stored as queryable substrate data — claiming "file-tying is a structural fact" left the central file-binding authority off-substrate. Fixes: 1. **§1 rewrite (lines 41-44)**: replace the overclaim "the substrate models File explicitly ... so file-tying is a structural fact" with an honest accounting: file_system.dag is POSIX ops only; the Node-to-File relationship is currently emergent from emit, NOT a queryable data row. Design intent is right (file-tying as substrate data so it's queryable and auditable, not implicit in emit behavior), but the primitive doesn't exist yet. Tracked as a §6.8 gap. 2. **§6.8 addition (item 6)**: add Node→File binding registry to the missing-substrate list. Concrete shape: `data <node>_rendered_into: NodeToFileBinding = { node, file, region }`. Closes the "files are a downstream effect of substrate state" framing — that effect becomes a structurally-recorded fact, not just a compile-time side effect. The design intent (node-centric, file-as-effect) survives intact; the honest update is that one of the substrate primitives needed to make it fully structural still has to land. That's the right shape per INVARIANTS P2 (illegal-states-unrepresentable / single authority): don't claim a structural fact that isn't yet stored as queryable data — name the gap as a tracked dependency. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: mirror ratified Edit definition exactly (replacement only) openai-pro BLOCKING inline at line 81 flagged that the doc's description of Edit as "Replace / insert / delete at a position" contradicted the ratified std/node.dag authority, which defines: type Edit { at: Path, replacement: Node } type Diff { edits: List<Edit> } type Path { steps: List<Symbol> } Edit is a SINGLE replacement at a Path — no separate insert / delete variants. The "Replace / insert / delete" prose introduced operations the ratified type doesn't model, violating P2 single-authority. Fix: replace the prose with the exact ratified shape, noting that insertions and deletions are expressed by replacing the parent node with a new parent whose children list includes / excludes the targeted child. This is the natural decomposition under the ratified single-Edit shape and avoids inventing a parallel contract. Same single-authority fix shape as the earlier SectionRef + apply_diff alignments — point at the ratified definition rather than restate with diverged wording. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: mark §5/§6 examples as future-combinator-layer pseudo-code codex BLOCKING review (sha:1dcf5193) wrap raised three findings; two were already addressed in prior commits (c431266 affected_set scope collapse + ab4bcdb Edit shape mismatch). The third is the worked examples using higher-level edit verbs (replace_with, replace, insert, insert_field) that don't map directly to the ratified Edit { at: Path, replacement: Node } shape. Per the reviewer's "either express as replacement-at-path rewrites or mark them as a future combinator layer" binary: chose mark-as-future- combinator-layer because the examples are illustrative intent shapes, not authoritative Edit constructors. Rewriting each into explicit parent-replacement decomposition would make the examples much longer and harder to read for the design intent they're meant to convey. Added a clear pseudo-code disclaimer at the top of §5 ("worked examples") that covers both §5 and §6 examples: - States the verbs (replace_with, replace, insert, insert_field) are future-combinator-layer shorthand, NOT literal .dag - Cites §3 for the ratified Edit { at: Path, replacement: Node } - Explains the decomposition: insertions/field-additions land as parent-replacement (build a new parent node whose children list includes the desired child, single Edit at parent_path) - Points at §6.8 items 1 + 3 (machine-readable Clean shape + DAG-of-edits composition) as the substrate work that builds the combinator layer - "Treat the examples as intent illustrations, not authoritative Edit constructors" This restores single-authority discipline: §3 names the ratified Edit shape, and the examples are explicitly framed as combinator-layer pseudo-code that compresses common intent shapes for readability. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design-read-edit-pipeline: candidate-state gating + grounded L1.12 transform openai-pro REQUEST_CHANGES on b26f0d8 raised two valid design-level defects, both blocking: **Finding 1 — gate/apply ordering bug** (P3 fail-closed / structure gates emission). The §4 pipeline was: 4. Gate on affected_set (pre-edit graph) 5. Apply diff That gates the PRE-edit state then applies the Diff, letting a Diff introduce post-edit invariant violations that never get enforced before re-emit. Violates THESIS:13-15 + :453-457 "compiler validates every causal link before emitting to targets." Fix: rewrite §4 as a SEVEN-step candidate-state pattern: 1. Read 2. Diagnose 3. Propose Diff 4. Candidate: candidate_dag = apply_diff(dag, Diff) # uncommitted 5. Gate: enforce lenses against the CANDIDATE state 6. Commit: dag := candidate_dag (only if every gate passed) 7. Re-emit Added explicit "Why gate the candidate, not the pre-edit graph" paragraph naming the semantic gap the prior ordering would have created. The "fail-closed promise honest" framing: validation happens against the state that will be emitted, not against a state already known to be valid. Updated worked examples (§5.A, §6.3 catamorphism pipeline, §6.6 CLI pipeline) to use the candidate-state ordering throughout — apply_diff to candidate, gate against candidate, commit if green. **Finding 2 — L1.12 transform with ungrounded canonical-home pick.** §6.4 L1_12_transform called `pick_canonical_home(matched_pair)` in the outcome (5) silence case (no CanonicalConcept row anywhere). That's ungrounded inference — picking which side is canonical when the substrate has no canonical authority declared. INVARIANTS:31-32 says missing facts should be authored, not inferred by shortcuts. Fix: rewrite L1_12_transform to branch on outcome: - **Outcome (4)** same-concept-without-alias-or-retirement: a CanonicalConcept row EXISTS; READ canonical_home from it. Auto(Diff). - **Outcome (5)** silence: no canonical authority declared. NeedsDecision { because: no_canonical_authority, needs: operator_authors_CanonicalConcept_row { candidates: pair } }. Never an inferred pick. Added the general pattern statement: "transforms ground in substrate-declared authority; absence of authority becomes NeedsDecision, never an inferred guess." This is the design rule for every L1.x transform — auto-fix only when the substrate gives you grounded structural facts to fix toward. Both fixes preserve the design direction and tighten it on the fail-closed-and-no-inferred-authority discipline the project thesis demands. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: add hero case (f) — mechanical refactor Operator-articulated hero case (2026-05-19): mechanical refactors — declarative model-A → model-B transitions across the corpus — are "a good use case for more mechanical things (i.e. the only judgement applied is in which command to run, not literally changing each line)." Adds §6.7b as the sixth hero case, between merge-sort synthesis (§6.7) and the missing-substrate enumeration (§6.8). Key positioning: - **Cleanest convolution shape** — judgment at command-selection, zero per-site judgment. Distinguished from the other cases: (a) one lens auto-fix (b) one lens with conditional outcomes (c) per-site conditional cascade (f) declarative target, uniform per-site application - **Substrate guarantees** — uses the §4 candidate-state pattern to give the atomicity guarantee the user asked about ("how can we guarantee a successful migration"): either complete or no-op, never a half-migrated state. LOC count is irrelevant; the substrate handles 10 sites or 10,000 the same way. - **Affected-LOC enumeration** — pre-execution preview of site_count + exact_paths + re_exec_scope, structurally, not by grep. Direct answer to the user's "what are all the affected LOC" question. - **Composes per-lens transforms from §6.2** — a mechanical refactor often decomposes into per-lens auto-fixes from the L1.x catalog. Canonical-B decomposes into L1.7 transforms + L1.12 outcome (4) transforms. Agent picks the named refactor; substrate composes the per-lens transforms that implement it. - **PR #3338 as the worked example** — canonical-B across 6 languages + 7 v3 ratchet dissolutions, two operator decisions ("use decl-ref for Bool" + "dissolve the 7 v3 ratchets") plus 13 uniform per-class site applications. Hand-executed in #3338; the substrate (had it been operational) could have applied the entire refactor mechanically from those two decisions. §6.9 recommended ordering updated: (f) mechanical refactor slots between (b) L1.12 and (c) interface cascade — it's the most directly useful hero shape for day-to-day refactoring work, and demonstrates the composition pattern that the agent-shape cases (c)/(d)/(e) build on. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design-read-edit-pipeline: fix §6.10 RootScope slip — use the §2 corpus-fold idiom cursor/composer-2 review caught a slip: §6.10 wrote `auto_fix_for_lens(L1.5, RootScope)` while §2 (lines 74-77) explicitly rules out RootScope as a scope variant ("no separate RootScope / corpus-wide variant — corpus-wide application is achieved by composition over the declaration set"). Replaced the RootScope call with the explicit fold over `declarations_in(dag)`: declarations_in(dag).for_each(d => auto_fix_for_lens(L1.5, DeclarationScope(d)) ) Added clarifying sentence: "auto_fix_for_lens itself takes a SectionRef (DeclarationScope or NodeScope) — never an invented RootScope." Keeps the doc internally consistent on the single structural scope vocabulary per INVARIANTS P2 / Practice 5. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: track L1.12 concept-identity carriers as §6.8 item 8 + §6.4 dependency caveat codex BLOCKING (sha:77469d84) raised two findings; one valid, one factually wrong. **Finding 1 — valid.** L1.12 concept identity depends on undeclared registry carriers (CanonicalConcept, ConceptDisambiguation, HistoricalDeclaration). Verified absent from src/v4/std/*.dag, src/v4/lens/*.dag, src/v4/extdeps/*.dag — they only exist as design in docs/design-dissolution-lens.md (PR #3334, operator manual-merge queue), not as ratified .dag substrate. Fix: - Added §6.8 item 8 explicitly tracking the L1.12 concept-identity carriers as missing substrate (alongside item 1 machine-readable Clean shapes, item 2 ConditionalDiff ADT, etc.). Lists the three carrier shapes and notes the design-pending status. - Added a dependency caveat callout at the top of §6.4 hero case (b) pointing at §6.8 item 8 so a reader hitting the example sees the carrier-not-yet-substrate dependency immediately. Finding 2 — factually wrong (rebutted on-PR, not in this commit). THESIS.md:232 explicitly carries the retraction with the "operator-ratified 2026-05-15" stamp. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: add §5 Example B dependency caveat matching §6.4 Same finding fired again at line 255 of pre-fix sha (§5 Example B "rename a concept across the corpus", which also references CanonicalConcept). The global §6.8 item 8 + §6.4 inline caveat from 07d862f cover the case, but a reader entering at §5 Example B should see the dependency callout immediately — same shape as the §6.4 callout. Both inline caveats point at §6.8 item 8 as the global tracking entry. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design-read-edit-pipeline: candidate root explicit in gate surface + LOC rename openai-pro REQUEST_CHANGES on f3d146b raised two valid design-level findings; both addressed. **Finding 1 — candidate authority not typed into gate surface.** The candidate-state pattern from earlier was correct in intent, but the worked examples called `apply_lens(_, ref, Enforce)` with a bare ref — leaving the candidate-vs-pre-edit context to a prose comment ("evaluated in candidate_dag context"). A worker following the pseudo-code could accidentally enforce against the wrong root. Fix: introduce `scope_in(root: Node, ref: NodeRef) -> SectionRef` as the helper that **explicitly binds a frontier ref to a dag root**. Updated §4 pipeline + §5 Example A + §6.3 catamorphism + §6.6 CLI + §6.7b mechanical refactor — every gate call now reads `apply_lens(_, scope_in(candidate_dag, ref), Enforce)`. The candidate root is structurally visible in every call; can't be lost via comment-level convention. **Finding 2 — "affected LOC" reintroduces file/line authority before Node→File binding exists.** §6.7b promised "affected LOC" structurally — but §1 explicitly says file/line is emergent-not-substrate. Promising LOC enumeration before the Node→File binding registry (§6.8 item 6) is built contradicts the node-centric framing. Fix: rename §6.7b "Affected-LOC enumeration" → "Affected-structural- paths enumeration"; the inline preview computes structural Paths, not file:line. Added a callout explicitly tying the LOC translation to the Node→File binding registry (§6.8 item 6) — until that registry lands, the substrate-native answer is in terms of Paths. LOC is the downstream projection of "affected sites" via emit's mapping; the substrate-native fact is "affected structural sites." Also updated the "guarantee is structural" close-out: "LOC count is irrelevant" → "Site count is irrelevant." Keeps the doc consistent that the substrate-native unit is the Path/site, not LOC. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design-read-edit-pipeline: fix §6.10 auto_fix_for_lens straggler — scope_in everywhere codex APPROVE_WITH_COMMENTS caught one remaining apply_lens call site I missed in the prior candidate-authority pass: §6.10 auto_fix_for_lens workflow at line 851 still used `apply_lens(lens, ref, Enforce)` with the bare ref. Fixed to `apply_lens(lens, scope_in(candidate_dag, ref), Enforce)` matching §4's "candidate root explicit in the gate surface" rule and the rest of the worked examples. Verified: only remaining `apply_lens(_, ref, Enforce)` in the doc is the §4 anti-pattern call-out itself (explaining what NOT to do). All actual call sites are consistent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…— coordi

briansrls · 2026-05-19T18:20:38Z

Verified against current head 80e1c52a9d62eac83133358d0a3863036255d81e: this finding is already addressed on tip. coverage_defect_acceptance_dag_test.rs now filters parsed rows with name.starts_with("coverage_defect_"), and INVARIANTS.md now describes the parsed (coverage_defect_* data row, CoverageDefectKey variant) set. I also re-ran the focused remote test: cargo test -p v3-compiler coverage_defect_acceptance --test integration passed via BuildBuddy invocation 9815f1cd-97e7-4b8c-ab62-32d720367e79. — sent from warm-koi-304

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 80e1c52a · Trigger: schedule
Thinking: 330s wall

Non-blocking — Strengths

src/v4/lens/coverage.dag The substrate coproduct is tagged and ledgered as a bounded scaffold, with the hand-authored key rows ratcheted until generated coverage can derive them.

ROADMAP — Verified

T-PB-B / pb_rust_tests_outside_residual_zero: The new Rust parse ratchet has the matching SG-0 census row, INVARIANTS P5 receipt, and PR-body append receipt.

✅ No blocking concerns in the changed lines.

briansrls changed the title ~~PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution — coordinate jolly-ibex-599 (Lane A)~~ PREFIX dissolution lens L1.1-L1.12 acceptance keys May 18, 2026

briansrls marked this pull request as ready for review May 18, 2026 19:08

briansrls added 6 commits May 18, 2026 19:25

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

e8060ba

…— coordi

Ratchet PREFIX dissolution lens acceptance rows

b3cfd8c

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

e74f755

…— coordi

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

c607917

…— coordi

Receipt PREFIX dissolution lens key ledger

2bf2413

Add SG-0 pairing receipt for PR 3318

d4f1322

briansrls force-pushed the session/warm-koi-304 branch from 31cd608 to d4f1322 Compare May 18, 2026 19:28

briansrls added 3 commits May 18, 2026 19:32

Fix PR 3318 SG-0 dispatch evidence

4624d6e

Correct PR 3318 SG-0 net delta

feca0cb

Tighten dissolution coverage row ratchet

b258a10

briansrls commented May 18, 2026

View reviewed changes

Comment thread src/v4/DECISIONS.md Outdated

briansrls added 4 commits May 18, 2026 16:01

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

b1184bf

…— coordi

Reclassify dissolution lens key scaffold

8ad0b86

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

f9c2e14

…— coordi

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

084fb00

…— coordi

briansrls marked this pull request as draft May 18, 2026 20:21

briansrls commented May 18, 2026

View reviewed changes

briansrls added 2 commits May 18, 2026 17:11

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

57a722b

…— coordi

Resolve dissolution lens design conflict

83e7c91

briansrls mentioned this pull request May 18, 2026

design-dissolution-lens: stabilize #3313 — L1.11/L1.12 fixes + canonical L1.x keys #3334

Merged

4 tasks

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

a7fedd0

briansrls marked this pull request as ready for review May 18, 2026 22:25

Align coverage lens receipt with ratchet

12076e2

briansrls commented May 18, 2026

View reviewed changes

briansrls added 2 commits May 18, 2026 22:47

Ratchet dissolution lens key variants

ac55359

Tighten dissolution lens key scaffold receipt

e9e3eab

briansrls commented May 18, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

a666ed1

briansrls added 4 commits May 18, 2026 21:35

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

0ffa201

…— coordi

Resolve PR 3318 main merge conflicts

2605234

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

5b3b280

…— coordi

Align dissolution coverage keys with canonical L1.10 split

274f8c2

briansrls commented May 19, 2026

View reviewed changes

briansrls added 2 commits May 19, 2026 02:49

Receipt retired L1.6 dissolution coverage key

e3347bc

Keep dissolution key tag adjacent

69465d9

briansrls commented May 19, 2026

View reviewed changes

briansrls added 2 commits May 19, 2026 06:08

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

6dc84bd

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

7d01e71

# Conflicts: # src/v4/DECISIONS.md

briansrls commented May 19, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

1b57cec

briansrls commented May 19, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/warm-koi-304

1a75f0d

briansrls commented May 19, 2026

View reviewed changes

briansrls added 2 commits May 19, 2026 14:13

WIP: PREFIX lens Acceptance batch (d): Wave-2 L1.1–L1.12 dissolution …

f36f4ec

…— coordi

Remove program markers from coverage defect ratchet

80e1c52

briansrls merged commit a982d95 into main May 19, 2026
7 checks passed

briansrls commented May 19, 2026

View reviewed changes

briansrls deleted the session/warm-koi-304 branch June 1, 2026 18:43

Conversation

briansrls commented May 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Notes

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 18, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 19, 2026

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 18, 2026 •

edited

Loading