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

[gunbai-bot]

What this head actually delivers (updated 2026-08-06). The substantive C0(b1) carrier —
gunbc.v1_complexity_capability_census, its roster, its fast and long-lane witnesses, and the
v1 eviction-hazard control — already landed on main via #7840, which had merged this
branch before C0(b2) merged. Verified by content on origin/main.

What remains in this diff is four documentation corrections, 5 insertions / 5 deletions:
the false ValueIdentity citation (DESIGN §3 cite-the-symbol), the c0_scope_note and
complexity_capability_id_note scope narrowing so C0(b2) is not misread as the trigger that
closes capability discovery (DESIGN §4b trigger honesty), the closure_cost_note measured
disjoint-range result superseding its earlier "actual size is unknown" wording, and the removal
of a self-referential (see c0_scope_note) citation found by review 49160.

The title was renamed accordingly. Leaving it as the b1 delivery title would have written an
overclaim into main's history through squash-merge — the same class of defect this diff exists
to correct. The original description follows unchanged.

---

C0(b1): a reviewed v1 complexity inventory

What this is: an authored, exactly-cited, disposition-partitioned inventory of what v1.compiler.complexity carries, so C4 can be sized. What it is not: the closed capability denominator. That is C0(b2), which derives the population from DeclFact instead of authoring it, and it is open.

The title changed from "C0(b): … census" on operator review. "Census" and "C0(b)" both read as a completeness claim this lane does not make; a 26th capability omitted from the roster would not be detected here, and the carrier now says so in c0_scope_note rather than leaving it to be inferred.

Carrier

gunbc.v1_complexity_capability_census — v1_complexity_inventory_roster, 27 rows.

It is an inventory, not a capability roster. Legacy residues are not peers of capabilities:

V1ComplexityInventoryItem
  = SemanticCapabilityItem { capability }
  | LegacyHazardItem       { hazard, of_capability }
  | LegacyRealizationItem  { realization, of_capability }

The eviction hazard and the v1 parser walker are residues that belong to a capability, carried as typed edges. So counting rows (27) and counting capabilities (25) are now different questions with different answers — inventory_semantic_capability_count() answers the second, and w_legacy_residues_are_not_semantic_capabilities executes the distinction.

The C0(a) ruling is carried on three axes, not one

The previous revision fused role, destination, and fact-producer into one CostAuthorityModule enum. Two states that ought to be impossible were writable, and one was actually written:

axis	what it says	why separate
CostProgramRole	what a module is — includes RoleLegacyOracle	the ruling assigns v1 a role
CostMigrationDestination	where owed work may land — legacy oracle absent	"migrate into the deletion target" now has no constructor
CapabilityFactProducer	who produces the facts	parser-progress facts come from the v2 parser, not the cost lens

w_parser_progress_producer_differs_from_its_destination pins the specimen: that row lands in v2.lens.cost while its producer is FactsFromV2Parser. Under one enum it had to name the lens as its own producer, contradicting its own note.

Identity distinctness: validated, not constructed

Corrected on review. A closed coproduct makes an identity outside the vocabulary unrepresentable; it does not stop a List from carrying one twice. So inventory_identity_keys_distinct() validates it, w_roster_identities_are_distinct executes it, and w_distinctness_fold_reds_on_a_planted_duplicate proves the fold discriminates — a planted duplicate must come back false, or the green means nothing. The carrier and the plan note both say "validated" now. C0(b2)'s derived population supplies the construction wall this list cannot.

Citations resolve; they are not substring matches

Every row carries a typed DeclarationRef resolved through v2.std.decl_ref_resolution — DESIGN §3's cite-the-symbol rule, mechanically. The discriminating control is census_prose_only_name_does_not_resolve: a name that exists only inside a note string does not resolve, which a .contains() check would have accepted.

Findings, each executed

1. C4 is smaller than the parity note's table implied — but the work is integration, not nothing. std.graph (SCC), std.termination (DescentEvidence), std.computation (LoweringTarget), std.induction (CostBound) are all reached by import from v1 and by none of v2's lens modules. First revision projected these as discharged; corrected to IntegrationOwed, its own work-state.
2. A migration hazard, proven by execution (src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag): cache a summary with work 42, evict it, look it up — the seed returns Present with work 0, span 0, certainty Proven. A consumer reads costs nothing, proven. Paired control: a never-cached function correctly returns Absent, so the seed can express not computed and eviction declines to use it.
3. A receipt for the CostBasis ruling: cost_account_space_from_summary cites a Derived basis in prose, returns a bare ByteSize?, constructs no CostAccount, does not import std.realization_schedule, and CostBasis has no Derived arm.

Execution split, stated not buried

lane	file	runs per-PR?
fast structural	dag/test/claim/v1_complexity_capability_census_witness_test.dag	yes
exact resolution	dag/test/claim/long/…_resolution_test.dag	no — needs a decl_facts scan over a pool incl. src/v1
eviction hazard	src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag	no — v1_claim_scoped_witness_batch

Both non-per-PR lanes are enrolled on executing cadences with named local recipes in gunbc.ci_layer_roots, not on a deferral arm.

A cost finding this PR paid for, recorded rather than quietly fixed — and re-stated with its clock basis

An earlier revision of the fast-lane witness imported v2.lens.cost / v2.lens.complexity to run one 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, with no change to its own semantic work.

Main landed witness_row_cost_clock_basis_note (#7820) while this PR was open, and it changes what those two numbers may be claimed to mean. Both are wall; the fast-lane cap is enforced on thread CPU. So:

• 3901.9ms is a real reading. Eval is single-threaded, so a wall figure under the cap proves cpu under it.
• 5019ms is not a cost. It is a censored measurement — its value is where the kill landed, and the true figure is unbounded above.

The honest claim is therefore weaker in one direction and stronger in the other: the regression is at least 1117ms, its actual size is unknown, and what is decided is only that the row crossed. closure_cost_note now states it that way rather than quoting a delta between two figures on a clock the cap does not enforce.

The imports moved to the long lane with the control that needed them. It stays recorded 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.

Plan-note state

C0(a) signed · C0(b1) delivered on merge of this PR (not "already delivered" — the artifact is the merged carrier) · C0(b2) open · C0(c) open. The stale "parser progress is still unsized" line is gone: the operator ruled that disposition on 2026-08-05 and the census models it as two rows.

[gunbai-bot]

Re: review 48593 — all three findings were real, and all three are fixed. They were caught mid-recut: the schema split landed in one commit and the follow-through in the next, and an autocommit published the intermediate state. Verified against 7d29d83, not asserted:

1. MigrationOwed.producer omitted on almost every row. Correct — the field insertion matched once. Now on all 20 MigrationOwed rows (grep -c "producer: FactsFrom" → 20, grep -c "disposition: MigrationOwed" → 20). Nineteen carry FactsFromCostLens; parser_progress_fact_production carries FactsFromV2Parser, which is the whole point of splitting the axis and is pinned by w_parser_progress_producer_differs_from_its_destination.

2. Fast-lane witness out of sync with its authority. Correct. Rewritten for the split schema — imports now CostProgramRole / CostMigrationDestination / CapabilityFactProducer, V1ComplexityInventoryRow, SemanticCapabilityItem / LegacyHazardItem / LegacyRealizationItem, MigrateTo*, SummaryEvictionHazard, ParserProgressV1WalkerRealization. All fixtures construct V1ComplexityInventoryRow with item:.

3. inventory_item_key defined but never called — specification without execution. The sharpest of the three, and correct as written. Three witnesses now execute it:

• w_roster_identities_are_distinct — folds distinctness over the live roster
• w_distinctness_fold_reds_on_a_planted_duplicate — the discriminating control, without which the green above means nothing; it also asserts the same hazard against two different capabilities yields two distinct keys
• w_legacy_residues_are_not_semantic_capabilities — pins the inventory/capability split

While fixing this I also linearized the fold: inventory_identity_keys_distinct was recomputing the key list inside its own body (O(n³) at n=27). Now the list is built once and keys_are_distinct / key_occurrence_count are shared with the witness. Small n, but DESIGN §6's bare-minimum-cost rule says a proven cost-shape defect is fixed regardless of realized n.

Executed on 7d29d83, local, all green:

• fast lane, 14/14 (dag + src/v2), max row 50 ms
• v1 eviction hazard, 3/3 (dag + src/v1)
• long-lane exact resolution — running; result to follow

One thing worth flagging that is not a fix: main landed gunbc.witness_row_cost witness_row_cost_clock_basis_note (#7820) while this PR was open, and it changes what my own cost finding may claim. The fast-lane cap is enforced on thread CPU; the recorded column is wall. So the 3901.9 ms baseline is a real reading (eval is single-threaded, so wall under the cap proves cpu under it), but the 5019 ms figure is a censored measurement — its value is where the kill landed, so the true figure is unbounded above. closure_cost_note now says the regression is at least 1117 ms with unknown actual size, rather than quoting a delta between two figures on a clock the cap does not enforce.

— sent from proud-bear-834

[gunbai-bot]

Long-lane result, completing the receipt above — 7/7 on 7d29d83 (dag + src/v2 walk roots; the census pool roots add src/v1 via decl_facts(pool_roots:), which is why this cannot be a fast-lane row):

PASS census_every_declaration_ref_resolves_exactly
PASS census_absent_declaration_refuses
PASS census_absent_module_refuses
PASS census_prose_only_name_does_not_resolve
PASS census_resolved_identity_carries_observed_path
PASS census_shared_substrate_carrier_resolves
PASS census_complexity_admission_predicate_is_vacuous_by_execution
7 witness(es) in 53615ms

53.6 s of eval is exactly why it is a long-lane resident and not a per-PR row — and census_prose_only_name_does_not_resolve is the one that earns the cost: a name that exists only inside a note string does not resolve, which a substring check would have accepted.

All three lanes on this head: fast 14/14 · long 7/7 · v1 eviction 3/3.

— sent from proud-bear-834

[gunbai-bot]

CI on a05bc26: regen fixed, ci reached witness discovery, two real defects found

regen passed. The previous failure was mine and now understood: adding a .dag under src/v1/** puts it in the v1 self-host closure, so stage0_emit_plan_generated.dag and .gitattributes both grew a row for v1_tests_claim_v1_complexity_eviction_hazard_test.rs — but the generated .rs itself was never emitted. regen_verify_gate_passes recomputed the fixed point, found a declared-but-absent output, and correctly returned false.

Cause of my miss: there are two regenerators and I ran one. generated_artifact_gate main_wet covers ci.yml / docs/plans / .gitattributes / the emit plan; regen_stage0 covers the 127 src/v1/stage0/src/*.rs outputs, and it is the one the self-host gate recomputes. Running regen_stage0 produced exactly two changes — the missing file and a one-line lib.rs module row — confirming the fixed point was otherwise intact.

The timing receipt

ci reached witness discovery for the first time on this branch:

✓ witness_live_constraint_present_iff_line_unaccepted
  (dag/test/claim/roadmap_program_view_witness_test.dag leg=InterpretedLeg)  4191.9ms

The arc for the closure regression this PR caused and then fixed: 3901.9 ms on green main → 5019 ms censored → 4191.9 ms passing.

Stated with its limit: both figures are wall, the cap is thread CPU, and I will not claim the +290 ms against main's baseline is attributable. One measurement per side does not separate my corpus growth from host noise on a host whose own receipts move between repeats of an identical entry.

Four ci failures — two inherited, two mine

Inherited from main (red at its last five commits, not touched here): falsifier_cold_control_steps_follow_floor_in_job_order and red_floor_workflow_fixture_cold_controls_still_execute, both undefined variable: job_id.

Mine, 1 — a §3 name collision, which is the finding worth reading. RetirementTrigger already exists in the tree as a variant: gunbc.stage0_rust_lifecycle_totality LifecycleTotalityUnderivedAxis, and again in gunbc.stage0_rust_honest_frontier_projection. This census declared it as a top-level type, shadowing the variant and breaking lifecycle_totality_counts_retirement_trigger_as_underived_axis with an undefined-variable refusal — in a module this PR never touched.

Renamed to CapabilityRetirementTrigger, with the reasoning recorded on the carrier rather than only here, because the non-action matters more than the rename:

• It is accidental homonymy, not a fork. Theirs is an axis label for a fact the stage0 rust lifecycle cannot yet derive; mine is the trigger carrier that discharges a capability retirement obligation. Different subjects — unifying them would be false unification, which is the mirror error of the one §3 warns about.
• This census does not discharge lifecycle_totality_retirement_trigger_dissolve_on. That row waits for a RetirementTrigger carrier in gunbc.stage0_rust_source_lifecycle_scaffold, for the stage0 rust source lifecycle subject. A future reader finding a modeled retirement trigger here must not close that row against this one, so the carrier says so explicitly.

The irony is not lost: the PR whose subject is cite exactly, do not re-mint names re-minted a name. It was caught by CI, not by inspection — which is the argument for the gate, not against the census.

Mine, 2 — a stale count gate. witness_v1_claim_scoped_batch_is_file_grain_and_batch_owned asserts length(xs: v1_claim_scoped_witness_entries) == 3; the eviction witness makes it 4. Updated.

Flagging without fixing, deliberately: that literal is the change-detector shape DESIGN §5's oracle rule names — it is measured from the same tree it checks, and automating its update collapses the clause to measure() == measure(). The surrounding clauses in that witness are real property checks (source roots, scan dirs, selection mode, clamp), so the file is not worthless; but this one clause counts the entries someone remembered to author. Redesigning another module's witness is outside this PR's scope, so it is named here rather than done.

— sent from proud-bear-834

[gunbai-bot]

Re: review 48680 — fixed, with one correction to the stated consequence.

The finding is real: dag/gunbc/ci_layer_roots.dag line 1183 was } with no comma before the first appended census row, inconsistent with all 35 other rows in falsifier_substrate_long_lane_rows. Comma added.

The predicted effect did not occur, and I checked rather than assumed because the difference matters. The review says it "should fail compile/parse for gunbc.ci_layer_roots". It does not — and the evidence was already on the table before I looked: CI compile-clean passed on this head, regen passed, ci ran 6,849 discovery witnesses, and my local ci_floor_plan_witness_test run read v1_claim_scoped_witness_entries out of that very module and passed. A module that failed to parse could not have done any of that.

So the question worth answering was not "does it break the build" but "does it silently drop my seven rows" — a truncation would be worse than a parse error, because the long-lane enrollment would read as present while executing nothing. Measured by evaluating the projection:

gunbc run --source-root dag --source-root src/v2 \
  --entry dag/gunbc/ci_layer_roots.dag --function falsifier_substrate_long_lane_entries

36 entries before the comma, 36 after — all seven v1_complexity_capability_census_resolution_test rows present in both, ending with census_complexity_admission_predicate_is_vacuous_by_execution. The separator is tolerated at that position and nothing was lost.

Fixed regardless, for the reason that survives the correction: resting a load-bearing enrollment roster on an undocumented parser tolerance is not something to leave in place, and one row formatted unlike its 35 siblings is a reader trap even when the evaluator does not care.

Worth noting as a repo observation rather than a claim about this PR: an optional list separator is a position where a genuine typo cannot be caught by the parser. I have not chased whether that is deliberate, and it is outside this PR.

Also fixed since the last CI run, both found by ci reaching witness discovery for the first time on this branch:

• RetirementTrigger renamed to CapabilityRetirementTrigger — it collided with an existing variant of that name in gunbc.stage0_rust_lifecycle_totality and gunbc.stage0_rust_honest_frontier_projection, breaking a witness in a module this PR never touched. Detail and the deliberate non-unification in the comment above.
• witness_v1_claim_scoped_batch_is_file_grain_and_batch_owned entry count 3 to 4.

Verified locally by execution on the current head: census fast lane 14/14 · stage0_rust_lifecycle_totality_witness_test 7/7 including the witness the collision broke · ci_floor_plan_witness_test 2/2 · long lane 7/7 · v1 eviction 3/3.

— sent from proud-bear-834

[gunbai-bot]

CI settled on 5029e77 — every defect of mine is gone; the two reds are main's

build                      success
heal_generated_artifacts   success
regen                      success
ci                         failure  (2 of 6849 discovery witnesses)

The two failures:

falsifier_cold_control_steps_follow_floor_in_job_order   runtime error: undefined variable: job_id
red_floor_workflow_fixture_cold_controls_still_execute   runtime error: undefined variable: job_id

Both in dag/test/claim/falsifier_workflow_witness_test.dag, which this PR does not touch. Main's last two completed runs fail with the identical pair. This branch runs 6,849 discovery witnesses against main's 6,835 — 14 added, zero new failures.

Three defects that CI found on earlier heads are fixed and verified by execution, not inspection:

defect	fix	verified
stage0 output declared but never emitted	ran regen_stage0	regen green on three consecutive heads
RetirementTrigger §3 name collision	renamed to CapabilityRetirementTrigger	stage0_rust_lifecycle_totality_witness_test 7/7
stale entry-count gate (3 → 4)	updated	ci_floor_plan_witness_test 2/2

The timing receipt, with a second reading

run	figure
green main (baseline)	3901.9 ms
this PR, before the closure fix	5019 ms — censored
this PR, reading 1	4191.9 ms ✓
this PR, reading 2	4106.4 ms ✓

What can be said: the closure regression is closed — the witness is back under the cap with roughly 800–900 ms of headroom, and both readings pass.

What cannot: whether the ~200–290 ms above main's baseline is real. My two readings differ by 85.5 ms, so the gap to main does exceed my own observed spread — suggestive of a small genuine increase. But main's baseline is a single measurement with no spread estimate, and per witness_row_cost_clock_basis_note these are wall figures while the cap is thread CPU. I am recording it as likely a small real increase, not established, rather than picking whichever reading tells a nicer story.

Main's break, diagnosed but deliberately not fixed here

fn falsifier_job_steps(job_id: String) -> List<Step> {
  fold(falsifier_workflow.jobs, init: [], f: fn(acc, j) {
    if j.id == job_id { j.steps } else { acc }
  })
}

The lambda does not capture the enclosing function's parameter. The sibling ci_job_steps() survives only because it inlines a literal "ci" rather than referencing a parameter.

Two observations, the second being the one worth acting on:

1. The tempting patch — inline the literal, as the sibling does — is DESIGN §5's unmarked workaround verbatim: it routes around a language-layer defect and zeroes the defect's frequency so it never ranks for fixing.
2. An unbound variable in a lambda body is structurally decidable at compile time, yet this surfaces as a runtime undefined variable. That is a §4b rung inversion: a class sitting at mitigatable that the closed substrate should be able to place at structurally guaranteed. Whichever way the capture question is resolved — lambdas capture, or they are refused — the refusal belongs at compile time.

Not touched here because it is outside this PR and fixing it would widen the diff into a module I have no mandate over. Flagged for routing.

Merge readiness — one thing I cannot verify

dashboard-ops reviews gunbc#7821 returns no data: null head, null mergeable, null checks, empty provider lists. Not "zero approvals" — no record at all, and the same for #7841. GitHub's own review list is empty because these are dashboard-only artifacts.

So I have no authoritative read on the tally, and I am not converting the notification stream into one. What I can state on my own evidence: mergeable: MERGEABLE, open, not draft, head 5029e77, and CI red solely on two witnesses identical to main's.

Per the temporary policy I am not merging this myself.

— sent from proud-bear-834

[gunbai-bot]

Merge-packet status at head c43428efaa8.

Main advanced by three commits (#7824, #7790, #7844) and I merged them. The merge collided at the tail of gunbc.ci_layer_roots falsifier_substrate_long_lane_rows — my seven C0(b1) census rows and main's two new rows append at the same list position. Both sides are kept: 39 rows, no duplicate (entry, function) pair, every entry file present on disk.

One thing worth reading in the history rather than glossing: 05096abf5dc ("WIP: cost analysis") carries the conflict markers. The autocommit path committed and pushed the conflicted file before I resolved it, and it left no MERGE_HEAD, so the tree read as a completed merge. c43428efaa8 is the repair of that state. Nothing between the two was ever green, and no reviewed content changed — the resolution is purely the two row sets concatenated.

Silent-drop check on the three merge=generated-artifact files ran after the merge, per the hazard that bit this PR earlier today: stage0_emit_plan_generated.dag, src/v1/stage0/src/lib.rs, and .gitattributes all still carry main's rows plus this branch's one new registration. No regeneration was needed — the branch-vs-main file set is exactly the fifteen files this PR authors.

Census suite re-run on the merged tree: 14/14 PASS, 10ms of eval across all fourteen.

— sent from proud-bear-834

[gunbai-bot]

CI red at c43428e, and the failure is not in this diff. Recording it here because the automated notice attributes it to this PR.

build, regen, and heal_generated_artifacts are green. The ci floor fails at dag_compile_clean_gate_passes, with ~100 hard diagnostics all in one file this PR does not touch:

dag/gunbc/plans/branch_merge_admission_model.dag:15:15: error: function 'row' not found in scope
dag/gunbc/plans/branch_merge_admission_model.dag:15:27: error: function 'cell' not found in scope

Mechanism: that module has no imports and resolves cell/row as bare references. gunbc.plans.md_helpers defines cell(text:) -> MarkdownTableCell and row(cells:) -> MarkdownTableRow. Main tip 4f9112965af (#7824) added a second module-scope pair in dag/gunbc/roadmap_instrument_sandbox.dag — cell(s: String) -> Fragment and row(cells: List<Fragment>) -> Fragment. Two candidates, no import, resolution refuses. This is the Class B shape DESIGN's open threads describe, with the pool-membership coincidence broken by a homonym rather than by a stripped import.

Confidence, stated rather than implied: I have the before/after (one such definition pair in the tree before #7824, two after) but I have not run a control that flips only that variable. deep-bat-181 reports verifying the same mechanism independently before landing their fix, and narrows the affected population to exactly two plan modules — this one and merge_admission_gate_shape_proposal — with every other md_helpers consumer already importing the definer.

The repair is already written and is not mine: #7832 adds import gunbc.plans.md_helpers { h2, h3, p, li, ul, quote, cell, row } to both files. I am not pushing a duplicate of it into another lane's file to unstick my own PR — a byte-identical race would only churn their branch. This PR is blocked on #7832 landing, after which I will merge main and rerun the floor.

Nothing about the reviewed content of this PR changed.

— sent from proud-bear-834

[gunbai-bot]

Correction to my previous comment. The causal story I gave for the compile-clean red is not established, and the control I said would close it did not.

What I got wrong:

1. I said main would red with the same diagnostic. Main did red on 4f9112965af, but on a different failure: WITNESS ADMISSION REFUSAL cause=FrozenPathDeferralGrew count=14 (gunbc.witness_deferral_freeze gained identities relative to its diff baseline). Main compile-clean passed.

2. It passed because main ran compile-clean at affected-set scope — 396 entries, module_rows=578 — so it never compiled branch_merge_admission_model.dag. This PR ran whole-tree, module_rows=1490, because merging main pulled compiler-infra .rs changes into the diff and forced the whole-tree baseline. This PR-s own pre-merge run was also affected-set (350 entries, module_rows=526).

3. A local test cuts against the homonym mechanism. Resolving the module directly with both md_helpers and roadmap_instrument_sandbox under the source roots evaluated cleanly and returned a MarkdownBlock — no cell not found. So the homonym does not break resolution at that pool breadth, and my "two candidates, resolution refuses" account does not hold as stated.

What still stands, and what it now means: the failing file is unchanged by this PR, and the difference between passing and failing is compile-clean scope, not content. So the breakage is latent on main and exposed by this PR-s whole-tree scope. Whether it arrived with #7824 is circumstantial (that module was added there, md_helpers is unchanged since #6927, exactly two module-scope cell/row pairs exist) and I have not isolated it.

I am not spending a whole-tree local compile to attribute the cause. #7832-s repair is explicit imports, which resolve a bare-reference failure whichever module created the ambiguity, so the fix does not depend on the attribution being right.

Also upstream of this PR: main is currently red on FrozenPathDeferralGrew, so merging main again pulls that in too. Both reds are external to this change, and nothing about its reviewed content has moved.

— sent from proud-bear-834