diff --git a/INVARIANTS.md b/INVARIANTS.md
index a166297bba7..7a7243818e9 100644
--- a/INVARIANTS.md
+++ b/INVARIANTS.md
@@ -178,7 +178,7 @@ A canonical accessor exists (e.g., a reflected substrate function), but a second
 
 ### Interim receipt: `v4.extdeps/languages/*` `compile_to_dag` smokes and `GroundingMap` / `Symbol`
 
-The pinned `compile_to_dag(include_str!(…), path)` integration smokes in §P5(b) (`v4_extdeps_*_dag_smoke_test.rs`) compile **one `.dag` source string in isolation**. On that path the compiler does **not** merge sibling-module bodies for `import v4.extdeps.languages.resolver { … }`, and under **M1(2.7)** `import v4.std.node { Symbol }` is not populated into the declaration table either. Until the smoke harness loads a multi-module **bundle** that includes the shared home or import-lowering closes those gaps, `lean.dag` and `cpp.dag` carry **structural twins** of the ratified `extdeps/languages/resolver.dag` surface (`GroundingMap`, and where needed bodiless `Symbol`), each tagged with a one-line pointer to **DECISIONS.md D4**. `machine_code.dag` keeps the local `Symbol` twin on the same M1(2.7) path but **omits** a `GroundingMap` twin after **D2-REV** (no spelling-only resolver rows on that slice). Treat as **P2-staging**: one named mechanical shape, one dissolution trigger (`resolver.dag` + smoke bundle, or M1(2.7) std-node import), not silent divergent semantics. `rust.dag` continues to import `Symbol` from `v4.std.node` where the full bootstrap path applies.
+The pinned `compile_to_dag(include_str!(…), path)` integration smokes in §P5(b) (`v4_extdeps_*_dag_smoke_test.rs`) compile **one `.dag` source string in isolation**. On that path the compiler does **not** merge sibling-module bodies for `import v4.extdeps.languages.resolver { … }`, and under **M1(2.7)** `import v4.std.node { Symbol }` is not populated into the declaration table either. **`GroundingMap` twin — retired (A-vs-B = B / ruled-B).** The `{spelling}` `GroundingMap` resolver-twin shape is now retired from **every** `extdeps/languages/*` slice: a bare D2 alias plus a spelling label asserts a grounding instead of demonstrating it (the hollow form the machine-readable-inhabitance bar forecloses), so under ruled-B no slice carries spelling-only resolver rows — `machine_code.dag` (omitted after **D2-REV**), and now `rust.dag`, `cpp.dag`, `lean.dag` (and `go.dag`, `python.dag`, `typescript.dag`) likewise carry **no** `GroundingMap` twin. The grounding *declaration* `data <lang>_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` (a decl-ref referencing the single `std/logic.dag` authority) is present and **v2-parse/resolve-verified** (0 diagnostics, `v2-compiler compile --source-root src/v4`, ci.yml `v4:` job; v2-*run* T-22-deferred → parse/resolve-verified, not execute-verified). **This is an E-6 *bounded exception* (clause (b)), not speculative metadata.** No same-PR consumer reads `<lang>_bool_grounding` — the canonical/coincidence fold consumer is *specified-not-realized* (`node.dag` B1-CANON contract; the fold is `[MODELED]`). E-6 explicitly permits a consumer-less target-spec decl that **sits behind a named scaffold marker with a dissolution trigger**: each declaration carries the inline marker `🟡 feature:canonical-b-grounding-consumer` with an explicit trigger — *dissolves when the B1-CANON canonical/content_hash fold + coercion zip-fold (`DECISIONS.md` B1 · T-9/C1) consume the row for coincidence-checking*. So the *shape* is the ratified canonical-B decl-ref; the *authority state* is **staging behind the E-6-named scaffold** (consumer-gated), not landed and not advisory (`docs/modeling/grounding-worked-examples.md` §0). The frozen v3 isolated-smoke ratchets reject decl-ref `data` bodies — a v3-only artifact (v3 is **FROZEN 2026-05-15** and **not** in the v2→v4 bootstrap chain). They are **DISSOLVED in this PR** (operator-authorized 2026-05-18 via PM `sunny-wolf-435`): the `v4_extdeps_{cpp_abi,cpp,typescript,machine_code,lean}_dag_smoke_test.rs`, `v4_std_fact_density_dag_smoke_test.rs`, **and `v4_lens_cost_dag_smoke_test.rs`** probes (**7 total**), their `mod` lines in `integration.rs`, these §P5(b) rows, and the matching `EXPECTED_HAND_AUTHORED_TEST` rows in `sg0_census_test.rs` are removed together (P5 = dissolution, not deactivation). For the **6 parse smokes** the authoritative v4 parse gate (genuinely equivalent — no coverage loss) is the CI `v4:` job's `v2-compiler compile --source-root src/v4` (v2→v4 bootstrap-viability per `src/v4/STRUCTURE.md`); a `compile_to_dag` parse-cleanliness probe is exactly what the whole-tree parse subsumes. (`v4_lens_cost_dag_smoke_test.rs` — the P9/T-12 cost-lens authority ratchet — was added by operator-extended authorization 2026-05-18, but is **NOT the same class** as the 6 and the whole-tree parse does **not** substitute it: `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`). That property currently **holds structurally** on `main` (one `fn llvm_instruction_cost` at `src/v4/lens/cost.dag:39`, none in `llvm_ir.dag`) but its regression-guard is removed with no equivalent gate. **Named tracked coverage gap (not "no coverage loss"):** re-express the P9 single-owner authority as a `.dag` `TestClaim` / generated structural check — scaffold `feature:p9-llvm-instruction-cost-single-owner`, dissolves when that check lands. Operator authorized the dissolution as a frozen-v3 ratchet with this residual gap explicitly named, not papered.) The local `type Symbol` twin in `lean.dag` / `machine_code.dag` stays in those `.dag` files (harmless under v2; its isolated-smoke rationale is now moot — twin removal is a deferred, separate substrate cleanup, not bundled here). The `GroundingMap`→`resolver.dag` **relocation** obligation (move the per-file twin into a shared `resolver.dag` home, D4) is therefore **obsolete for the removed twin shape** — the twin is deleted, not relocated. This is scoped strictly to that retired per-file `GroundingMap` twin; it does **not** cancel, supersede, or bear on any independent shared-`resolver.dag` / D4 work that exists for other reasons. **`Symbol` twin — still P2-staging.** Until the smoke harness loads a multi-module **bundle** or M1(2.7) std-node import-lowering closes the gap, `lean.dag` retains only a local bodiless `type Symbol` twin (the M1(2.7) isolated-smoke enabler), tagged with a one-line pointer to **DECISIONS.md / P2**; `machine_code.dag` keeps the same local `Symbol` twin. Treat the `Symbol` twin as **P2-staging**: one named mechanical shape, one dissolution trigger (smoke bundle, or M1(2.7) std-node import), not silent divergent semantics. `cpp.dag` carries no twin (it references neither). `rust.dag` continues to import `Symbol` from `v4.std.node` where the full bootstrap path applies.
 
 ### Problem shape: Consumer reverse-engineers storage shape
 
@@ -365,13 +365,6 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
 | `src/v3/compiler/tests/integration/common/wiring_scanner_test.rs` | **ROADMAP:** same **v3 lens capability honesty pass** bullet — Band-C `tests/integration.rs` `#[path]` wiring is enforced by `integration_rs_wiring_scan.rs` + `cementing_dispatch.rs`. **Dissolution:** remove when `integration.rs` wiring can be validated structurally for cementing modules without line scanners. **Interim ratchet:** unit tests for helpers promoted from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
 | `src/v3/compiler/tests/integration/ctrl_pr_digests_dag_smoke_test.rs` | **Project plan:** `docs/r4-ctrl-dag-migration-project-plan.md` §3 — catalog **#8** `dsl/ctrl/pr_digests.dag` (Wave-1 ctrl → `.dag` subsystem modeling). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + the matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke test. **Dissolution:** remove when `compile_to_dag` (or a single generated harness) validates `module … service …` ctrl carrier files end-to-end without a parallel Rust string/lexer ratchet, or when the contract migrates to `.dag` `TestClaim` coverage. **Interim ratchet:** `ctrl_pr_digests_dag_tokenizes_and_matches_expected_surface` requires clean tokenization plus presence of `module ctrl.pr_digests`, `import extdeps.github.pulls { PullRequest, PullReview, ReviewComment }`, `std.errors` / `std.types` imports, the four Practice-4 sum/record carriers (with `🟡 STAGED` / `🟢 TERMINAL` markers per `dsl/ctrl/README.md`), `ReviewCommentBody` + `review_line_comments` wiring, and `service ctrl.PrDigests` / the four `operation` blocks / `readonly`. |
 | `src/v3/compiler/tests/integration/extdeps_sql_transport_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; this Rust integration receipt keeps HTTP/SQL/audit extdeps compiled by the existing v3 parser before downstream emission-target consumers rely on them. **Dissolution:** remove when extdeps transport and Phase 3 emission-target files are covered by a `.dag`-native parse/authority suite or generated test harness rather than per-file Rust `compile_to_dag` probes. **Interim ratchet:** `rest_transport_dag_compiles_cleanly` and `sql_transport_dag_compiles_cleanly` pin `dsl/extdeps/transports/rest.dag` and `dsl/extdeps/transports/sql.dag`; `http_server_extdep_dag_compiles_cleanly`, `sql_migration_extdep_dag_compiles_cleanly`, and `audit_event_extdep_dag_compiles_cleanly` pin `dsl/extdeps/http/server.dag`, `dsl/extdeps/sql/migration.dag`, and `dsl/extdeps/audit/event.dag` as parseable staged emission-target substrate. The field-sensitive companions (`http_server_target_fields_are_authoritative_substrate_edges`, `sql_migration_target_fields_bound_raw_sql_scaffold`, `audit_event_target_fields_preserve_cloudevents_core_names`) consume the new target-contract fields directly so they fail on raw `String`/`Int` regressions, missing SQL scaffold bounds, or CloudEvents alias drift while the first real projection consumer is still staged; the audit ratchet also locks CloudEvents core fields to branded carriers and `std.types.Timestamp` rather than raw strings. |
-| `src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-29 C++ ABI / target data-model feeder (`src/v4/extdeps/cpp_abi.dag`, consumed by T-4 `cpp.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/cpp_abi.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_cpp_abi_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
-| `src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4 C++ language-model lane (`src/v4/extdeps/languages/cpp.dag`, DECISIONS.md D2 / P4-3208 `CppBool` surface). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/languages/cpp.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_cpp_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
-| `src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4 typescript language-model lane (`src/v4/extdeps/languages/typescript.dag`, DECISIONS.md D2 resolver slice). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/languages/typescript.dag` (or the v4 extdeps fixture set it belongs to) is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_typescript_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
-| `src/v3/compiler/tests/integration/v4_lens_cost_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** **T-12** (`lens/complexity.dag + lens/cost.dag`); **Audit:** `docs/audit/dissolution-inventory.md` **P9** (`lens/cost.dag` cost-of-instruction model fact / lens). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the ratchet. **Dissolution:** remove when the P9 single-authority claim is exercised by `.dag` `TestClaim` rows / a generated harness without this host parser-backed test. **Interim ratchet:** `v4_lens_cost_owns_llvm_instruction_cost_table` tokenizes/parses `src/v4/lens/cost.dag` and `src/v4/extdeps/languages/llvm_ir.dag`, then asserts exactly one parsed `llvm_instruction_cost` declaration under `v4.lens.cost` and zero parsed declarations in `llvm_ir.dag`. |
-| `src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4.13 (`src/v4/extdeps/languages/machine_code.dag`, DECISIONS.md L-3 / P4-3208). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `machine_code.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_machine_code_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
-| `src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** B-2 / DECISIONS.md L-4 (`src/v4/extdeps/languages/lean.dag`, PROOF-1 prover surface / P4-3208). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `lean.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_lean_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
-| `src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs` | **TASKS.md** **T-30** (`src/v4/TASKS.md` — structural hollow-alias / fact-density gate); **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **Spec:** `docs/modeling-discipline.md` **Practice 8** — *Interim floor: the hollow-alias discriminator* (Practice 8 *Interim floor* on `main` post-#3226 `77b9e7d72` + Practice 9 #3234 `125fc88c8`; diff `main` if §8/§9 drift). **P2 / Practice 5:** this smoke is a **parse + inference cleanliness** probe for `src/v4/std/fact_density.dag` only — it does **not** claim a **generated** substrate consumer for `SourceSpecReadFact` (INVARIANTS §P2: declaration without generated consumer = staging; see `STRUCTURE.md`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/std/fact_density.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_std_fact_density_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. |
 | `src/v3/compiler/tests/integration/file_attachment_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` (T-Workflow-As-Data substrate-gap class; worker brief `docs/briefs/r3-substrate-gate-62-file-attachment-carrier-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `FileAttachment` field names + cross-module nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `timing_lens_substrate_carrier_test.rs` for gate #55). **Interim ratchet:** `file_attachment_shape_locked` + `file_attachment_field_types_locked` + `file_attachment_field_count_is_five` pin the ratified Refined-B-1 five-field subset of `WorkflowObservationAnchor` (`NodeId`, `ContentHash`, `WorkflowProducerId`, `WorkflowRunId`, `Nanoseconds`) exactly as declared in `src/v3/std/timing_lens.dag`; existence proof carrier construction stays in-module as `gate_62_file_attachment_demo_record`. |
 | `src/v3/compiler/tests/integration/lens_application_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#89** `section_ref_substrate_landed` (T-Lens-Application-Surface — `SectionRef` disjoint sum over `DeclarationScope` and `NodeScope` in `src/v3/std/lens_application.dag`; design authority `docs/design-lens-application-surface.md` §1.2–§2). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the harness. **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `SectionRef` variant labels, field names, and `DeclarationId` / `NodeId` nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as gate **#62** `file_attachment_substrate_carrier_test.rs`). **Interim ratchet:** `gate_89_section_ref_is_disjoint_sum_from_lens_application_authority` pins variant order (`DeclarationScope` then `NodeScope`) and payload fields to `lens_application.dag`. |
 | `src/v3/compiler/tests/integration/workflow_substrate_carriers_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#53** `workflow_substrate_carriers_landed` (T-Workflow-As-Data Slice 1; worker brief `docs/briefs/r3-substrate-t-workflow-as-data-slice-1-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `WorkflowSecret`, `SecretScope`, `CronSchedule`, and `CronField` structural shape against `generated_full_bootstrap_dag()` without this hand-Rust ratchet. **Interim ratchet:** `workflow_secret_shape_locked` + `secret_scope_variants_locked` + `cron_schedule_shape_locked` + `cron_field_variants_locked` pin the Slice 1 β-ratified carriers (STOP+PING discipline on `CronSchedule` field-count drift >5 per brief). |
diff --git a/docs/modeling/grounding-worked-examples.md b/docs/modeling/grounding-worked-examples.md
index 3cf829b967a..7f83e03362c 100644
--- a/docs/modeling/grounding-worked-examples.md
+++ b/docs/modeling/grounding-worked-examples.md
@@ -290,6 +290,121 @@ overflow at the emit boundary.
 
 ## Per-target carrier groundings
 
+## 0. `bool` / `!` — grounding at the primitive level (the base case of one universal discipline)
+
+**There are no "quirked" types.** *Every* external type is grounded in
+our primitives. The only question is **at what level the grounding
+starts**: most types start as a **refinement some level above a
+primitive**; a genuinely boutique type starts from the **raw
+primitives** and is built up. `bool` is the base case only because it
+sits *so close to a primitive* that there is almost nothing to get
+wrong — not because it is a different category. We model each
+language's type by **reading that language's spec for that type** (we
+are modeling the spec), then expressing it in our vocabulary at the
+appropriate level. Modeling accuracy is fundamentally an *integration*
+problem — it is iterative and validated by testgen against the target
+(separate followup), not asserted.
+
+**The retired shape (D2a).** The pre-ruling form asserted identity by a
+label + a spelling string:
+
+```
+type RustBool = Bool                                   // bare D2 assertion
+data rust_bool_grounding: GroundingMap<RustBool> = GroundingMap {
+  spelling: "bool"                                      // identity by a label string
+}
+```
+
+`"bool"` is prose a checker cannot walk — the hollow form the
+machine-readable-inhabitance bar forecloses. "Identity is a claim
+discharged by the fold, never an assertion."
+
+**The ratified shape (canonical-B) — declaration present, P2/E-6
+staging.** The grounding *declaration* is a real, fold-traversable edge
+that **references the single std authority** for the shared structure:
+
+```
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
+// Anchor: <the language's own bool spec>
+data <lang>_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
+```
+
+This is not an assertion: it grounds the language's `bool`, *read from
+that language's spec*, into the shared `std/logic` + `std/algebra`
+vocabulary by pointing at the one authoritative `BooleanAlgebra<Bool>`
+instance (`std/logic.dag`). A checker walks `<lang>_bool_grounding` →
+the real `bool_boolean_algebra` structure; coincidence with std `Bool`
+is then a structural fact the fold discharges, not a label. **One
+authority** (no per-file algebra duplication — M2); codewide
+improvements to the bool concept centralise there, and any future
+divergence is *fold-rechecked*, not silently inherited (the
+centralisation/drift resolution). `!` grounds to the std `Never`
+primitive directly (`type RustNever = Never`) — zero inhabitants, no
+structure above the primitive, so the primitive identity *is* the
+complete grounding (the degenerate base of the same discipline).
+
+**Verified scope (honest) — declaration, not landed authority.** The
+declaration compiles **0 diagnostics under the real bootstrap gate** —
+`v2-compiler compile --source-root src/v4` (ci.yml `v4:` job; 72 modules
+resolved). That is the *parse/resolve* half of bootstrap viability; the
+v2-**run** gate is T-22-deferred. Crucially this is **not** landed
+target-spec authority: no same-PR consumer reads `<lang>_bool_grounding`
+(the canonical/coincidence fold — the consumer — is
+*specified-not-realized*: `node.dag` B1-CANON contract, `[MODELED]`).
+**INVARIANTS E-6 permits this as a *bounded exception* (clause (b))** —
+a consumer-less target-spec decl that **sits behind a named scaffold
+marker with a dissolution trigger**: each `data <lang>_bool_grounding`
+carries the inline marker `🟡 feature:canonical-b-grounding-consumer`
+that dissolves when the B1-CANON fold + coercion zip-fold
+(`DECISIONS.md` B1 · T-9/C1) consume it for coincidence-checking. So the
+*shape* is the ratified canonical-B decl-ref and parse-verified; the
+*authority state* is **staging behind the E-6-named scaffold** —
+consumer-gated, not landed, **not** speculative metadata — claimed no
+further. (Aside: the frozen v3 interim parse-ratchets reject decl-ref
+`data` bodies — a v3-only artifact, v3 is *not* in the bootstrap chain;
+they are **dissolved in this PR** under operator authorization, with the
+v2 `v4:` job as the replacement parse gate.)
+
+**The level spectrum — bool vs int (the lesson).** Same discipline,
+different starting level:
+
+- **`bool`** — starts *at* the primitive: `bool` *is* the shared
+  2-element `BooleanAlgebra`. The grounding is the bare reference; no
+  build-up. (Rust / C++ / Go / Lean / TS bool all read this way from
+  their specs — strictly two values, standard ops, no object/null
+  semantics — so all use the identical shared reference.)
+- **`int`** — starts as a **refinement above** the primitive. Per
+  `std/integer.dag`, `Int = GroupCompletion<Nat>` is unbounded ℤ and
+  does **not** model overflow; `Int64 = Compose<Int,
+  MachineWidth<Word64>>` is `Int` *refined* by a width dimension, and
+  overflow is that refinement's boundary predicate. Python `int`
+  (arbitrary precision) grounds to bare `Int`; Rust `i64` grounds to
+  the `Compose` refinement + an overflow disposition — **same shared
+  `Int`, different spec-sourced refinements.**
+- **Python `bool`** — the worked deviation. The Python data model says
+  `bool` *is a subtype of `int`* (`True == 1`). So Python's bool reads
+  as: the shared truth grounding (`py_bool_grounding` → the same
+  authority) **plus** numeric-tower membership — carried by the
+  existing `PythonNumericTower.BoolLevel` classifier, the build-up
+  above the primitive. (Object/singleton *identity* is a runtime-layer
+  fact, outside the type model — the placement axis.) This is a *first
+  iteration*; the exact build-up shape is expected to refine as testgen
+  pressure-tests it against CPython.
+
+The contrast is the whole point: there is one grounding engine —
+*reference the shared authority for what the spec says is shared, build
+up from the primitives for what the spec says deviates.* `bool` is
+where the build-up is empty; `int` and Python-`bool` are where it
+isn't. None of them are special-cased.
+
+**Coercion shape.** `bool`: the fold compares canonical `Node` forms
+leaf-to-leaf (`True`↔`True`, `False`↔`False`) — identity-quality
+`Produced`; no width/sign/unit coordinate to drop or fabricate (the
+clean endpoint). `!`: `Never` has no inhabitants, so `T -> Outcome<!>`
+can only be `Rejected` (fail-closed by construction) and
+`! -> Outcome<T>` is the unique empty map (ex falso, vacuously total).
+
 ## 1. Rust — `[T; N]` (const generics, compound coercion)
 
 **Model** — grounded from the Rust Reference array type:
diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs
index 9ab9ce7d823..a87f7560825 100644
--- a/src/v3/compiler/tests/integration.rs
+++ b/src/v3/compiler/tests/integration.rs
@@ -273,20 +273,6 @@ mod thesis_validation_test;
 mod timing_lens_substrate_carrier_test;
 #[path = "integration/v2_oracle_no_remaining_test_consumers_test.rs"]
 mod v2_oracle_no_remaining_test_consumers_test;
-#[path = "integration/v4_extdeps_cpp_abi_dag_smoke_test.rs"]
-mod v4_extdeps_cpp_abi_dag_smoke_test;
-#[path = "integration/v4_extdeps_cpp_dag_smoke_test.rs"]
-mod v4_extdeps_cpp_dag_smoke_test;
-#[path = "integration/v4_extdeps_lean_dag_smoke_test.rs"]
-mod v4_extdeps_lean_dag_smoke_test;
-#[path = "integration/v4_extdeps_machine_code_dag_smoke_test.rs"]
-mod v4_extdeps_machine_code_dag_smoke_test;
-#[path = "integration/v4_extdeps_typescript_dag_smoke_test.rs"]
-mod v4_extdeps_typescript_dag_smoke_test;
-#[path = "integration/v4_lens_cost_dag_smoke_test.rs"]
-mod v4_lens_cost_dag_smoke_test;
-#[path = "integration/v4_std_fact_density_dag_smoke_test.rs"]
-mod v4_std_fact_density_dag_smoke_test;
 #[path = "integration/value_body_substrate_mirror_isomorphism_test.rs"]
 mod value_body_substrate_mirror_isomorphism_test;
 #[path = "integration/common/wiring_scanner_test.rs"]
diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs
index 8f851915e22..bdb41501a94 100644
--- a/src/v3/compiler/tests/integration/sg0_census_test.rs
+++ b/src/v3/compiler/tests/integration/sg0_census_test.rs
@@ -828,22 +828,6 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
     // R3 T-V2-Retirement §1.8 gate #41 (`v2_oracle_no_remaining_test_consumers`): comment-aware
     // source ratchet — no `v2-compiler` crate references outside `src/v2/`.
     "src/v3/compiler/tests/integration/v2_oracle_no_remaining_test_consumers_test.rs",
-    "src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs",
-    "src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs",
-    // T-4.13 / B-2: `compile_to_dag` smoke on `machine_code.dag` / `lean.dag` (zero module diagnostics).
-    "src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs",
-    "src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs",
-    // T-4 TypeScript primitive scaffold: `compile_to_dag` smoke on
-    // `src/v4/extdeps/languages/typescript.dag` (zero module diagnostics).
-    // SG-0 ratchet per INVARIANTS §P5(b) + `extdeps_sql_transport_test` precedent.
-    "src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs",
-    // P9 / T-12 cost-lens authority ratchet: parsed single-owner check for
-    // `llvm_instruction_cost` moving from LLVM IR shape model to v4 cost lens.
-    // SG-0 + INVARIANTS §P5(b) receipt.
-    "src/v3/compiler/tests/integration/v4_lens_cost_dag_smoke_test.rs",
-    // T-30: `compile_to_dag` smoke on `src/v4/std/fact_density.dag` (Practice 8
-    // structural mirror in `v4_hollow_alias_gate`). SG-0 + INVARIANTS §P5(b) receipt.
-    "src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs",
     // §1.8 gate #96 (`value_body_substrate_mirror_isomorphism_executable`):
     // CI-visible generated Rust `ValueBody` mirror vs `substrate.dag`
     // constructor isomorphism. Dissolves when `ValueBody` no longer has a
diff --git a/src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs
deleted file mode 100644
index 6588101635e..00000000000
--- a/src/v3/compiler/tests/integration/v4_extdeps_cpp_abi_dag_smoke_test.rs
+++ /dev/null
@@ -1,27 +0,0 @@
-//! **Layer:** integration
-//!
-//! Smoke `compile_to_dag` on `src/v4/extdeps/cpp_abi.dag` — T-29's
-//! C++ ABI / target data-model slice must lower+infer with zero module
-//! diagnostics before `cpp.dag` fact-bundles consume it.
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const CPP_ABI_DAG: &str = include_str!("../../../../v4/extdeps/cpp_abi.dag");
-const CPP_ABI_PATH: &str = "src/v4/extdeps/cpp_abi.dag";
-
-#[test]
-fn v4_extdeps_cpp_abi_dag_compiles() {
-    match compile_to_dag(CPP_ABI_DAG, CPP_ABI_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{CPP_ABI_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{CPP_ABI_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{CPP_ABI_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs
deleted file mode 100644
index b8cf3c94641..00000000000
--- a/src/v3/compiler/tests/integration/v4_extdeps_cpp_dag_smoke_test.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! **Layer:** integration
-//!
-//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/cpp.dag` — T-4 C++
-//! LanguageModel D2-resolver slice must lower+infer with **zero** module diagnostics.
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const CPP_DAG: &str = include_str!("../../../../v4/extdeps/languages/cpp.dag");
-const CPP_PATH: &str = "src/v4/extdeps/languages/cpp.dag";
-
-#[test]
-fn v4_extdeps_cpp_dag_compiles() {
-    match compile_to_dag(CPP_DAG, CPP_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{CPP_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{CPP_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{CPP_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs
deleted file mode 100644
index 136992035c4..00000000000
--- a/src/v3/compiler/tests/integration/v4_extdeps_lean_dag_smoke_test.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! **Layer:** integration
-//!
-//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/lean.dag` — B-2 / L-4
-//! Lean LanguageModel must lower+infer with **zero** module diagnostics.
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const LEAN_DAG: &str = include_str!("../../../../v4/extdeps/languages/lean.dag");
-const LEAN_PATH: &str = "src/v4/extdeps/languages/lean.dag";
-
-#[test]
-fn v4_extdeps_lean_dag_compiles() {
-    match compile_to_dag(LEAN_DAG, LEAN_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{LEAN_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{LEAN_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{LEAN_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs
deleted file mode 100644
index e59df6dd3d1..00000000000
--- a/src/v3/compiler/tests/integration/v4_extdeps_machine_code_dag_smoke_test.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! **Layer:** integration
-//!
-//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/machine_code.dag` —
-//! T-4.13 machine-code model must lower+infer with **zero** module diagnostics.
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const MACHINE_CODE_DAG: &str = include_str!("../../../../v4/extdeps/languages/machine_code.dag");
-const MACHINE_CODE_PATH: &str = "src/v4/extdeps/languages/machine_code.dag";
-
-#[test]
-fn v4_extdeps_machine_code_dag_compiles() {
-    match compile_to_dag(MACHINE_CODE_DAG, MACHINE_CODE_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{MACHINE_CODE_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{MACHINE_CODE_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{MACHINE_CODE_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs
deleted file mode 100644
index 4ee8525ac70..00000000000
--- a/src/v3/compiler/tests/integration/v4_extdeps_typescript_dag_smoke_test.rs
+++ /dev/null
@@ -1,27 +0,0 @@
-//! **Layer:** integration
-//!
-//! Smoke `compile_to_dag` on `src/v4/extdeps/languages/typescript.dag` —
-//! T-4 TypeScript primitive scaffold must lower+infer with **zero** module
-//! diagnostics while the fact-bundle Phase-3 rework is gated.
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const TYPESCRIPT_DAG: &str = include_str!("../../../../v4/extdeps/languages/typescript.dag");
-const TYPESCRIPT_PATH: &str = "src/v4/extdeps/languages/typescript.dag";
-
-#[test]
-fn v4_extdeps_typescript_dag_compiles() {
-    match compile_to_dag(TYPESCRIPT_DAG, TYPESCRIPT_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{TYPESCRIPT_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{TYPESCRIPT_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{TYPESCRIPT_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v3/compiler/tests/integration/v4_lens_cost_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_lens_cost_dag_smoke_test.rs
deleted file mode 100644
index 188a63b9847..00000000000
--- a/src/v3/compiler/tests/integration/v4_lens_cost_dag_smoke_test.rs
+++ /dev/null
@@ -1,70 +0,0 @@
-//! **Layer:** integration
-//!
-//! Ratchet P9's LLVM instruction cost-table move to the cost-lens authority.
-
-use v3_compiler::parse_for_test;
-use v3_compiler::parse_surface::SurfaceItem;
-use v3_compiler::tokenize_for_test;
-
-#[test]
-fn v4_lens_cost_owns_llvm_instruction_cost_table() {
-    let cost_lens = parse_module(
-        include_str!("../../../../v4/lens/cost.dag"),
-        "src/v4/lens/cost.dag",
-    );
-    let llvm_ir = parse_module(
-        include_str!("../../../../v4/extdeps/languages/llvm_ir.dag"),
-        "src/v4/extdeps/languages/llvm_ir.dag",
-    );
-
-    assert_eq!(
-        module_paths(&cost_lens),
-        vec![vec!["v4", "lens", "cost"]],
-        "P9 authority module should remain v4.lens.cost"
-    );
-    assert_eq!(
-        function_count(&cost_lens, "llvm_instruction_cost"),
-        1,
-        "P9 requires exactly one parsed llvm_instruction_cost declaration under v4/lens/cost.dag"
-    );
-    assert_eq!(
-        function_count(&llvm_ir, "llvm_instruction_cost"),
-        0,
-        "llvm_ir.dag must not keep a second parsed llvm_instruction_cost authority"
-    );
-}
-
-fn parse_module(source: &str, file: &str) -> v3_compiler::parse_surface::SurfaceModule {
-    let tokens = tokenize_for_test(source, file)
-        .unwrap_or_else(|diag| panic!("{file}: tokenization failed: {diag:?}"));
-    parse_for_test(&tokens, file).unwrap_or_else(|diag| panic!("{file}: parse failed: {diag:?}"))
-}
-
-fn module_paths(module: &v3_compiler::parse_surface::SurfaceModule) -> Vec<Vec<&str>> {
-    module
-        .items
-        .iter()
-        .filter_map(|item| match item {
-            SurfaceItem::Module { path, .. } => {
-                Some(path.iter().map(String::as_str).collect::<Vec<_>>())
-            }
-            _ => None,
-        })
-        .collect()
-}
-
-fn function_count(module: &v3_compiler::parse_surface::SurfaceModule, name: &str) -> usize {
-    module
-        .items
-        .iter()
-        .filter(|item| match item {
-            SurfaceItem::Fn {
-                name: item_name, ..
-            }
-            | SurfaceItem::FnExternalBody {
-                name: item_name, ..
-            } => item_name == name,
-            _ => false,
-        })
-        .count()
-}
diff --git a/src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs
deleted file mode 100644
index 4c4b0c3afd9..00000000000
--- a/src/v3/compiler/tests/integration/v4_std_fact_density_dag_smoke_test.rs
+++ /dev/null
@@ -1,39 +0,0 @@
-//! **Layer:** integration
-//!
-//! **P2 / Practice 5 (single authority):** This harness proves **parse + inference cleanliness**
-//! for the nominal `SourceSpecReadFact` carrier only (`compile_to_dag`, empty diagnostics) — it
-//! does **not** claim a **generated** substrate consumer for that type (INVARIANTS §P2: declaration
-//! without generated consumer = staging). The Practice-8 hollow predicate’s authority remains the
-//! handwritten mirror `src/v3/compiler/src/v4_hollow_alias_gate.rs` (**private** `mod` in
-//! `v3_compiler`, not `pub` API; `#[cfg_attr(not(test), allow(dead_code))]` in that file until a
-//! production consumer exists) until the generated `.dag` checker replaces it (`INVARIANTS.md`
-//! §P5(b)
-//! dissolution on that path). **Interim-floor authority** is
-//! `docs/modeling-discipline.md` Practice 8 (landed on `main`: **#3226** `77b9e7d72`;
-//! Practice 9 **#3234** `125fc88c8`).
-//!
-//! **INVARIANTS §P5 Dispatch-Discipline Mechanism (b):** this path’s SG-0 census
-//! line + matching `INVARIANTS.md` table row land in the same PR as the harness
-//! (home-of-record for the hand-Rust receipt).
-
-use v3_compiler::compile_to_dag;
-use v3_compiler::CompileError;
-
-const FACT_DENSITY_DAG: &str = include_str!("../../../../v4/std/fact_density.dag");
-const FACT_DENSITY_PATH: &str = "src/v4/std/fact_density.dag";
-
-#[test]
-fn v4_std_fact_density_dag_compiles() {
-    match compile_to_dag(FACT_DENSITY_DAG, FACT_DENSITY_PATH) {
-        Ok(dag) => assert!(
-            dag.diagnostics().is_empty(),
-            "{FACT_DENSITY_PATH}: expected empty diagnostics, got {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(CompileError::Semantic(dag)) => panic!(
-            "{FACT_DENSITY_PATH}: semantic errors: {:?}",
-            dag.diagnostics().iter().collect::<Vec<_>>()
-        ),
-        Err(other) => panic!("{FACT_DENSITY_PATH}: {other:?}"),
-    }
-}
diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md
index 76f5b81982c..448ffa17f35 100644
--- a/src/v4/DECISIONS.md
+++ b/src/v4/DECISIONS.md
@@ -120,7 +120,7 @@ remain boundary indexes until the named substrate support lands.
 | `extdeps/languages/go.dag` | (Practice-4 sum carriers + D2 partial) | Green coproduct family / records | Per merge-base `92cb26402` 🟢 blocks (see **Part 6 · CP-3229-GREEN-TERMINAL**). De-prose 2026-05-18: in-file prose removed; `GoCost` / `GoIntegerOverflowDisposition` / D2 deferrals indexed here, not in body comments. |
 | `extdeps/languages/python.dag` | (Practice-4 sum carriers + cost record) | Green coproduct family / records | Same as go row; merge-base had three 🟢 sum ledgers (see **Part 6 · CP-3229-GREEN-TERMINAL**). **Heuristic vs content (Practice 9):** mechanical `//`-line share may sit modestly above the reviewer’s ~20% *heuristic* while the file still meets **content** compliance (mandated path + four-line header + `// Anchor:` + one-line 🟢 tag per coproduct only). That is not a license to pad with blank lines to game the ratio; additional non-`//` lines should come from real substrate (e.g. more carriers/imports), not whitespace inflation. |
 | `extdeps/languages/rust.dag` | (Practice-4 sum carriers + D2 resolver) | Green coproduct family / records | Same bulk **CP-3229-GREEN-TERMINAL** receipt; `PubInPath` semantic scaffold and `RustCost` raw-`Int` bridge remain producer obligations per Part 6 / substrate tables, not narration in the `.dag` body. |
-| `extdeps/languages/typescript.dag` | `TsEcma262NumericPrimitiveKind`, `TsEcma262PrimitiveOperationSemantics`, D2 resolver scaffolds | Green coproduct family / yellow D2 deferrals | De-prose 2026-05-18: in-file prose removed; carrier declarations are byte-identical. `TsEcma262NumericPrimitiveKind` is 🟢 terminal because ECMA-262/TypeScript exposes exactly one numeric primitive kind per value: `number` or `bigint`; the partition is not a bool proxy, a dimensional product, or a parameterized width family, and algebraic facts land through future std numeric aliases rather than collapsing this boundary classifier. `TsEcma262PrimitiveOperationSemantics` is 🟢 terminal because resolver rows choose one ECMA primitive-semantics track among IEEE-754 `Number`, ToInt32/ToUint32 bitwise `Number`, and exact `BigInt`; this is not Rust overflow policy and not a width-indexed family. D2a(2) `GroundingMap` remains 🟡 operator-pending until the shared P2 home is pinned; no local `GroundingMap` or `ts_*_grounding` rows may be declared. Non-Bool D2a(1) alias rows remain 🟡 tracked scaffolds: `TsNumber = Float64` waits on std/float `Float64` + `ApproximateField`, `TsBigInt = Int` waits on unbounded integer/BigInt alignment, `TsString = String` waits on UTF-16/std text refinement policy, and `symbol`/`null`/`undefined` wait on the LanguageModel/nominal-runtime substrate. D2a(3) per-primitive instance rows remain deferred only on top-level nullary sum-variant `data` body validation (Class-5-Gap-3); record-structural disposition rows are safe, and D2a(2) rows are blocked only by the shared `GroundingMap` authority decision. D2b IEEE-754 `number` Arrow bodies remain deferred to the bundled T-4 grammar and std/float ApproximateField lane. |
+| `extdeps/languages/typescript.dag` | `TsEcma262NumericPrimitiveKind`, `TsEcma262PrimitiveOperationSemantics`, D2 resolver scaffolds | Green coproduct family / yellow D2 deferrals | De-prose 2026-05-18: in-file prose removed; carrier declarations are byte-identical. `TsEcma262NumericPrimitiveKind` is 🟢 terminal because ECMA-262/TypeScript exposes exactly one numeric primitive kind per value: `number` or `bigint`; the partition is not a bool proxy, a dimensional product, or a parameterized width family, and algebraic facts land through future std numeric aliases rather than collapsing this boundary classifier. `TsEcma262PrimitiveOperationSemantics` is 🟢 terminal because resolver rows choose one ECMA primitive-semantics track among IEEE-754 `Number`, ToInt32/ToUint32 bitwise `Number`, and exact `BigInt`; this is not Rust overflow policy and not a width-indexed family. D2a(2): the `{spelling}` `GroundingMap` shape is **retired** under ruled-B — there is no "shared P2 home" pending because the shape is removed, not relocated (cf. INVARIANTS §P2; the `GroundingMap`→`resolver.dag` relocation obligation is obsolete for the removed twin). A local `GroundingMap` type and `{spelling}`-style `ts_*_grounding: GroundingMap{…}` rows remain **forbidden** (the hollow form). The **ruled-B decl-ref** `ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` is a *different, sanctioned* shape (single std-authority reference, not a `GroundingMap` row) — declared this PR, **P2/E-6 staging** (consumer-gated); single-authority disposition is the **TS-D2 §** below. The Bool D2a(1) alias `TsBoolean = Bool` is **retired** (A-vs-B = B / ruled-B) — removed from `typescript.dag`, **not** in the remaining-scaffold set; single-authority disposition is the **TS-D2 §** below (machine-readable grounding *declaration* `ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` — decl-ref shared-authority, present + v2-parse-verified; **P2/E-6 STAGING**, not landed authority — no same-PR consumer, canonical fold specified-not-realized; `grounding-worked-examples.md` §0). Non-Bool D2a(1) alias rows remain 🟡 tracked scaffolds: `TsNumber = Float64` waits on std/float `Float64` + `ApproximateField`, `TsBigInt = Int` waits on unbounded integer/BigInt alignment, `TsString = String` waits on UTF-16/std text refinement policy, and `symbol`/`null`/`undefined` wait on the LanguageModel/nominal-runtime substrate. D2a(3) per-primitive instance rows remain deferred only on top-level nullary sum-variant `data` body validation (Class-5-Gap-3); record-structural disposition rows are safe; the retired D2a(2) `{spelling}`-`GroundingMap` shape is superseded by the ruled-B decl-ref grounding above (no pending `GroundingMap` authority decision — the shape is removed). D2b IEEE-754 `number` Arrow bodies remain deferred to the bundled T-4 grammar and std/float ApproximateField lane. |
 
 ### Coordination coproduct receipts
 
@@ -261,7 +261,7 @@ checked against the Practice-4 five-pattern ledger:
 | `LeanFidelityDisposition` | 🟢 GREEN terminal | All five dissolution patterns fail: modeled/normalized/fail-closed is the shared C5 disposition; non-modeled variants carry feature payloads and a flat record admits impossible combinations; not algebra; one feature has one disposition; payloads are heterogeneous. |
 | `LeanIntKind` | 🟢 GREEN terminal | Same dissolution posture as `RustIntKind` (`rust.dag`, DECISIONS.md Part 6 / CP-3229): signed vs unsigned is a closed external alternative for fixed-precision scalars, not a hideable coordinate; not algebra; not one `F<X>` family over identical payloads. |
 | `LeanIntWidth` | 🟢 GREEN terminal | Same dissolution posture as `RustIntWidth` (`rust.dag`): closed width ladder for fixed-precision scalars; `Pointer` names platform-sized facts separately from fixed bit widths; not algebra; not a `Symbol` tag. |
-| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts read from the Lean 4.20 anchor; `BoolScalar` parallels the Rust scalar bundle while kernel `LeanBool = Bool` + `lean_bool_grounding` cites std coincidence for the kernel bool spelling only (**D2-REV**). **Signed** fixed-precision surface types from the anchor (`Int8`…`Int64`, `ISize`) inhabit `IntScalar { kind: Signed, width: … }` (use the `Pointer` width arm for `ISize` per anchor); **unsigned** (`UInt8`…`UInt64`, `USize`) inhabit `IntScalar { kind: Unsigned, width: … }`. Per-name std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow); unbounded `Nat`/`Int` are deferred until explicit fact-bundles. |
+| `LeanScalar` | 🟢 GREEN terminal | Same dissolution posture as `RustScalar` `IntScalar` / `BoolScalar` (`rust.dag`): kind×width bundles fixed-precision facts read from the Lean 4.20 anchor. **A-vs-B = B (ruled-B):** the prior kernel `LeanBool = Bool` + `lean_bool_grounding` (spelling/coincidence assertion) is **retired** — a bare D2 alias asserts identity instead of demonstrating it (the hollow form the machine-readable-inhabitance bar forecloses). Lean `Bool`'s **classifier fact** is the `LeanScalar.BoolScalar` variant; the *machine-readable grounding edge* declaration `lean_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` (decl-ref, single std authority) is present + v2-parse-verified — **P2/E-6 STAGING**, not landed authority (no same-PR consumer; canonical fold specified-not-realized; `docs/modeling/grounding-worked-examples.md` §0). `lean.dag`'s per-file `GroundingMap` twin is retired with it (no spelling-only resolver rows post-D2-REV; cf. `machine_code.dag` / INVARIANTS §P2). **Signed** fixed-precision surface types from the anchor (`Int8`…`Int64`, `ISize`) inhabit `IntScalar { kind: Signed, width: … }` (use the `Pointer` width arm for `ISize` per anchor); **unsigned** (`UInt8`…`UInt64`, `USize`) inhabit `IntScalar { kind: Unsigned, width: … }`. Per-name std aliases + spelling-only `GroundingMap` rows are **omitted** (reversed-D2 hollow); unbounded `Nat`/`Int` are deferred until explicit fact-bundles. |
 
 ### `src/v4/extdeps/languages/machine_code.dag`
 
@@ -297,7 +297,7 @@ Non-Bool C++ scalar ladder in this slice: **tracked** — 🟡 `feature:t4-cpp-s
 
 | Carrier | Classification | Ledger result |
 |---------|----------------|---------------|
-| `CppBool` | 🟢 GREEN terminal | **C++ authority:** ISO C++ `bool` keyword / fundamental boolean type (`https://eel.is/c++draft/lex.key` — mirrored by `cpp.dag` `Anchor:`). `CppBool = Bool` + `cpp_bool_grounding { spelling: \"bool\" }` is the lexical spelling read for kernel-ambient `Bool` coincidence (Practice 8 / D2-REV). `rust.dag` `RustBool` is a sibling pattern only, not the C++ spec source. |
+| `CppBool` | 🟡 staging (canonical-B decl-ref declared + v2-parse-verified; P2/E-6 consumer-gated — no same-PR consumer, canonical fold specified-not-realized); non-bool C++ scalar ladder still 🟡 `feature:t4-cpp-scalar-ladder` | **A-vs-B = B (operator-ratified, ruled-B).** The prior `CppBool = Bool` + `cpp_bool_grounding { spelling: \"bool\" }` shape is **retired**: a bare D2 alias plus a `{spelling}` label asserts identity instead of demonstrating it — the hollow form the machine-readable-inhabitance bar forecloses. The machine-readable grounding edge *declaration* `cpp_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` — a decl-ref referencing the single std authority (ISO C++ [basic.fundamental]: `bool` is exactly `true`/`false`, standard ops — nothing above the primitive to model) — is present + v2-parse-verified (0 diagnostics, v2 bootstrap gate). **P2/E-6: STAGING, not landed authority** — no same-PR consumer reads it; the canonical/coincidence fold consumer is specified-not-realized (`docs/modeling/grounding-worked-examples.md` §0). This is independent of the C++ **scalar ladder** (non-bool int/float widths), which remains 🟡 `feature:t4-cpp-scalar-ladder`; when that lands, `CppScalar.BoolScalar` adds the *classifier* fact alongside this grounding. `cpp.dag`'s per-file `{spelling}` `GroundingMap` twin is retired (no spelling-only resolver rows post-D2-REV; cf. `machine_code.dag` / INVARIANTS §P2). |
 
 ## OS-1 — #3209 Coproduct Dissolution And Scaffold Record
 
@@ -899,11 +899,20 @@ rework** list above (the 5th merged D2 language file). Row established
   spec, not `std/` alias re-declarations and not a parallel
   `OrderedRing` algebra (INVARIANTS P1:42). They are terminal: nothing
   dissolves further, hence the in-file `🟢`.
-- **🟡 gated (remaining D2→fact-bundle debt).** `type TsBoolean = Bool`
-  (kernel-ambient alias bridge) plus the still-unmodeled `number` /
-  `string` / `symbol` / `null` / `undefined` primitive facts (the
-  numeric/text `std/` carriers the header marks "fact-bundle-gated").
-  These are **not yet fact-modeled**; they remain D2-shaped bridges.
+- **A-vs-B = B (ruled-B): `TsBoolean = Bool` retired.** The prior
+  `type TsBoolean = Bool` kernel-ambient alias bridge is **removed** — a
+  bare D2 alias asserts identity instead of demonstrating it (the hollow
+  form the machine-readable-inhabitance bar forecloses). TypeScript
+  `boolean`'s machine-readable grounding edge *declaration*
+  `ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra`
+  (decl-ref, single std authority) is present + v2-parse-verified —
+  **P2/E-6 STAGING**, not landed authority (no same-PR consumer;
+  canonical fold specified-not-realized;
+  `docs/modeling/grounding-worked-examples.md` §0), not the bare alias.
+  The still-unmodeled `number` / `string` / `symbol` /
+  `null` / `undefined` primitive facts (the numeric/text `std/` carriers
+  the header marks "fact-bundle-gated") remain **🟡 gated D2→fact-bundle
+  debt** — not yet fact-modeled — and are unaffected by this row.
 - **Named trigger / dissolve-on-arrival:** upstream P4 node
   `node://adhoc-71ec74f4-080` ("T-4 fact-bundle Phase-3 rework
   `extdeps/languages`", `crisp-crab-858`) is to author the remaining
@@ -1645,9 +1654,9 @@ Verbatim `//` lines from merge-base `float.dag` (lines **104–144** — modelin
 
 - **`go.dag` / `GoNever`:** `std/cardinality.dag` `Never` is landed. This slice’s `GoScalar` is the six‑variant go1.26 predeclared scalar partition; there is **no** modeled bottom primitive in that closed set, so **no** `type GoNever = Never` D2a row. A row lands only after an operator‑ratified `GoScalar` extension (or an explicit encoding that bottom is control‑flow‑only without a scalar carrier).
 
-- **`python.dag` / singletons:** `Unit` lands the shared cardinality‑1 authority for the three spec singleton kinds. Per‑singleton D2a(1)/(2) alias + grounding rows remain **deferred** on the shared `GroundingMap` home (D2 row) plus integer/text ladder work — not expanded inline in `python.dag`.
+- **`python.dag` / singletons:** `Unit` lands the shared cardinality‑1 authority for the three spec singleton kinds. Per‑singleton D2a rows remain **deferred** — but **under ruled-B the `{spelling}` `GroundingMap` home is retired**: grounding is a fold-discharged structural coincidence, never an asserted alias/spelling-map (`docs/modeling/grounding-worked-examples.md` §0). When the singleton carrier lands it grounds structurally (via `Unit` / a `PythonScalar` variant), not through a `GroundingMap` row. `python.dag`'s former `PyBool = Bool` is removed; the machine-readable grounding edge *declaration* `py_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` (decl-ref shared-authority, the truth facet) is present + v2-parse-verified — **P2/E-6 STAGING**, not landed authority (no same-PR consumer; canonical fold specified-not-realized). Python's data-model fact that `bool` is an `int` subtype is the build-up above the primitive — carried by `PythonNumericTower.BoolLevel` inside `PythonScalar.Numeric` (first iteration; §0).
 
-- **`rust.dag` / `RustNever`:** D2a(1) `type RustNever = Never` is in‑file. D2a(2) `rust_never_grounding` and **numeric** cost/width refinement (distinct from inhabitance `Never`/`Unit`) stay on the existing **GroundingMap** + **T‑25 / nat / integer** triggers already named in TASKS / SL‑3229 ledger rows.
+- **`rust.dag` / `RustNever`:** **A-vs-B = B (ruled-B).** The bare D2a(1) `type RustNever = Never` and the D2a(2) `{spelling}` `GroundingMap` shape are **retired**: identity is a claim discharged by the fold, never an asserted alias/spelling-map (the hollow form the machine-readable-inhabitance bar forecloses). Rust `!` / `bool`'s **classifier fact** is `RustScalar.NeverScalar` / `RustScalar.BoolScalar` (an honest surface enumeration). The **machine-readable grounding edge** *declarations* `rust_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra` (decl-ref, single std authority) and `type RustNever = Never` (direct primitive identity — `!` is uninhabited, nothing above the primitive) are present + v2-parse-verified — **P2/E-6 STAGING**, not landed authority (no same-PR consumer; canonical fold specified-not-realized) — `docs/modeling/grounding-worked-examples.md` §0. The per-file `GroundingMap` twin is retired from `rust.dag` (cf. `machine_code.dag` post-D2-REV; INVARIANTS §P2). Numeric cost/width refinement (distinct from inhabitance `Never`/`Unit`) stays on its existing **T‑25 / nat / integer** triggers — unchanged by this row.
 
 ### SL-3229-T4-FORMAT-T6T7 — T-4.6 format parse/emit bodies (compiler pipeline P3)
 
diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag
index 9c01a46167a..9bbb1cb1bab 100644
--- a/src/v4/extdeps/languages/cpp.dag
+++ b/src/v4/extdeps/languages/cpp.dag
@@ -1,20 +1,13 @@
 // src/v4/extdeps/languages/cpp.dag
 // Scope: C++ language primitive resolver facts.
-// Owns: CppIntegerOverflowDisposition, CppBool, GroundingMap, cpp_bool_grounding.
-// Consumes: Bool, String (explicit imports); CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows.
-// Status: D2-REV resolver slice; 🟡 feature:t4-cpp-scalar-ladder — DECISIONS.md P4-3208 + T29-ABI.
+// Owns: CppIntegerOverflowDisposition, cpp_bool_grounding.
+// Consumes: v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; CppTargetProfile/CppTargetDataModel via T29-ABI follow-up rows.
+// Status: D2-REV resolver slice; bool canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0). Non-bool C++ scalar ladder still 🟡 feature:t4-cpp-scalar-ladder — DECISIONS.md P4-3208 + T29-ABI.
 
 module v4.extdeps.languages.cpp
 
-
-import v4.std.logic { Bool }
-import v4.std.text { String }
-
-
-// Twin of `rust.dag` `GroundingMap` pending `resolver.dag` (DECISIONS.md D4; INVARIANTS P2).
-type GroundingMap<IRCarrier> {
-  spelling: String
-}
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
 
 
 // 🟢 coproduct dissolution — DECISIONS.md T29-ABI + D2-REV.
@@ -23,9 +16,6 @@ type CppIntegerOverflowDisposition
   | UnsignedModuloArithmetic
 
 
-// Anchor: https://eel.is/c++draft/lex.key
-type CppBool = Bool
-
-data cpp_bool_grounding: GroundingMap<CppBool> = {
-  spelling: "bool"
-}
+// Anchor: https://eel.is/c++draft/basic.fundamental
+// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data cpp_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
diff --git a/src/v4/extdeps/languages/go.dag b/src/v4/extdeps/languages/go.dag
index e436cd173d8..0319cefc701 100644
--- a/src/v4/extdeps/languages/go.dag
+++ b/src/v4/extdeps/languages/go.dag
@@ -1,14 +1,16 @@
 // src/v4/extdeps/languages/go.dag
 // Scope: Go language spec surface (scalar width/kind sums, channel direction, export, cost shape, partial D2 resolver); L-2 pin go1.26 via Anchor.
-// Owns: SignedIntWidth, UnsignedIntWidth, GoFloatWidth, GoComplexWidth, GoScalarKind, GoScalar, GoChannelDirection, GoExportLocus, GoExportStatus, GoChannel, GoCost, GoBuiltinIntegerArithmeticOverflow, GoIntegerOverflowDisposition, GoBool.
-// Consumes: v4.std.node.Symbol; kernel-ambient Bool, Int (STRUCTURE.md traceability).
-// Status: extdeps go slice; D2a(2) GroundingMap home + numeric D2a rows deferred per DECISIONS.md D2-REV and resolver.dag; no D1 ops in-file.
+// Owns: SignedIntWidth, UnsignedIntWidth, GoFloatWidth, GoComplexWidth, GoScalarKind, GoScalar, GoChannelDirection, GoExportLocus, GoExportStatus, GoChannel, GoCost, GoBuiltinIntegerArithmeticOverflow, GoIntegerOverflowDisposition, go_bool_grounding.
+// Consumes: v4.std.node.Symbol; v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; kernel-ambient Int (STRUCTURE.md traceability).
+// Status: extdeps go slice; bool canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0); classifier = GoScalar.BoolScalar; numeric D2a rows deferred per DECISIONS.md D2-REV and resolver.dag; no D1 ops in-file.
 // Anchor: https://go.dev/ref/spec
 // Ledger: DECISIONS.md Part 6 (PR #3229): CP-3229-GREEN-TERMINAL.
 
 module v4.extdeps.languages.go
 
 import v4.std.node { Symbol }
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
 
 // 🟢 coproduct dissolution — DECISIONS.md Part 6 · CP-3229-GREEN-TERMINAL.
 type SignedIntWidth
@@ -91,5 +93,8 @@ type GoIntegerOverflowDisposition<IRCarrier> {
   release_default: GoBuiltinIntegerArithmeticOverflow
 }
 
-type GoBool = Bool
 // 🟢 GoNever / no GoScalar bottom — DECISIONS.md §PR-3252-extdeps-deferrals (Practice 9).
+
+// Anchor: https://go.dev/ref/spec#Boolean_types
+// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data go_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
diff --git a/src/v4/extdeps/languages/lean.dag b/src/v4/extdeps/languages/lean.dag
index 527a5b0e383..22e9938f6ad 100644
--- a/src/v4/extdeps/languages/lean.dag
+++ b/src/v4/extdeps/languages/lean.dag
@@ -1,27 +1,21 @@
 // src/v4/extdeps/languages/lean.dag
 // Scope: Lean 4 language model for PROOF-1 termination export.
-// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, GroundingMap, LeanIntKind, LeanIntWidth, LeanScalar, LeanBool, lean_bool_grounding.
-// Consumes: List, Bool, String.
-// Status: D2-REV; 🟢 P4-3208 — DECISIONS.md (lean scalar + ledger).
+// Owns: LeanDeclarationKind, LeanName, LeanLevel, LeanLevelRef, LeanLevelNode, LeanBinderInfo, LeanBinder, LeanTermRef, LeanTermNode, LeanTermForm, LeanMatchAlternative, LeanTerminationMeasure, LeanTerminationBy, LeanDecreasingProof, LeanTerminationClause, LeanDefinitionTermination, LeanProofArtifact, LeanFidelityFeature, LeanFidelityDisposition, LeanProofCheckSemantics, Symbol, LeanIntKind, LeanIntWidth, LeanScalar, lean_bool_grounding.
+// Consumes: List, Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra.
+// Status: D2-REV; 🟢 P4-3208 — DECISIONS.md (lean scalar + ledger); bool canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0); classifier = LeanScalar.BoolScalar.
 
 module v4.extdeps.languages.lean
 
 
 import v4.std.collection { List }
-import v4.std.logic { Bool }
-import v4.std.text { String }
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
 
 
 // Twin of `v4.std.node.Symbol` — M1(2.7) compile_to_dag import lowering; local L-2 atom until `v4.std.node` import lowering lands (DECISIONS.md / P2).
 type Symbol
 
 
-// Twin of `rust.dag` `GroundingMap` pending shared `resolver.dag` home (DECISIONS.md D4; cpp.dag P2 note).
-type GroundingMap<IRCarrier> {
-  spelling: String
-}
-
-
 // Anchor: https://lean-lang.org/doc/reference/4.20.0/
 // 🟢 coproduct dissolution — DECISIONS.md P4-3208
 type LeanDeclarationKind
@@ -210,9 +204,6 @@ type LeanScalar
   | BoolScalar
 
 
-// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/
-type LeanBool = Bool
-
-data lean_bool_grounding: GroundingMap<LeanBool> = {
-  spelling: "Bool"
-}
+// Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Booleans/
+// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data lean_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
diff --git a/src/v4/extdeps/languages/python.dag b/src/v4/extdeps/languages/python.dag
index bfa99858ae3..864e7f087ac 100644
--- a/src/v4/extdeps/languages/python.dag
+++ b/src/v4/extdeps/languages/python.dag
@@ -1,12 +1,16 @@
 // src/v4/extdeps/languages/python.dag
 // Scope: Python 3.14 Reference surface (numeric tower, singleton kinds, scalar sum, cost shape, partial D2 resolver).
-// Owns: PythonNumericTower, PythonSingletonKind, PythonScalar, PythonCost, PyBool.
-// Consumes: Kernel-ambient Bool, Int; std/integer, std/float, std/cardinality when T-3 alias rows land (DECISIONS.md D2-REV).
+// Owns: PythonNumericTower, PythonSingletonKind, PythonScalar, PythonCost, py_bool_grounding.
+// Consumes: Kernel-ambient Int; v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; std/integer, std/float, std/cardinality when T-3 alias rows land (DECISIONS.md D2-REV).
+// Bool: canonical-B decl-ref grounding (truth facet; int-subtype build-up = PythonNumericTower.BoolLevel) — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0).
 // Status: extdeps python slice; numeric overflow and resolver deferrals per DECISIONS.md D2-REV + Part 6 (PR #3229 · CP-3229-GREEN-TERMINAL); principal int unbounded—no overflow carrier in-file.
 // Anchor: https://docs.python.org/3.14/reference/
 
 module v4.extdeps.languages.python
 
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
+
 // 🟢 coproduct dissolution — DECISIONS.md Part 6 · CP-3229-GREEN-TERMINAL.
 type PythonNumericTower
   = BoolLevel
@@ -30,5 +34,8 @@ type PythonCost {
   allocation_cost: Int
 }
 
-type PyBool = Bool
 // 🟢 Singleton / `Unit` D2a slice — DECISIONS.md §PR-3252-extdeps-deferrals + §PR-3252-cardinality-std (Practice 9).
+
+// Anchor: https://docs.python.org/3.14/library/stdtypes.html#boolean-type-bool
+// 🟡 canonical-B decl-ref (truth facet; int-subtype build-up = PythonNumericTower.BoolLevel) · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data py_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
diff --git a/src/v4/extdeps/languages/rust.dag b/src/v4/extdeps/languages/rust.dag
index 0f0cf7d1a7a..674775bee36 100644
--- a/src/v4/extdeps/languages/rust.dag
+++ b/src/v4/extdeps/languages/rust.dag
@@ -1,14 +1,16 @@
 // src/v4/extdeps/languages/rust.dag
 // Scope: Rust Reference surface (scalar/reference/visibility/cost carriers) plus ratified D2 resolver types homed here pending resolver.dag migration.
-// Owns: RustIntKind, RustIntWidth, RustFloatWidth, RustScalar, RustReferenceKind, NamedSegment, PubInPath, RustVisibility, RustReference, RustCost, GroundingMap, OverflowAction, OverflowDisposition, RustBool, RustNever, rust_bool_grounding.
-// Consumes: v4.std.node.Node, Symbol; v4.std.cardinality.Never; kernel-ambient Bool, Int, List, String.
-// Status: extdeps rust slice; PubInPath path semantics producer-obligation per DECISIONS.md Part 6 + D2-REV; D2b Arrow bodies deferred to bundled LanguageModel work.
+// Owns: RustIntKind, RustIntWidth, RustFloatWidth, RustScalar, RustReferenceKind, NamedSegment, PubInPath, RustVisibility, RustReference, RustCost, OverflowAction, OverflowDisposition, rust_bool_grounding, RustNever.
+// Consumes: v4.std.node.Node, Symbol; v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra; v4.std.cardinality.Never; kernel-ambient Int, List.
+// Status: extdeps rust slice; bool/`!` canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0). PubInPath path semantics producer-obligation per DECISIONS.md Part 6 + D2-REV; D2b Arrow bodies deferred to bundled LanguageModel work.
 // Anchor: https://doc.rust-lang.org/reference/
 // Ledger: DECISIONS.md Part 6 (PR #3229): CP-3229-GREEN-TERMINAL.
 
 module v4.extdeps.languages.rust
 
 import v4.std.node { Node, Symbol }
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
 import v4.std.cardinality { Never }
 
 // 🟢 coproduct dissolution — DECISIONS.md Part 6 · CP-3229-GREEN-TERMINAL.
@@ -69,10 +71,6 @@ type RustCost {
   allocation_cost: Int
 }
 
-type GroundingMap<IRCarrier> {
-  spelling: String
-}
-
 // 🟢 coproduct dissolution — DECISIONS.md Part 6 · CP-3229-GREEN-TERMINAL.
 type OverflowAction
   = PanicOnOverflow
@@ -83,11 +81,12 @@ type OverflowDisposition<IRCarrier>
   = MustPanicOnOverflow
   | MayPanicOrTwoComplementWrap
 
-type RustBool = Bool
-
-data rust_bool_grounding: GroundingMap<RustBool> = GroundingMap {
-  spelling: "bool"
-}
+// Anchor: https://doc.rust-lang.org/reference/types/boolean.html
+// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data rust_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra
 
-// 🟢 Rust `!` → `Never`; D2a(2) deferrals — DECISIONS.md §PR-3252-extdeps-deferrals (Practice 9).
+// Anchor: https://doc.rust-lang.org/reference/types/never.html
+// `!` is the uninhabited type: zero inhabitants, no operations — it *is*
+// the std `Never` primitive. Nothing above the primitive to model, so the
+// grounding is the direct primitive identity (the degenerate base case).
 type RustNever = Never
diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag
index d173ad53b0c..5bb8a4c5536 100644
--- a/src/v4/extdeps/languages/typescript.dag
+++ b/src/v4/extdeps/languages/typescript.dag
@@ -1,11 +1,14 @@
 // src/v4/extdeps/languages/typescript.dag
 // Scope: TypeScript 5.9 + ECMA-262 ES2025 primitive scaffold.
-// Owns: TsEcma262NumericPrimitiveKind, TsBoolean, TsEcma262PrimitiveOperationSemantics.
-// Consumes: kernel-ambient Bool; std numeric/text carriers are fact-bundle-gated.
-// Status: 🟡 gated — feature: T-4 fact-bundle Phase-3 rework after T-3/T-29/T-30/T-25-core.
+// Owns: TsEcma262NumericPrimitiveKind, TsEcma262PrimitiveOperationSemantics, ts_bool_grounding.
+// Consumes: v4.std.logic.Bool, bool_boolean_algebra; v4.std.algebra.BooleanAlgebra.
+// Status: bool canonical-B decl-ref grounding — 🟡 E-6(b) staging (scaffold at decl; ledger DECISIONS.md/§0). Non-bool numeric primitives still 🟡 gated — feature: T-4 fact-bundle Phase-3 rework after T-3/T-29/T-30/T-25-core.
 
 module v4.extdeps.languages.typescript
 
+import v4.std.logic { Bool, bool_boolean_algebra }
+import v4.std.algebra { BooleanAlgebra }
+
 
 
 
@@ -21,9 +24,6 @@ type TsEcma262NumericPrimitiveKind
 
 
 
-type TsBoolean = Bool
-
-
 
 
 
@@ -34,3 +34,8 @@ type TsEcma262PrimitiveOperationSemantics
   = TsNumberIeee754Binary64Semantics
   | TsNumberBitwiseInt32Uint32Semantics
   | TsBigIntExactUnboundedSemantics
+
+
+// Anchor: https://tc39.es/ecma262/#sec-ecmascript-language-types-boolean-type
+// 🟡 canonical-B decl-ref · E-6(b) bounded-exception · scaffold feature:canonical-b-grounding-consumer · dissolve-on: B1-CANON+zip-fold consume (ledger: DECISIONS.md B1·T-9/C1 · grounding-worked-examples.md §0)
+data ts_bool_grounding: BooleanAlgebra<Bool> = bool_boolean_algebra