docs/plans: inert-layer lens — observe modeled-but-unreached layers (+ live census)

ROADMAP.md

@@ -29,7 +29,7 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l
 
 - [x] **numeric-tower grounding** (#5428) — `Int=GroupCompletion<Nat>`; `==` straddle guard now dead-in-corpus ([plan](docs/plans/model-realization-fork.md))
 - [ ] **cache trustworthy** — authoritative home is §2 F2/F3/P1; ship the warm==cold oracle as a detective now
-- [ ] **rust-gate coverage** (shared §1) — opt-level=3 restores Pop-A to per-PR (#5456); run-all-unless-`#[ignore]`d (#5427) ([cause table](docs/plans/expensive-test-cause-table.md))
+- [ ] **rust-gate coverage** (shared §1) — opt-level=3 restores Pop-A to per-PR (#5456); run-all-unless-`#[ignore]`d (#5427) ([cause table](docs/plans/ci-selection-vs-scheduling.md))
 - [ ] **promote-or-delete every inert lens** + de-vacuum thin gates *(silent-wren-739)*
 - [x] **realization-vocabulary containment guard** (#5445/#5453) — target-AST importable only at the realization edge (fail-closed, shrinking-roster); dissolve-on: bash-sidecar arc empties the roster → pure wall → `program.dag` deletable ([plan](docs/plans/emission-ingestion-inverse.md))
 - [ ] **stage0 clone-census inert + seed regressed** to 21540 (~1138 over) — resolve by clone-reduction / substrate-migration, NEVER a cap-bump; #5427 `#[ignore]` is the interim *(fierce-hawk-540 via quick-ant-298)*
@@ -45,6 +45,7 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l
 **Meta — lock down the reasoning (§7 recursion):**
 
 - [x] **inert-lens hygiene backstop** — every `lens/*.dag` wired or deleted; runs over the corpus (#5433)
+- [ ] **reachability-completeness lens** — every declared node (code carrier · doc · lens) reachable from a run-root, rostered, or deleted; generalizes #5433 to carriers + docs ([plan](docs/plans/inert-layer-lens.md))
 - [ ] **gate-hygiene: a floor-enrolled gate must be green-on-main at merge** — roster-completeness assertion promoted to should-land ([plan](docs/plans/emission-ingestion-inverse.md) §2) *(quick-ant-298)*
 - [ ] **construction-justification rule** (authoring-time) — justify why a class can't be construction before adding a lens ([DESIGN §6](DESIGN.md)) *(silent-wren-739)*
 - [ ] **expressibility frontier** — partition each modeling discipline into wall / lens-residue / undecidable-review *before* gating ([plan](docs/plans/expressibility-frontier.md))

docs/plans/inert-layer-lens.md

@@ -0,0 +1,216 @@
+# The inert-layer lens — modeled but unreached
+
+> A lens that reports declared concepts (carriers, fns, whole modules) that are **modeled but unreached
+> from any live run-root** — DESIGN §6's "the machinery exists but nothing gates on it," made
+> *observable* and eventually fail-closed. The dangerous subset, and the reason for the lens, is the
+> **load-bearing-but-unwired** layer: a richly-structured carrier that *looks* like it drives behavior
+> and drives none. DESIGN refs: §3 (single authority — generalizes the #5433 inert-lens backstop, does
+> not fork it), §5 (fail-closed; construction over validation), §6 (lens as residue; coverage-by-illusion),
+> §7 (recursion — the compiler's own dead model is a substrate fact).
+
+## 1. The definition (why reference-count is not enough)
+
+A declared concept is **inert** iff it is **not reachable from a live run-root** over the reference
+graph. The subtlety that makes this a real lens and not a grep:
+
+- **Reference-count overstates liveness.** A carrier with N>0 consumers can still be inert if all N
+  consumers are themselves inert — a self-referencing cluster. Measured example: `RealizationObjective`
+  and `ComputeOffer` each have 4 consumer files, but `RealizationObjective` is **live** (`ci_floor_plan`,
+  a run-root, imports `realization_width`→it) while the work-demand cluster around `ComputeOffer` reaches
+  nothing that runs. Same count, opposite verdict. **Reachability, not count.**
+- **Run-roots ≠ test-roots.** The existing #5433 backstop seeds reachability from *discovered test
+  witnesses* — it answers "is this lens **covered**?". Inert-layer detection must seed from the *run*
+  roots — what actually executes in production: the CI floor plan, the compiler pipeline driver, the emit
+  entry. A module reached only by tests but by nothing that runs is *inert in production yet covered* — a
+  distinct, also-interesting state. The lens reports both, labeled.
+
+So: **inert = declared ∧ ¬reachable(run-roots)**. Decidable (graph reachability), a pure Node read.
+
+### 1.1 The rules — what is a hard wall, and what only looks like one
+
+Four cases decide whether this is a *rule* or a *vibe*. Each lands in a different frontier region
+([expressibility-frontier](expressibility-frontier.md)); the design discipline is to keep them apart.
+
+- **Does a test consumer count? — NO, for the *live* verdict; it is a separate, labeled state.** Run
+  reachability from each root set independently: run-roots (executed entries) → "inert in production?";
+  test-roots (witnesses) → "covered?". A concept reachable from tests but not from run-roots is
+  **"tested but unrun"** — its own bucket (a test can pin dead code alive). Report it; **wall only on
+  run-root-inert.** Decidable per root set → ①.
+
+- **One consumer, but that consumer is dead? — you never count local consumers.** The verdict is
+  *membership in the complement of the reachable set*, a fixpoint from the roots over the whole tree. A
+  node alive only through a dead consumer is simply not in the reachable set → inert. "Inspect the entire
+  tree" is exactly right: global reachability, not per-node degree. This is the case reference-count gets
+  wrong (§1). Decidable → ①.
+
+- **Dead arms / fields (one honest reading of "should be 10, has 1") — decidable, a sharper wall.** A
+  reachable carrier can still have *arms never constructed* or *fields never read*. Arm-level
+  reachability is decidable (an arm appears in some reached construction or it doesn't), and the *match*
+  side is already CoproductExhaustiveness (§4 testgen). So "a 6-arm coproduct where 3 arms are never
+  built" is a wall, not a guess → ①.
+
+- **One consumer, but it *should* be ten call-sites? — this is NOT inertness, and forcing it into this
+  rule breaks the wall.** "Should be ten" needs the set of sites that *ought* to consume the concept —
+  not derivable from the concept alone (③ undecidable directly, by Rice). But its **dual is decidable**:
+  the sites that should have consumed an authority and didn't are the ones that *rolled their own
+  equivalent* — a §3 nickname / §2 anemic pattern. So under-consumption is detected **as redundancy**, by
+  the anemic / nicknaming lens, *not* by counting expected consumers.
+
+**The framing rule: inertness (0 reachable) is a wall; under-wiring (too few) is a hand-rolled fork —
+keep them separate.** Fusing them is the trap: you would try to make "should be N" a hard gate, fail by
+Rice, and either fire falsely or abandon the whole rule.
+
+So the hard rule is exactly the **0-reachability** one, and it is a wall on three conditions:
+1. **the run-root set is enumerable** — it is (the floor plan, the compiler/emit drivers, the CLI bins:
+   things with a `main` or a discovered entry). A fuzzy root set is a fuzzy wall — pin it.
+2. **reflective / host-bridge consumption counts as an edge** — `concept_index` is host-fed and the floor
+   discovers witnesses by marker scan, not import; a carrier consumed only through such a bridge is
+   *live* and would false-positive a pure import walk. The roots must include the bridge entry points.
+3. **a named, shrinking exception roster** for carriers deliberately modeled ahead of their consumer (the
+   realization loop is model-first by design) — each entry names its dissolve-on PR; the roster empties
+   as the loop wires them, and the lens flips advisory → wall when it does (the #5433 / realization-vocab
+   shape).
+
+The rule, stated once:
+
+> A declared concept must be **reachable from a live run-root** (over static **and** reflective edges),
+> be on the **exception roster** with a dissolve-on, or be **deleted**. Test-only reachability is a
+> separate "unrun" bucket — reported, not gated. **Under-consumption is out of scope** — it is the
+> redundancy lens, not this one.
+
+## 2. The census (the discriminating witnesses the lens must reproduce)
+
+Measured 2026-06-21 over `dsl/**` + `src/v2/**`, reachability cross-checked against run-roots
+(`ci_floor_plan`, `scheduler`, the v1 run path). This is what the lens must independently re-derive:
+
+**Fully inert (0 live consumers), load-bearing — the target class:**
+
+| carrier | home | what it models |
+| --- | --- | --- |
+| `CacheLayerPlan` | `cache_interface.dag` | the L1/L2/L3 cache-layer plan — the whole §2 cache-planner output |
+| `WorkDemand` | `compute_fabric.dag` | the work-demand vocabulary (isolation/memory/GPU) — nothing emits one |
+| `ParallelismShape` · `IndependentShards` · `PartitionedReduce` | `compute_fabric.dag` | the corpus-sharding demand model |
+| `Partitioner` · `SymbolicCost` (forward-stubs `= Node`) | `compute_fabric.dag` | map→reduce execution decomposition |
+| `execution_receipt_digest` | `compute_fabric.dag` | the digest the 3-dimension unification rests on — a stub returning `work.id`, consumed nowhere |
+
+**Edge-wired (consumed by a model that is not itself the live source yet):**
+
+| carrier | consumed by | why still inert-at-the-edge |
+| --- | --- | --- |
+| `ComputeOffer` / the fleet model | `ci_fleet`, `operator_fleet`, `runner_spec_from_offer` | projected to a `RunnerSpec`, but `ci.yml`'s runner block is still a literal — the projection isn't the live emission source (Phase 3 open) |
+
+**Now-wired (recorded so the lens does *not* false-positive these):**
+
+| carrier | reached via |
+| --- | --- |
+| `RealizationObjective` · `realization_width` · `HardwareThreadCount` (11) · `AxisGoal` | `ci_floor_plan` → `realization_width.width_fold_objective_goals` / `memory_aware_spawn_width` — the memory-aware width landed; the *schedule/width* arm of realization is live |
+
+The reading: the **schedule/width** arm of the realization layer is now wired; the **cache-plan** arm and
+the **work-demand / sharding / receipt-digest** arm are the inert load-bearing layers. Exactly the
+realization-loop thesis ("shape-complete but input-starved"), now with names.
+
+## 3. Two tiers (what's buildable now vs gated)
+
+**Tier 1 — module-level, buildable now (reuse #5433).** `inert_lens_modules` (`cli_run.rs:2558`) already
+computes module-import transitive closure from seed roots and reports unreached `v2.lens.*` modules. The
+inert-*layer* lens is the **same machinery with two generalizations**: (a) widen the output filter from
+`is_top_level_lens_module` to *all* modules; (b) seed from the **run-roots** (floor plan + pipeline +
+emit), not only discovered witnesses. Output: unreached *files/layers*. Reuses the existing BFS over
+`module_to_path` + `path_imports`; no new host machinery.
+
+**Tier 2 — symbol-level, gated.** Within reached modules, which declared carriers/fns have zero live
+consumers (the §2 census above is symbol-level). This needs **whole-corpus reference (`BindsTo`)
+enumeration**, which does *not* exist today — `dependency_lens` is per-declaration, `concept_index`
+enumerates *declarations* but not *reference sites*. So Tier 2 is host-fed today (a
+`enumerate_all_binds_to_edges()` bridge beside `concept_decl_facts_live()`) and becomes a pure `.dag`
+walk on the **same dissolution trigger as `concept_index`** (gunbc#5364 — v2 self-host gains
+compile-graph access). Until then Tier 2 is host-fed, Tier 1 is pure.
+
+## 4. The load-bearing ranking (the advisory half)
+
+"Inert" is decidable; **"load-bearing" is a heuristic** — so the lens *decides* inertness and *ranks*
+apparent load-bearingness, never gates on the ranking. Rank an inert concept by structural richness:
+coproduct arm-count + record field-count + fn return-type richness, plus name signals
+(`Plan`/`Account`/`Receipt`/`Schedule`/`Demand`/`Policy`). A 6-arm `ParallelismShape` with 0 consumers
+ranks far above an unused 1-line helper. This is the operator's exact ask — "ones that *seem* load-bearing
+but are unwired" — surfaced as the ranked head of the inert list.
+
+## 5. Frontier placement (per [expressibility-frontier](expressibility-frontier.md))
+
+- **Inertness is a ① wall candidate.** Reachability is decidable; an inert load-bearing carrier should
+  eventually **fail closed** exactly as #5433 does for lenses ("an inert lens is a lie" → "an inert
+  load-bearing carrier is a lie"). The honest path: ship as a ② *observing* lens first (a ranked report,
+  no gate), promote to a ① wall once the corpus is clean enough that a new inert load-bearing carrier is
+  a genuine defect rather than expected staged-ahead modeling.
+- **The "staged-ahead" exception is the catch.** Much of the inert set is *deliberately* modeled before
+  its consumer (the realization loop is built model-first by design). So a blanket wall would fight the
+  project's own just-in-time-after-modeling discipline. The resolution is the #5433 pattern: a
+  **named, shrinking exception roster** (carriers modeled ahead of a tracked consumer-PR) that empties as
+  the realization loop wires them — the same ratchet-during-migration → wall-when-empty shape as the
+  realization-vocabulary guard. Each roster entry names its dissolve-on (the PR that wires it).
+- **The ranking is the ② residue**, permanently advisory (judging "load-bearing" needs domain knowledge).
+
+## 6. Reuse map (do not fork — §3)
+
+| need | reuse | file |
+| --- | --- | --- |
+| transitive reachability BFS | `inert_lens_modules` | `cli_run.rs:2558-2606` |
+| enumerate all declared concepts | `concept_index.enumerate_concepts()` | `concept_index.dag:130` |
+| use vs structural edge classification | `unused_parameters` `UseRelation` (`BindsTo` = the use authority) | `unused_parameters.dag:22` |
+| import/reference edge-walk | `layering_imports` projection | `layering_imports.dag` + `layering_imports_project.rs` |
+| run-roots | floor gates + corpus + pipeline/emit entries | `ci_floor_plan.dag:83`, `cli_run.rs:run_discovery_corpus` |
+
+## 7. Wiring + dissolution
+
+- Tier 1 lands as `v2.lens.inert_layer` + a floor witness; runs over the corpus, **reports** (advisory)
+  first, ranked, with the exception roster.
+- Promote to fail-closed once the roster is small and stable (per §5 above).
+- **Load-bearing seed caveat:** Tier 1 touches `cli_run.rs` (the #5433 closure) — a DESIGN-named
+  load-bearing file → **escalate before editing**; prefer extending `inert_lens_modules` behind a flag to
+  forking it.
+- **Dissolution:** the lens itself never dissolves (inertness is a standing property); its *exception
+  roster* dissolves to empty as the realization loop wires each carrier, at which point the lens flips
+  from advisory ② to fail-closed ① wall.
+
+## 8. Generalization — one rule, N substrates (code · docs · lenses)
+
+Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every
+breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or
+deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph —
+and the doc instance is the **cheapest wall of all** (pure link reachability, no reflective edges, no
+host bridges):
+
+| substrate | nodes | edges | roots | inert = | dangling = |
+| --- | --- | --- | --- | --- | --- |
+| code | declared concepts | reference / `BindsTo` | run entries | unreachable carrier | — |
+| **docs** | `docs/**/*.md` | markdown links (+ `.dag`-comment `bind:` refs) | `ROADMAP.md`, `DESIGN.md`, runbook index | **orphan plan doc** | **broken `](path)` link** |
+| lenses | `v2.lens.*` | module imports | discovered witnesses | inert lens (#5433) | — |
+
+The same three conditions (§1.1) decide the doc wall:
+1. **enumerable roots** — `ROADMAP.md` + `DESIGN.md` for *plan* docs; **runbooks need their own root** (an
+   operational index), or they false-positive (a runbook is not a roadmap item). Pin the root per doc
+   *kind*.
+2. **reflective edges count** — a doc referenced only from a `.dag` comment (`bind: docs/...`, the
+   CLAUDE.md open thread) is *consumed* but invisible to a markdown-link walk; include those refs.
+3. **exception roster** — best expressed as a **PR-local rule**: a PR that adds `docs/plans/X.md` must add
+   its inbound link in the same PR. That is the doc-graph analog of "an inert lens is a lie" — and this PR
+   honors it (it adds this doc *and* its ROADMAP line).
+
+**Live census (2026-06-21) — the doc instance's discriminating witnesses:** 18 docs, 13 reachable,
+**5 orphans** — `compile-clean-forcecheck.md`, `inert-layer-lens.md` (this very doc, before its ROADMAP
+line landed — the self-demonstrating case), `m4-universal-hermetic-corpus.md`,
+`m5-fixture-store-consolidation.md`, `runbooks/bmc-redfish-operator-access.md` (likely a legitimate
+runbook-root case, not a roadmap orphan) — and **1 dangling link**: `ROADMAP.md`'s rust-gate-coverage
+bullet linked `docs/plans/expensive-test-cause-table.md`, a #5463 forward-reference never written (the
+Pop-A/Pop-B content already lives in `ci-selection-vs-scheduling.md`, so a new doc would §2/§3-duplicate
+it). **Repointed in this PR** to the doc that holds the content. The wall would have blocked all six.
+(Methodology note: the *first* census run reported this ref as 2× — it had read a stale local `ROADMAP`
+behind main's terse pass; the lens must run against the live tree, the same discipline it enforces.)
+
+## 9. Open
+
+- Confirm the run-root set (is `scheduler.dag` the sole runtime, or also the v1 `claim_executor` path?
+  the digest census touched both).
+- Decide Tier-1-now vs wait for Tier-2's host bridge so the first landing is symbol-granular (the census
+  shows the interesting cases are symbol-level — `execution_receipt_digest`, `CacheLayerPlan` — so a
+  module-only first cut may under-deliver; weigh against Tier 1's zero-new-machinery cost).