[codex] Retire exact string bridge residual

docs/r3-program-plan.md

@@ -257,8 +257,8 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 31 | `bridge_source_span_file_participation_retired` | state-check | T-Bridge-Retirement | DECLARED | typed-identity-surface authority |
 | 32 | `bridge_mark_bootstrap_secret_nominal_opacity_retired` | state-check | T-Bridge-Retirement | **PASSING** | `dsl/std/types.dag` `type Secret nominal_opaque = String` + `src/v3/std/bridge_ledger.dag` row `Retired` + unit ratchet `dag.rs::bridge_mark_bootstrap_secret_nominal_opacity_retired` (bootstrap snapshots carry `Declaration.nominal_opacity` on `Secret`); historical name-keyed bootstrap bridge removed (#1272 / #937 lineage) |
 | 33 | `bridge_canonical_lens_name_dispatch_retired` | state-check | T-Bridge-Retirement | DECLARED | DeclarationRef/typed identity |
-| 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | DECLARED | substrate query surface |
-| 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | DECLARED | umbrella for exact-string scaffolds |
+| 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | PASSING | pipeline-authority source-text side channel retired; stage order reads structural `PipelineStageBinding` |
+| 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | PASSING | exact-string scaffolds retired; Bool-inhabits is source-authored and lower-helper patch remains zero-ratcheted |
 | 36 | `bridge_retirement_ledger_zero` | ledger-count | T-Bridge-Retirement | DECLARED | unified ledger reports 0 |
 | 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — PR #2181 ε path: `lens_cost_target_realization_test.rs` proves (i) **TypeRealization** slice: Rust-side `symbolic_cost_of` on a tiny program × `rust_int` row `cost` composed via `Semiring<SymbolicCost>` `sequential`; (ii) **CallableRealization** slice: bootstrap `rust_is_empty_callable` row `cost` readable as a lowered structural field (same row-shape discipline as (i), **without** a second `sequential` composition pin in that subtest). **Not** full emit-time / `LanguageSpec`-indexed cost-lens consumer (that closure remains with gates **#40** / **#70** / follow-on slices per program plan). Historical gate id; lens output stays abstract `SymbolicCost`. | ε-slice receipt; emit-time fold follow-on |
 | 38 | `coercion_cost_equals_complexity_by_construction` | structural-fold | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `Semiring<SymbolicCost>` `sequential`/`iterate` at `src/v3/std/algebra.dag:181-188` is sole composition authority — no parallel "complexity-vs-cost" reconciliation surface exists) | thesis unification holds structurally |

docs/r3-structure.md

@@ -116,8 +116,8 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
   - `bridge_source_span_file_participation_retired` — **Green predicate:** no production code path consults `SourceSpan.file` for participation/inclusion logic; participation is structural per declared facts. **Current state (R3-deferred; Director acceptance #1130 / dispatch #1139, 2026-04-29):** the gate is not satisfied; partial string-check retirement was rejected because parallel participation rules would remain. Production inclusion (distinct from diagnostics-only span use) is still keyed on path / `span.file` at: `src/v3/compiler/src/lens_apply.rs` (`behavior_source_file`, `reflect_program_dag_nodes_in_file` / `fold_lens_over_reflected_program`); `src/v3/compiler/src/lower.rs` (`lower_type_alias_refinements_phase` `dsl/std/types.dag` gate; `declaration_name_preference_rank` duplicate merge; `Dimension` + `DIMENSION_STD_AUTHORITY_FILE`); `src/v3/compiler/src/emit.rs` (`source_filtering.excludes` on declaration/bind spans). **Structural prerequisites:** module/compilation-unit identity for lens reflection; typed authority/emit-scope carriers for lower/emit; fold-shape / carrier work for remaining fold-path source-path semantics ([ROADMAP: *Lens fold execution: undeclared fallback structure + file-path semantics*](../ROADMAP.md#lens-fold-file-path-semantics)).
   - `bridge_mark_bootstrap_secret_nominal_opacity_retired` — name-keyed bootstrap bridge from #937 deleted; nominal-opacity authority lives in source-level declaration (PR A landed in R2)
   - `bridge_canonical_lens_name_dispatch_retired` — lens dispatch routes via `DeclarationRef`/typed identity, not canonical name strings
-  - `bridge_include_str_side_channels_retired` — no `include_str!` macro reads source-substrate identity; substrate query surface used instead. **Open disposition (`pipeline_authority`, PR #1171, 2026-04-29):** `compile` remains `ArrowBody::Unparsed`, so compile-body stage order is not yet a structural Dag fact; runtime ordering reads `PipelineStageBinding` only — full gate for this site awaits derivation / lowered compile witness, not file IO.
-  - `bridge_exact_string_patching_residual_retired` — umbrella row for exact-string patching scaffolds. **PB lower-helper slice (Tier-2 / #1014 lineage) is pinned at zero** in v3-compiler Rust: no `patch_lower_helpers*` code paths remain, and `bridge_lower_helpers_patch_zero_residual_test` ratchets reintroduction. **Other** exact-string patching classes (outside this retired lower-helper post-process bridge) remain **out of scope for this receipt** and keep their own dissolution triggers.
+  - `bridge_include_str_side_channels_retired` — pipeline-authority source-text side channel retired. Stage order reads structural `PipelineStageBinding`, and the integration ratchet forbids reintroducing a compiler-crate `include_str!` of `pipeline.dag`; `compile` still lowers as `ArrowBody::Unparsed`, so this retirement means no source-text side channel remains for the authority path, not that compile-body drift is structurally checkable.
+  - `bridge_exact_string_patching_residual_retired` — exact-string patching scaffolds retired. **PB lower-helper slice (Tier-2 / #1014 lineage) is pinned at zero** in v3-compiler Rust: no `patch_lower_helpers*` code paths remain, and `bridge_lower_helpers_patch_zero_residual_test` ratchets reintroduction. The BR-19 Bool-inhabits post-parse patch is retired by authoring `Bool inhabits BooleanAlgebra<Bool>` directly in `dsl/std/types.dag`; bootstrap no longer mutates `Declaration.inhabits` for kernel `Bool`.
   - `bridge_retirement_ledger_zero` — unified ledger reports 0 named identity bridges remaining
 - **T-V2-Retirement** (NEW 2026-04-30; pulled into R3 per user directive *"nothing can be deferred past R3"*).
   - `v2_oracle_no_remaining_test_consumers` — no `.rs` test file under the workspace consumes anything from `src/v2/`; v2-oracle and v2-using test scaffolds retired

dsl/std/types.dag

@@ -164,13 +164,9 @@ fn canonical_container_names() -> List<String> {
 // require v3 to resolve aliases in Branch input type-checking
 // (currently pins Bool as a direct Disj for if/else). Deferred until
 // that compiler work lands; keeps intent-signaling via distinct names.
-// v3 Path A (Lane 1e-2b): `Bool` still parses here for v2 (`dsl/` is v2-scanned;
-// see `v2-compiler-tests` `gist_transitive_closure_parse` and stage0 self-host
-// fixtures). `Declaration.inhabits` → `BooleanAlgebra<Bool>` is applied in v3
-// bootstrap after std fixtures lower (`bootstrap::patch_kernel_bool_boolean_algebra_inhabits`).
-// Surface `type … inhabits … =` is v3-only under `src/v3/compiler/` (generated
-// parser) and cannot appear in this file until v2 gains a compatible parse path.
-type Bool = True | False
+// v3 Path A (Lane 1e-2b): the `Bool` -> `BooleanAlgebra<Bool>` relation is
+// authored here, not patched after parse.
+type Bool inhabits BooleanAlgebra<Bool> = True | False
 
 // Unit: terminal object (zero-field product, single inhabitant).
 type Unit