C0(b1) follow-up: correct the ValueIdentity citation and narrow the b1/b2 scope claims

dag/gunbc/plans/v2_complexity_capability_parity.dag

@@ -125,7 +125,7 @@ fn v2_complexity_capability_parity_body() -> List<MarkdownBlock> {
     h2(text: "6. What must NOT be carried across"),
     p(text: "v1's identities are string-keyed in five places, verified: `SizeVar { name: String }`, `SizeLen { collection: String }`, `CostExtern { name: String }`, `CostUnknown { reason: String }`, and `CostInternTable { summaries: Map<String, ComplexitySummary> }`. Every one is the anemic-modeling class DESIGN §2 names — a `String` leaf standing where a grounded identity exists. The migration re-grounds each:"),
     ul(items: [
-      li(text: "function and collection identity → `DeclarationRef` / `ValueIdentity` (the G1 cited-symbol resolution work already makes these resolvable)"),
+      li(text: "function and collection identity → `DeclarationRef`, which exists today and resolves through `v2.std.decl_ref_resolution`. **`ValueIdentity` does NOT exist in the tree** — corrected 2026-08-05, after this line misled the C1 lane. It appears only inside the sibling note's *proposed* `CostSubject` and `CostJustification` code blocks; a corpus grep resolves it to no declaration of any kind. The original wording said the G1 cited-symbol work 'already makes these resolvable', which is true of `DeclarationRef` and false of `ValueIdentity` — the DESIGN §3 cited-symbol class, a name-level claim a grep decides, sitting false in an authority doc while the mechanism it describes stayed correct. C1 must therefore either ground size identity on the existing `SizeVariable` carrier or land a value-identity authority first; it may not cite a symbol that does not exist."),
       li(text: "`CostExtern { name }` → `CostEffect { operation: DeclarationRef }`, joining the sibling note's `ExecuteEffect` atom rather than a second extern channel"),
       li(text: "`CostUnknown { reason: String }` → a typed, located, **countable** cause — a free-text reason cannot be tallied, so its frequency never ranks the deficit for fixing (DESIGN §5)"),
       li(text: "`Certainty = Proven | Conservative` → reconciled with the existing `DescentEvidence` and `Measured` bases rather than minted as a third confidence vocabulary"),

dag/gunbc/v1_complexity_capability_census.dag

@@ -7,7 +7,7 @@ import std.decl_ref { DeclarationRef, DeclField, WholeDeclaration, decl_ref }
 
 data v1_complexity_capability_census_note: String = "C0(b1) of the v2 complexity capability parity program: a REVIEWED capability roster over src/v1/complexity.dag, with every citation carried as a typed DeclarationRef that resolves through the single resolution authority rather than as a name matched by substring. It is deliberately NOT the closed capability denominator — that is C0(b2), the declaration-to-capability totality slice, which derives the population from DeclFact instead of authoring it. This module states the difference rather than blurring it (operator review, 2026-08-05): what is proven here is that the authored rows are well-formed, exactly cited, and disposition-partitioned; what is NOT proven here is that no capability is missing."
 
-data c0_scope_note: String = "Scope, stated so the title cannot overclaim. PROVEN by this carrier and its witnesses: every row carries a typed DeclarationRef; every ref resolves to exactly one declaration through v2.std.decl_ref_resolution (long lane, which pays the decl_facts scan); capability identity is a closed coproduct, so an identity OUTSIDE the vocabulary is unrepresentable — but the roster is a List, so the same identity CAN appear twice and distinctness is VALIDATED by an executing witness, not constructed (claim narrowed on operator review 2026-08-05: the earlier 'duplicates are unrepresentable' was too strong). C0(b2)'s derived declaration population supplies the construction wall this list cannot; every disposition arm lands in exactly one work-state partition, with a controlled fixture for every arm including the uninhabited ones. NOT PROVEN: declaration-grain completeness. A 27th capability omitted from the roster would not be detected here, and no assertion in this lane should be read as claiming otherwise."
+data c0_scope_note: String = "Scope, stated so the title cannot overclaim. PROVEN by this carrier and its witnesses: every row carries a typed DeclarationRef; every ref resolves to exactly one declaration through v2.std.decl_ref_resolution (long lane, which pays the decl_facts scan); capability identity is a closed coproduct, so an identity OUTSIDE the vocabulary is unrepresentable — but the roster is a List, so the same identity CAN appear twice and distinctness is VALIDATED by an executing witness, not constructed (claim narrowed on operator review 2026-08-05: the earlier 'duplicates are unrepresentable' was too strong). C0(b2)'s derived declaration population supplies the construction wall this list cannot FOR DISTINCTNESS AND FOR DECLARATION COVERAGE, though not for capability discovery; every disposition arm lands in exactly one work-state partition, with a controlled fixture for every arm including the uninhabited ones. NOT PROVEN: declaration-grain completeness. A 26th semantic capability omitted from this roster would not be detected here — AND, corrected 2026-08-05 against the b2 author own report, it is NOT detected by C0(b2) either. b2 derives the DECLARATION population from DeclFact and classifies each declaration against this closed ComplexityCapabilityId vocabulary; a capability absent from the vocabulary therefore has no row to fail against and no declaration classifies to it. The earlier wording said such a capability would not be detected HERE, which implied b2 was its trigger. It is not. What would actually close it is capability discovery FROM THE SURFACE — deriving the capability set from what v1.compiler.complexity does rather than checking an authored set against declarations — and no slice of this program currently owns that. Naming it as an untriggered stall is the point (DESIGN §4b meta-obligation 2: separate cannot-climb from can-climb-after-one-grounding from can-climb-now-but-unbuilt; this one is the third, and it had a wrong trigger attached)."
 
 data v1_declaration_counting_method_note: String = "Method identity for the declaration count, which two notes reported differently (operator review, 2026-08-05). Over src/v1/complexity.dag at this revision: 171 counts top-level `fn` declarations only; 201 counts `fn` + `type` + `data` + `let`; 26 are `type` and 4 are `data`. Both figures are correct under their own method and neither was wrong — what was missing is the method, without which the two numbers read as a contradiction. This note is the method authority; a figure quoted without one is not quotable. C0(b2) derives its denominator from DeclFact rather than from either grep, at which point this note is superseded by the derived population."
 
@@ -90,7 +90,7 @@ type ComplexityCapabilityId
   | SizeVariableLegend
   | CostAccountSpaceBridge
 
-data complexity_capability_id_note: String = "Capability identity as a closed coproduct rather than a string key. What this buys is exact: an identity OUTSIDE the vocabulary is unrepresentable, and cross-capability edges get a checkable target rather than prose — RetirementOwed names the capability that supersedes it as a variant, not a spelling. What it does NOT buy is distinctness: a List can carry the same variant twice, so inventory_identity_keys_distinct VALIDATES that and says so (operator review 2026-08-05 corrected the earlier overclaim).  C0(b2) will join this set against the derived declaration population; until then, the set is authored and its completeness is explicitly unproven."
+data complexity_capability_id_note: String = "Capability identity as a closed coproduct rather than a string key. What this buys is exact: an identity OUTSIDE the vocabulary is unrepresentable, and cross-capability edges get a checkable target rather than prose — RetirementOwed names the capability that supersedes it as a variant, not a spelling. What it does NOT buy is distinctness: a List can carry the same variant twice, so inventory_identity_keys_distinct VALIDATES that and says so (operator review 2026-08-05 corrected the earlier overclaim).  C0(b2) joins this set against the derived declaration population — which proves every capability here HAS an authority declaration, and does NOT prove that every capability v1.compiler.complexity implements HAS a row. Those are different claims and only the first is b2 scope. The set remains authored, and its completeness over the surface is unproven by b1 and by b2 alike."
 
 type V1ComplexityResidueId
   = SummaryEvictionHazard

dag/test/claim/v1_complexity_capability_census_witness_test.dag

@@ -70,7 +70,7 @@ import gunbc.v1_complexity_capability_census {
 
 data witness_note: String = "FAST-LANE structural hygiene for the C0(b1) v1 complexity INVENTORY. Exact DeclarationRef resolution against live decl_facts is deliberately NOT here — it costs a full witness-layer decl_facts scan and would breach the 5s fast-lane budget, the same reason test.claim.cited_symbol_resolution_witness_test keeps its resolution census in the long lane. That census is this roster's companion in test.claim.long.v1_complexity_capability_census_resolution_test. What this file proves is what is cheap and structural: every arm lands in exactly one work-state, EVERY arm has a controlled fixture including the ones no row inhabits, and routing metadata is drawn from typed vocabularies. The vacuity control moved to the long-lane companion with the lens imports it needed — see closure_cost_note."
 
-data closure_cost_note: String = "COST FINDING, measured on this PR (2026-08-05), stated with its clock basis. An earlier revision of this file imported v2.lens.complexity, v2.lens.cost and v2.std.refinement to execute the vacuity control. No other witness under dag/test/claim imports them, so this file was the FIRST to drag the v2 lens closure into the per-PR witness layer — and the floor measured the consequence on an unrelated witness: roadmap_program_view_witness_test witness_live_constraint_present_iff_line_unaccepted recorded 3901.9ms on green main and 5019ms here, without its own semantic work changing. BASIS, per gunbc.witness_row_cost witness_row_cost_clock_basis_note (landed on main 2026-08-05, gunbc#7820): both figures are WALL and the fast-lane cap is enforced on thread CPU. The 3901.9ms baseline is therefore a real reading — eval is single-threaded, so a wall figure under the cap proves cpu under it. The 5019ms figure is NOT a cost: it is a CENSORED measurement whose value is where the kill landed, so the true figure is unbounded above. The honest claim is consequently weaker in one direction and stronger in the other: the regression is at least 1117ms and its actual size is unknown, and what is decided is only that the row crossed. Recorded rather than silently fixed because it is a measured instance of this program's own subject twice over — a per-witness cost invisible until it lands on somebody else's budget, and a threshold that reports the victim rather than the cause on a clock other than the one it enforces. The lens imports moved to the long-lane companion with the control that needed them."
+data closure_cost_note: String = "COST FINDING, measured on this PR (2026-08-05), stated with its clock basis. An earlier revision of this file imported v2.lens.complexity, v2.lens.cost and v2.std.refinement to execute the vacuity control. No other witness under dag/test/claim imports them, so this file was the FIRST to drag the v2 lens closure into the per-PR witness layer — and the floor measured the consequence on an unrelated witness: roadmap_program_view_witness_test witness_live_constraint_present_iff_line_unaccepted recorded 3901.9ms on green main and 5019ms here, without its own semantic work changing. BASIS, per gunbc.witness_row_cost witness_row_cost_clock_basis_note (landed on main 2026-08-05, gunbc#7820): both figures are WALL and the fast-lane cap is enforced on thread CPU. The 3901.9ms baseline is therefore a real reading — eval is single-threaded, so a wall figure under the cap proves cpu under it. The 5019ms figure is NOT a cost: it is a CENSORED measurement whose value is where the kill landed, so the true figure is unbounded above. MEASURED AFTERWARD, which supersedes the weaker claim this note first carried. Three readings per side, all wall: main 3728.8 / 3901.9 / 3964.4 (mean 3865.0, spread 235.6) and this branch 4106.4 / 4179.0 / 4191.9 (mean 4159.1, spread 85.5). The ranges are DISJOINT with a 142.0ms gap between main slowest and this branch fastest, and main spread is the WIDER of the two — so the roughly 294ms increase is a real cost this change imposes, not host noise, and the earlier its-size-is-unknown wording is retired rather than left standing. The likely cause is not mysterious and is worth naming: this change adds content to the two design-note carriers that the roadmap program view projects, so the witness folding over that view genuinely does more work. It remains about 800ms under the cap. What is still NOT established is the censored 5019ms figure, which stays a lower bound by construction: a killed run reports where the kill landed, never what it would have cost. RECONCILED ON MERGE WITH MAIN: gunbc#7762 independently moved this same witness OUT of the per-PR fast lane into falsifier_substrate_long_lane_rows, on the ground that it flaked at 5004ms under host contention and was declared not caused by that PR diff. Both readings can hold and this branch does not contest that row: a witness can be contention-sensitive AND diff-sensitive, and the measurement above is evidence for its borderline status rather than against it — but it does refute the general form of the attribution, because here a diff moved it about 294ms with disjoint ranges. The practical consequence is that this branch cost no longer lands on anyone per-PR budget, since the witness now runs on the long lane. The cost finding is retained rather than deleted because the mechanism it records — a witness import closure landing on an unrelated witness budget — is unchanged by where the victim happens to run. SUBJECT DECOMPOSED AFTER MEASUREMENT (gunbc#7822, merged 2026-08-05, after every reading above was taken): roadmap_program_view_witness_test witness_live_constraint_present_iff_line_unaccepted NO LONGER EXISTS. The index-backed projection work decomposed it, and its long-lane row is replaced by roadmap_program_view_live_corpus_receipt_test live_roadmap_program_view_corpus_projection_receipt. Every figure above is therefore a historical measurement of a function that is gone, and the name is retained ONLY because it identifies what was measured — it is not a live citation and must not be treated as one. This is worth writing down rather than quietly deleting, because it is this census own subject happening to this census: a symbol cited in prose stopped resolving without anyone touching the sentence that cited it. The mechanism the finding records is unaffected, since it concerns import closures landing on a neighbour budget, not that particular neighbour. Recorded rather than silently fixed because it is a measured instance of this program's own subject twice over — a per-witness cost invisible until it lands on somebody else's budget, and a threshold that reports the victim rather than the cause on a clock other than the one it enforces. The lens imports moved to the long-lane companion with the control that needed them."
 
 
 data green_by_vacancy_note: String = "The operator finding this file exists to answer. The previous revision's exhaustiveness check was green only because no row inhabited the DeliberatelyRetired arm — a check that would have failed the first time that declared arm was used. Fixtures below inhabit ALL SIX arms independently of the roster, so the partition is proven total over the type rather than over today's row set. Retired and SupersededByBetterModel have no roster row at all; they are proven here and nowhere else."

docs/plans/v2-complexity-capability-parity.md

@@ -97,7 +97,7 @@ v1.compiler.complexity    legacy realization, capability inventory,
 
 v1's identities are string-keyed in five places, verified: `SizeVar { name: String }`, `SizeLen { collection: String }`, `CostExtern { name: String }`, `CostUnknown { reason: String }`, and `CostInternTable { summaries: Map<String, ComplexitySummary> }`. Every one is the anemic-modeling class DESIGN §2 names — a `String` leaf standing where a grounded identity exists. The migration re-grounds each:
 
-- function and collection identity → `DeclarationRef` / `ValueIdentity` (the G1 cited-symbol resolution work already makes these resolvable)
+- function and collection identity → `DeclarationRef`, which exists today and resolves through `v2.std.decl_ref_resolution`. **`ValueIdentity` does NOT exist in the tree** — corrected 2026-08-05, after this line misled the C1 lane. It appears only inside the sibling note's *proposed* `CostSubject` and `CostJustification` code blocks; a corpus grep resolves it to no declaration of any kind. The original wording said the G1 cited-symbol work 'already makes these resolvable', which is true of `DeclarationRef` and false of `ValueIdentity` — the DESIGN §3 cited-symbol class, a name-level claim a grep decides, sitting false in an authority doc while the mechanism it describes stayed correct. C1 must therefore either ground size identity on the existing `SizeVariable` carrier or land a value-identity authority first; it may not cite a symbol that does not exist.
 - `CostExtern { name }` → `CostEffect { operation: DeclarationRef }`, joining the sibling note's `ExecuteEffect` atom rather than a second extern channel
 - `CostUnknown { reason: String }` → a typed, located, **countable** cause — a free-text reason cannot be tallied, so its frequency never ranks the deficit for fixing (DESIGN §5)
 - `Certainty = Proven | Conservative` → reconciled with the existing `DescentEvidence` and `Measured` bases rather than minted as a third confidence vocabulary