Skip to content

Bind documentary system references to live declarations - #8066

Merged
briansrls merged 18 commits into
mainfrom
session/calm-newt-575
Aug 10, 2026
Merged

briansrls merged 18 commits into
mainfrom
session/calm-newt-575

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 9, 2026 •

Copy link
Copy Markdown
Contributor

Documents in this repository name the systems they discuss in prose, so a system can be renamed, deleted, or forked in two while every sentence describing it stays green. This binds those names to live declarations instead.

The measured specimen. The body-lowering paragraph named v2.std.symbol_index SymbolIndex as an open prerequisite gating Stage A. The prerequisite was discharged; the declaration existed the whole time; the sentence stayed. Nothing was wrong with the declaration, so no declaration-level check could fire — and the sentence was not a reference to anything, so no reference-level check could either. Four copies of that one claim were live across DESIGN.md and two plan documents.

What this does

  • gunbc.documentary_refs carries one typed DeclarationRef per system a migrated paragraph names, and the paragraph renders its symbol text from those rows. A row typed beside a paragraph that independently spells the same name would be two representations of one fact, so the bytes come from the row.
  • v2.lens.cited_symbol_resolution's denominator widens from hand-authored binds to hand-authored plus generated-document references. The population widened; no second resolver was written — v2.std.decl_ref_resolution stays the single authority for what resolving a reference means, because a second algorithm that agrees today is a fork that disagrees later.
  • docs/plans/general-body-producer-design.md is enrolled as a HandAuthoredDocBind carrying the same three systems.
  • The four stale gate copies are deleted, and the superseded numbered five-minute sequence is replaced by a citation of gunbc.roadmap_authority five_minute_ci_gate_program_note — rendered from its row, asserting nothing about its mutable contents.

What this deliberately does NOT establish

A resolved reference proves the named system exists and is uniquely identified. It does not prove a production relationship — that a consumer invokes an implementation on a live path is a different claim needing an executing witness, and a reference population cannot carry it. Reference resolution is the honest rung here.

Product RED

documentary_refs_witness_test runs the perturbations against cited_declaration_ref_refusal_count — the resolver the required gate itself calls, not a second one agreeing with it:

control result
intact population 0 refusals
referenced system removed, no document source edited refuses
system forked into two same-named declarations refuses (exists, and a grep passes — only zero/one/many catches it)
rendered symbols appear in the generated document holds
population is the union of both sources holds

Recut history

An earlier head of this branch built a documentary-standing subsystem (design_truth, design_projection, design_subject_registry) and a declaration-grain consumption authority (v2.lens.decl_consumption). Both are deleted here, per operator ruling: the consumption module was not consumed by documentary standing or PR delivery on this branch, was knowingly binder-imprecise, and its root population was structurally always partial — it could not become an authority. The concrete stale-claim cleanup survives; the architecture does not.

One repair that was not mine

gunbc.doc_graph_roots carried NativeBlocked{GeneralWitnessTargetModelUnavailable} unescaped in a dissolution string. It compiles on main only because nothing in that closure pulled the module in; the new design_document → documentary_refs → doc_graph_roots edge exposed it as a parse-time undefined variable. Escaped rather than routed around — dodging it by dropping the import would have been the workaround DESIGN §5 names.

The repository already generates DESIGN.md, ROADMAP.md and every registered
plan with a byte-drift wall. That wall proves checked-in Markdown equals prose
stored in .dag; it does not prove the prose equals the standing of the
implementation. gunbc.design_document builds its sections from literal p(text:)
and li(text:) strings, so a sentence there can become false without any file it
describes being touched, and nothing in the tree can see it.

Carriers:
- gunbc.design_truth: subject identity, contract, contract proof, realization
  binding, production-consumer reachability, and the standing fold
  (Declared | Realized | RealizedContractProofUnmeasured | Ambiguous |
  ContractChanged | Retired | Unreadable). No stored status field and no
  rendered standing string.
- gunbc.design_projection: every sentence is a function of typed rows; no
  parameter accepts a status, so a migrated section cannot build one.
- gunbc.design_subject_registry: the declared subject population, one subject.
- dag/test/claim/design_truth_witness_test.dag: every arm in discriminating
  pairs.

First migrated thread: the "gated on the namespace lane's containment
SymbolIndex" claim. That gate is discharged (v2.std.symbol_index is consumed by
v2.compiler.resolve lookup_symbol_index_atom_identity on the production path)
and the sentence had FOUR copies -- design_document (hence DESIGN.md), the plan
doc, and two in wave2_prep_design. All four retired; DESIGN.md renders the
binding from the registry. Stage A itself remains open and is unchanged.

Also deletes the superseded six-step five-minute-CI sequence from
design_document, citing gunbc.roadmap_authority five_minute_ci_gate_program_note
by symbol only. #8034 recut that note, so a draft that summarized its contents
was already false on main.

DeliverableSubject wraps RoadmapNodeIdentity rather than minting a fifth
subject key space; a scheduled subject with an independent key has no
representation.

RealizationContractProof is a coproduct rather than a required digest: the
first draft carried 0000000000000000, a fabricated value in the position whose
job is to record what a realization was proven against. Measurement exceeded a
45-minute executor budget (CONFIDENCE-0 measured the same class at 409s wall,
~92% in load_bare_edge_index), so the state is typed with a named trigger
instead of guessed. Contract-drift detection is not active for the production
row; the mechanism is proven on fixtures.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title doc cleanup Derive documentary standing from typed rows instead of authored prose Aug 9, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 9, 2026 01:35
@gunbai-bot

gunbai-bot Bot commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

Correcting my own PR description before review starts — two defects, both mine.

1. DESIGN.md in this branch is stale relative to its generator, so the drift gate will red. I edited design_document.dag's five-minute sentence after the last regeneration and did not re-run main_wet. A verification run confirms DESIGN.md differs after regeneration. That is precisely the class this PR exists to remove, committed by the PR that removes it — worth stating plainly rather than quietly fixing, because it is evidence for the change: the byte-drift wall caught it, and nothing else would have. Fix incoming as a follow-up commit with the regenerated bytes.

2. The evidence claim in the description is overstated and I am withdrawing part of it. The description says 14 witnesses were green before the RealizationContractProof refactor and a 15th was added. On the post-refactor re-run, 10 of 15 reported PASS and 0 reported FAIL — the other 5 produced no line at all. The five unaccounted are exactly the digest-comparison group (zero_realizations_is_declared, one_realization_is_realized, two_realizations_refuse_as_ambiguous, moved_contract_is_stale, unmoved_contract_is_not_stale), which includes the moved/unmoved pair I cited as the key discriminator.

They passed on the pre-refactor run, so the likely cause is the refactor, but 'likely' is not a result. The run also died on a 45-minute executor timeout caused by an unpaged git diff blocking on --More--, so I cannot distinguish 'did not run' from 'ran and printed nothing'. Re-running the five in isolation now and will post the actual outcome either way.

Until that lands, the honest state of this branch is: 10 witnesses confirmed green by execution, 5 unverified, DESIGN.md drift-red. Please weight the description's Evidence section accordingly — the reachability, retirement, identity-fork, unmeasured-proof, dissolution and registry-citation controls are confirmed; the contract-digest discrimination is not.

@gunbai-bot

gunbai-bot Bot commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

Witness result: all 15 green by execution. Withdrawing the doubt I raised, not the caution.

The five unaccounted witnesses were re-run in isolation against the same head and all five PASS:

PASS design_truth_zero_realizations_is_declared
PASS design_truth_one_realization_is_realized
PASS design_truth_two_realizations_refuse_as_ambiguous
PASS design_truth_moved_contract_is_stale
PASS design_truth_unmoved_contract_is_not_stale

Combined with the 10 from the prior run at the same head, 15 of 15 are confirmed green, including the moved/unmoved contract pair — the discriminator the Evidence section rests on. The RealizationContractProof refactor did not break them.

What I will not do is invent a cause for the earlier silence. The run that lost them died on a 45-minute executor timeout triggered by an unpaged git diff blocking on --More--, and the five missing lines were the first five in the roster. I can rule out failure (they pass, and 0 FAIL was reported) but I cannot explain the omission, so it is recorded as unexplained rather than dressed up. The operational lesson is real regardless: a truncated harness run reported a strict subset of its roster with no indication that anything was missing, which is a reporting shape that can turn a partial run into a false green. That is worth someone's attention independent of this PR.

DESIGN.md drift: the regenerated five-minute sentence has been applied locally and a regeneration run is verifying that the committed bytes now equal the generator output. Pushing once that returns clean — I am not pushing a fix I have not verified, which is the same discipline that kept the placeholder digest out of this branch.

Corrected standing of the branch: 15/15 witnesses green by execution; DESIGN.md drift fix verified-and-pushed pending. The Evidence section in the description is accurate as written.

gunbc-ci-auto-heal and others added 3 commits August 9, 2026 01:49
The prior commit edited gunbc.design_document's five-minute sentence without
re-running main_wet, so the committed DESIGN.md was stale relative to its
generator and the drift gate would have redded. Regenerated bytes verified by
executing the generator and comparing output.

Worth recording rather than fixing silently: the PR that removes stale
generated-doc drift shipped stale generated-doc drift, and the byte-drift wall
is what caught it. That is the wall working, and it is also why the projection
half matters -- the drift wall proves the Markdown equals the .dag prose, and
only a derived projection can make the .dag prose track the tree.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every authored row now receives a disposition, and three fields that
were stored-but-unread became load-bearing.

- design_standing no longer filters rejected realizations out before
  counting them. It partitions admitted/rejected and disposes of both:
  DesignMixedValidAndInvalidRealizations, DesignRealizationUnreachable,
  DesignRealizationUnreadable. The previous fold was the
  empty-observation narrow this carrier exists to close, and the
  witness that blessed it asserted DesignDeclared for an unreachable
  realization; it now requires a refusal.

- Retirement cardinality is counted, not list_head-selected, in BOTH
  folds. Two retirements is DesignDuplicateRetirement /
  AuthoredDuplicateRetirement; a retirement beside a live realization
  is DesignRetiredWithLiveRealization rather than a silent DesignRetired.

- design_contract_for_subject returned Optional, so two registered
  contracts for one subject produced the first one and made standing
  depend on authoring order. It returns DesignContractSelection with
  ContractSubjectUnregistered and ContractSubjectDuplicated as separate
  arms, and drops a bare `filter` that was the capture hazard this
  module's own note documents.

- DeclarationPresence replaces the Optional presence probe: module-absent
  maps to unreadable rather than absent, because on a corpus that does
  not whole-tree-resolve it is routinely a universe hole, and
  DeclarationAbsentCondition was reading every failure arm as
  DissolutionReached.

- evidence enters admission. A realization whose named witness
  declaration does not resolve is refused
  (DesignRealizationEvidenceMissing / EvidenceUnreadable) rather than
  reading DesignRealized off an unread field. Presence is not execution
  and the note says so.

- design_projection_note no longer calls itself a construction wall
  without qualification: the guarantee is scoped to sections that
  consume the projection, and corpus-wide coverage is monotone.

21/21 witnesses green by execution, including four new controls for the
dropped-row class and one for evidence admission.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

All six blocking findings are real and all six are fixed. Pushed; 21/21 witnesses green by execution (12 + 10 in two runs, the retirement control re-run after its expectation changed).

1 — the fold dropped broken rows before counting. Confirmed, and it is the sharpest of the six: I built the empty-observation narrow I have been citing all session, inside the carrier that exists to close it, and wrote a witness that blessed it (design_truth_unreachable_realization_is_not_admitted asserted DesignDeclared for a subject whose only realization is unreachable — "nothing here" where the truth was "one row, refused"). design_standing now partitions into admitted/rejected and disposes of every authored row: DesignMixedValidAndInvalidRealizations, DesignRealizationUnreachable, DesignRealizationUnreadable. The witness requires a refusal now. Four new controls cover the class.

2 — retirement cardinality. Counted in both folds. Two retirements → DesignDuplicateRetirement / AuthoredDuplicateRetirement; a retirement beside a live realization → DesignRetiredWithLiveRealization, not a silent DesignRetired. design_retirement_for_subject is deleted rather than left beside its replacement.

3 — dissolution conditions fail open on ambiguity. DeclarationPresence replaces the Optional probe. The reasoning I want on record because it cuts the other way from the obvious fix: module-absent maps to unreadable, not absent. Only DeclarationRefDeclarationAbsent means "the module is declared and the declaration is genuinely not in it"; module-absent on a corpus that does not whole-tree-resolve is routinely a universe hole, and treating it as deliberate absence would let an excluded import target retire live work.

4 — evidence stored and never read. Now part of admission. A realization whose named witness declaration does not resolve is refused (DesignRealizationEvidenceMissing / EvidenceUnreadable) instead of reading DesignRealized off an unread field. Scoped honestly in realization_evidence_admission_note: presence closes the rot channel (a renamed or deleted witness reds), it is not execution — enrollment is the floor's question and claiming it here would be a rung the fold cannot support.

5 — list_head in the registry. design_contract_for_subject returns DesignContractSelection (ContractSelected / ContractSubjectUnregistered / ContractSubjectDuplicated). It also dropped a bare filter, which is exactly the capture hazard design_truth_bare_name_capture_note documents for this module's own pool — the defect and its own written warning were three hundred lines apart.

6 — "construction wall" overstated. Corrected in design_projection_note. design_document can still call p(text:) with any literal, so the guarantee is scoped: a section that consumes design_subject_standing_sentence cannot carry an authored standing; a section that does not is unmigrated. Structural at the seam, monotone across the corpus. Calling it a wall over DESIGN.md would be the §4b rung inflation.

On the required finish line — I am declining part of it, with reasons.

You wrote that #8066 should not merge while its production standing depends on acknowledged fail-open module-grain reachability, and that the migration should complete in this PR. I accept the defect and decline the remedy, on three grounds:

  • The declaration-grain authority does not exist and is not mine to mint. warm-crane-642 (CONFIDENCE-0) measured the same gap independently and disclaims authorship of the symbol→consumer edge. Building a second one here to unblock my own PR is the §3 fork this carrier is about.
  • Whole-corpus reachability is unsound today, not merely expensive: src/v2 does not whole-tree-resolve (wiring_liveness_whole_tree names v2.lens.resolved_imports as its blocker), so a consumer outside the universe renders its subject unconsumed — the empty-observation narrow, which invites deleting live code. It is also unaffordable: 409s wall, ~92% in load_bare_edge_index.
  • The registry is deliberately one subject. Growing it corpus-wide before the grain is right would multiply an acknowledged fail-open across every migrated thread.

What I have done instead is make the gap typed, cited, and dissolving: design_realization_reach_second_query_disposition names the second module-grain query, names the shared point-query authority as its dissolve-on target (explicitly not module_impact_query_front_door, which is the 409s whole-corpus fold), and the one production row stands at DesignRealizedContractProofUnmeasured rather than DesignRealized — so the generated sentence in DESIGN.md says the drift detection is inactive for it.

If you want the merge blocked until the declaration-grain authority lands, say so and I will park the branch rather than argue it — but that authority is a separate lane with a separate owner, and this PR does not get better by waiting inside it.

— sent from calm-newt-575

@gunbai-bot
gunbai-bot Bot marked this pull request as draft August 9, 2026 03:49
@gunbai-bot

gunbai-bot Bot commented Aug 9, 2026

Copy link
Copy Markdown
Contributor Author

Moved to draft under the new operating guidance, before the approvals could carry it to merge.

This PR is a specimen of the local-proof attractor, and I should name it rather than wait to be told. The stale-doc problem I was given is: a documentary claim in this repository cannot be false without something reddening. What I hit was the missing declaration-grain reachability authority. What I then did is the exact sequence in the ruling — typed the missing capability (ContractProofUnmeasured, DesignRealizedContractProofUnmeasured, the second-query disposition), narrowed the boundary to one subject, put strong fixtures around the narrowed boundary (21 witnesses, 5 REDs), described the rest as monotone migration, and collected two approvals for a locally honest implementation. Two reviewers called it clean, and against its narrowed contract it is.

Displacement standing, in the denomination that matters:

paragraphs in DESIGN.md whose standing is derived 1 / ~50
stale claims that would now red 0 — nothing gates on design_standing; there is no consumer
production rows at full strength 0 / 1 — the one row is ProofUnmeasured, drift detection inactive
prose status sentences made unwritable 0 — p(text:) still takes any literal

The witnesses are green by execution and the carrier is real, but by the merge-is-evidence-not-acceptance rule this is support delivered, outcome displacement ~0. There is no executing consumer, so the mechanism cannot yet make any document wrong.

What it would take to earn the outcome, so the residue is a bounded list rather than a gesture: a gate that runs design_standing over the registry per PR and reds on a refusing arm; the declaration-grain reachability authority, which is the same dependency CONFIDENCE froze on and which I do not own; and the migration of the remaining paragraphs, which is only meaningful once the first two exist.

Holding here for the operator's ending sentence rather than opening a successor.

— sent from calm-newt-575

gunbc-ci-auto-heal and others added 12 commits August 9, 2026 06:48
Steps 1-2 of the absorbed blocker. One shared authority answering
"which declarations reference this declaration", built once per run,
cheap point queries thereafter -- the doc standing gate consumes it
now and the PR delivery check consumes it later, neither approximating
it and neither forking it.

v2.lens.witness_cost_locality states in tree that module grain IS the
declared precision frontier and fn-grain reachability does not exist.
That is what this replaces. Module grain is fail-open exactly where
both consumers care: a declaration added to a module that already has
dependents reads as reached while nothing references it.

Design decisions worth the review time:

- Resolution is over the DECLARATION universe (decl_facts), not the
  BINDING universe (SymbolIndex.global_bare). Same shape, different
  populations: the binding index contains parameters and let binders,
  so it would refuse edges the declaration question determines. The
  reconciliation trigger is named -- the namespace lane's containment
  tree makes both one index.

- Consumers are carried as DeclarationIdentity, not DeclarationRef.
  The only composer in tree runs ref -> qualified name; splitting on
  the final dot to manufacture the inverse would be a second naming
  scheme decided by punctuation, and would fabricate a module_path for
  any name the guess did not fit. So the index keys on qualified names
  and the point query composes.

- A subject the fact pack does not declare REFUSES
  (SubjectUniverseAbsent) rather than answering zero consumers. Those
  two states license opposite actions -- the first is a universe hole,
  the second licenses deleting the declaration.

- An ambiguous short name lands in unresolvable and credits NEITHER
  candidate. Undecidable edges are carried, never dropped: a dropped
  edge renders as "no consumers", and the action taken on that answer
  is deletion.

- Self-references are excluded. Every fn names itself at its own
  definition site and host-backed stubs call themselves, so counting
  them would give every declaration a consumer by construction.

The residual imprecision is stated rather than asserted absent: a
local binder colliding with a declaration name produces an edge no
reference justifies. Fail-open, narrow, and it dissolves on the same
containment-tree walk.

6/6 witnesses green by execution, each asserted against its opposite
population. The orphan control is the one the predecessor cannot
reach: fx.m.orphan sits in a module that has dependents.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The floor's naming-hygiene walk refused v2.lens.decl_consumption for
carrying no construction_justification, which is the DESIGN §5/§6 gate
asking why the bad-state class is not made unwritable instead.

Classified WallAfterGrounding, dissolving to SingleAuthority, because
the honest answer is neither of the easy ones. The class -- an authored
declaration no live consumer reaches -- is DECIDABLE given the
declaration universe, so calling it RatchetForever would be the "never"
trap §5 names. But consumption is not a LOCAL property: a declaration
and its consumer can be authored in one commit, so nothing at the
authoring site separates the good case from the bad one and only a
whole-corpus read decides it. A whole-corpus read is a reader.

It becomes a wall on the same trigger the module's other two residues
name -- the containment tree as single naming authority, at which point
a reference is an edge in a structure the compiler already walks and an
unreached declaration is refusable the way an unbound name already is.
One grounding closes the universe fork, the binder-shadowing
imprecision, and this justification together.

6/6 witnesses still green.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Step 3. A root is a declaration nothing needs to reference, so the
purpose law cannot read an unreferenced declaration as dead without
first knowing the root set. Joining an explicit ScheduleWitnessEntry
roster to decl_facts by (rel_path, name) yields real declarations --
legitimate rather than positional citation in disguise, because the
roster natively carries a path and a name and this join CONSUMES the
identity it already has instead of inventing one.

The finding is what is NOT enumerable. Since the discovery flip most
executing witnesses are found by a host-side directory scan
(CiSpec.discovery_scan_dirs) that no .dag fold can read, and
generated-artifact producers are dispatched by a match in
gunbc.generated_artifact_emit rather than listed as declaration names.
So the root set is structurally incomplete here.

decl_consumption_roots therefore returns RootEnumerationPartial and
CANNOT return RootsEnumerated today -- the total arm exists because
the population becomes enumerable once discovery is declared, and it
is deliberately unselectable until then. An empty root set must read
as unknown, never as proof a declaration is unrooted, because that
conclusion licenses deleting live code. Its witness asserts the
partial arm even though every roster entry resolved, which is the
claim that matters: the incompleteness is not about the roster.

7/7 witnesses green by execution.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The floor's lens_registry_completeness_holds_live failed: a new module
under v2.lens.* is either an enrolled enforcing lens or a declared
infra row, and mine was neither. That is the inert-lens backstop
working -- coverage by illusion is the tier where machinery exists and
nothing gates on it, so an unenrolled module must red.

Enrolled as infra rather than as a LensIdV0 row, and the distinction
is the real one rather than the convenient one: decl_consumption
produces facts (subject in, consuming declarations out) and carries
no verdict and no remedy. The verdict lives in the documentary
standing fold that consumes it. That is precisely the class
v2.lens.module_impact_query already occupies one grain up, whose row
says the same thing -- a reading with no verdict authority.

The generic infra dissolve_on applies unchanged: the row deletes if
the module ever gains its own verdict authority or leaves src/v2/lens.

Verified by executing the failing witness, not by reasoning about the
roster.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts:
#	dag/gunbc/doc_graph_roots.dag
@gunbai-bot gunbai-bot Bot changed the title Derive documentary standing from typed rows instead of authored prose Bind documentary system references to live declarations Aug 9, 2026
…ion/calm-newt-575

# Conflicts:
#	DESIGN.md
@briansrls
briansrls marked this pull request as ready for review August 10, 2026 02:12
@briansrls
briansrls merged commit 5d3d165 into main Aug 10, 2026
17 checks passed
@briansrls
briansrls deleted the session/calm-newt-575 branch August 10, 2026 02:37
briansrls pushed a commit that referenced this pull request Aug 10, 2026
* Derive documentary standing from typed rows instead of authored prose

The repository already generates DESIGN.md, ROADMAP.md and every registered
plan with a byte-drift wall. That wall proves checked-in Markdown equals prose
stored in .dag; it does not prove the prose equals the standing of the
implementation. gunbc.design_document builds its sections from literal p(text:)
and li(text:) strings, so a sentence there can become false without any file it
describes being touched, and nothing in the tree can see it.

Carriers:
- gunbc.design_truth: subject identity, contract, contract proof, realization
  binding, production-consumer reachability, and the standing fold
  (Declared | Realized | RealizedContractProofUnmeasured | Ambiguous |
  ContractChanged | Retired | Unreadable). No stored status field and no
  rendered standing string.
- gunbc.design_projection: every sentence is a function of typed rows; no
  parameter accepts a status, so a migrated section cannot build one.
- gunbc.design_subject_registry: the declared subject population, one subject.
- dag/test/claim/design_truth_witness_test.dag: every arm in discriminating
  pairs.

First migrated thread: the "gated on the namespace lane's containment
SymbolIndex" claim. That gate is discharged (v2.std.symbol_index is consumed by
v2.compiler.resolve lookup_symbol_index_atom_identity on the production path)
and the sentence had FOUR copies -- design_document (hence DESIGN.md), the plan
doc, and two in wave2_prep_design. All four retired; DESIGN.md renders the
binding from the registry. Stage A itself remains open and is unchanged.

Also deletes the superseded six-step five-minute-CI sequence from
design_document, citing gunbc.roadmap_authority five_minute_ci_gate_program_note
by symbol only. #8034 recut that note, so a draft that summarized its contents
was already false on main.

DeliverableSubject wraps RoadmapNodeIdentity rather than minting a fifth
subject key space; a scheduled subject with an independent key has no
representation.

RealizationContractProof is a coproduct rather than a required digest: the
first draft carried 0000000000000000, a fabricated value in the position whose
job is to record what a realization was proven against. Measurement exceeded a
45-minute executor budget (CONFIDENCE-0 measured the same class at 409s wall,
~92% in load_bare_edge_index), so the state is typed with a named trigger
instead of guessed. Contract-drift detection is not active for the production
row; the mechanism is proven on fixtures.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Regenerate DESIGN.md after the five-minute citation rewrite

The prior commit edited gunbc.design_document's five-minute sentence without
re-running main_wet, so the committed DESIGN.md was stale relative to its
generator and the drift gate would have redded. Regenerated bytes verified by
executing the generator and comparing output.

Worth recording rather than fixing silently: the PR that removes stale
generated-doc drift shipped stale generated-doc drift, and the byte-drift wall
is what caught it. That is the wall working, and it is also why the projection
half matters -- the drift wall proves the Markdown equals the .dag prose, and
only a derived projection can make the .dag prose track the tree.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Close the six blocking review findings on the design-truth carrier

Every authored row now receives a disposition, and three fields that
were stored-but-unread became load-bearing.

- design_standing no longer filters rejected realizations out before
  counting them. It partitions admitted/rejected and disposes of both:
  DesignMixedValidAndInvalidRealizations, DesignRealizationUnreachable,
  DesignRealizationUnreadable. The previous fold was the
  empty-observation narrow this carrier exists to close, and the
  witness that blessed it asserted DesignDeclared for an unreachable
  realization; it now requires a refusal.

- Retirement cardinality is counted, not list_head-selected, in BOTH
  folds. Two retirements is DesignDuplicateRetirement /
  AuthoredDuplicateRetirement; a retirement beside a live realization
  is DesignRetiredWithLiveRealization rather than a silent DesignRetired.

- design_contract_for_subject returned Optional, so two registered
  contracts for one subject produced the first one and made standing
  depend on authoring order. It returns DesignContractSelection with
  ContractSubjectUnregistered and ContractSubjectDuplicated as separate
  arms, and drops a bare `filter` that was the capture hazard this
  module's own note documents.

- DeclarationPresence replaces the Optional presence probe: module-absent
  maps to unreadable rather than absent, because on a corpus that does
  not whole-tree-resolve it is routinely a universe hole, and
  DeclarationAbsentCondition was reading every failure arm as
  DissolutionReached.

- evidence enters admission. A realization whose named witness
  declaration does not resolve is refused
  (DesignRealizationEvidenceMissing / EvidenceUnreadable) rather than
  reading DesignRealized off an unread field. Presence is not execution
  and the note says so.

- design_projection_note no longer calls itself a construction wall
  without qualification: the guarantee is scoped to sections that
  consume the projection, and corpus-wide coverage is monotone.

21/21 witnesses green by execution, including four new controls for the
dropped-row class and one for evidence admission.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Land the declaration-grain consumption authority

Steps 1-2 of the absorbed blocker. One shared authority answering
"which declarations reference this declaration", built once per run,
cheap point queries thereafter -- the doc standing gate consumes it
now and the PR delivery check consumes it later, neither approximating
it and neither forking it.

v2.lens.witness_cost_locality states in tree that module grain IS the
declared precision frontier and fn-grain reachability does not exist.
That is what this replaces. Module grain is fail-open exactly where
both consumers care: a declaration added to a module that already has
dependents reads as reached while nothing references it.

Design decisions worth the review time:

- Resolution is over the DECLARATION universe (decl_facts), not the
  BINDING universe (SymbolIndex.global_bare). Same shape, different
  populations: the binding index contains parameters and let binders,
  so it would refuse edges the declaration question determines. The
  reconciliation trigger is named -- the namespace lane's containment
  tree makes both one index.

- Consumers are carried as DeclarationIdentity, not DeclarationRef.
  The only composer in tree runs ref -> qualified name; splitting on
  the final dot to manufacture the inverse would be a second naming
  scheme decided by punctuation, and would fabricate a module_path for
  any name the guess did not fit. So the index keys on qualified names
  and the point query composes.

- A subject the fact pack does not declare REFUSES
  (SubjectUniverseAbsent) rather than answering zero consumers. Those
  two states license opposite actions -- the first is a universe hole,
  the second licenses deleting the declaration.

- An ambiguous short name lands in unresolvable and credits NEITHER
  candidate. Undecidable edges are carried, never dropped: a dropped
  edge renders as "no consumers", and the action taken on that answer
  is deletion.

- Self-references are excluded. Every fn names itself at its own
  definition site and host-backed stubs call themselves, so counting
  them would give every declaration a consumer by construction.

The residual imprecision is stated rather than asserted absent: a
local binder colliding with a declaration name produces an edge no
reference justifies. Fail-open, narrow, and it dissolves on the same
containment-tree walk.

6/6 witnesses green by execution, each asserted against its opposite
population. The orphan control is the one the predecessor cannot
reach: fx.m.orphan sits in a module that has dependents.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Classify decl_consumption's construction justification

The floor's naming-hygiene walk refused v2.lens.decl_consumption for
carrying no construction_justification, which is the DESIGN §5/§6 gate
asking why the bad-state class is not made unwritable instead.

Classified WallAfterGrounding, dissolving to SingleAuthority, because
the honest answer is neither of the easy ones. The class -- an authored
declaration no live consumer reaches -- is DECIDABLE given the
declaration universe, so calling it RatchetForever would be the "never"
trap §5 names. But consumption is not a LOCAL property: a declaration
and its consumer can be authored in one commit, so nothing at the
authoring site separates the good case from the bad one and only a
whole-corpus read decides it. A whole-corpus read is a reader.

It becomes a wall on the same trigger the module's other two residues
name -- the containment tree as single naming authority, at which point
a reference is an edge in a structure the compiler already walks and an
unreached declaration is refusable the way an unbound name already is.
One grounding closes the universe fork, the binder-shadowing
imprecision, and this justification together.

6/6 witnesses still green.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Enumerate roots at declaration grain, and type what is not enumerable

Step 3. A root is a declaration nothing needs to reference, so the
purpose law cannot read an unreferenced declaration as dead without
first knowing the root set. Joining an explicit ScheduleWitnessEntry
roster to decl_facts by (rel_path, name) yields real declarations --
legitimate rather than positional citation in disguise, because the
roster natively carries a path and a name and this join CONSUMES the
identity it already has instead of inventing one.

The finding is what is NOT enumerable. Since the discovery flip most
executing witnesses are found by a host-side directory scan
(CiSpec.discovery_scan_dirs) that no .dag fold can read, and
generated-artifact producers are dispatched by a match in
gunbc.generated_artifact_emit rather than listed as declaration names.
So the root set is structurally incomplete here.

decl_consumption_roots therefore returns RootEnumerationPartial and
CANNOT return RootsEnumerated today -- the total arm exists because
the population becomes enumerable once discovery is declared, and it
is deliberately unselectable until then. An empty root set must read
as unknown, never as proof a declaration is unrooted, because that
conclusion licenses deleting live code. Its witness asserts the
partial arm even though every roster entry resolved, which is the
claim that matters: the incompleteness is not about the roster.

7/7 witnesses green by execution.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Enroll decl_consumption in the lens registry as a fact producer

The floor's lens_registry_completeness_holds_live failed: a new module
under v2.lens.* is either an enrolled enforcing lens or a declared
infra row, and mine was neither. That is the inert-lens backstop
working -- coverage by illusion is the tier where machinery exists and
nothing gates on it, so an unenrolled module must red.

Enrolled as infra rather than as a LensIdV0 row, and the distinction
is the real one rather than the convenient one: decl_consumption
produces facts (subject in, consuming declarations out) and carries
no verdict and no remedy. The verdict lives in the documentary
standing fold that consumes it. That is precisely the class
v2.lens.module_impact_query already occupies one grain up, whose row
says the same thing -- a reading with no verdict authority.

The generic infra dissolve_on applies unchanged: the row deletes if
the module ever gains its own verdict authority or leaves src/v2/lens.

Verified by executing the failing witness, not by reasoning about the
roster.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP recut: delete design_truth chain and decl_consumption; bind documentary refs

* wip: single-line data initializers

* wip: logical qualified names; retire the prose-substring control

* wip: escape the interpolation brace exposed by the new import edge

* chore: regenerate drifted generated artifacts (ci auto-heal)

* wip: regenerate DESIGN.md from the ref rows

* Repair the stale citations the recut left behind

The #8066 recut deleted design_truth, design_subject_registry and
design_projection but left four paragraphs citing them, including one
that claimed to name only a single symbol while naming three that no
longer existed. Also homes the three body-lowering DeclarationRef rows
once instead of twice, and drops the out-of-scope five-minute roadmap
ref from the general-body-producer bind.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Strip the conflict markers the merge committed

* chore: regenerate drifted generated artifacts (ci auto-heal)

* Delete the machinery narration rather than replacing stale status with it

Both repairs replaced a stale gate claim with prose describing the
reference mechanism -- the same habit one level up. general-body-producer
said it named no system while naming four, and wave2_prep claimed typed
coverage it does not consume. Deletion is the durable form.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Register the 84 unbound plan documents at subject grain

Each document names one primary_work plus the supporting authorities
whose movement would make its purpose false -- not every system its
prose mentions. Subjects were selected from a measured candidate
manifest and every new reference resolves uniquely through
v2.std.decl_ref_resolution.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Point the floor-materialization ref at the module name, not the file basename

* Drop the bind whose decl_name literal trips the mock-corpus prefilter

precompute_whole_tree_published_mock_keys selects declarer files by
sf.content.contains("PublishedMockCase") and strict-resolves their
closure under dag-only roots. A bind row naming that type as a document
subject put the literal into doc_graph_roots.dag, which imports v2
modules -- unresolvable under dag-only roots, so the precompute errored
and claim_batch exited 1.

The row is removed rather than reworded: that document's subject was a
single weak candidate and asserting a different one to dodge a substring
match would be a workaround. The seed prefilter defect is reported
separately -- its comment claims a false positive can only widen the
closure, but a widened closure needing absent roots fails the build.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Decide mock-corpus declarers structurally, not by substring

precompute_whole_tree_published_mock_keys selected declarer files with
sf.content.contains("PublishedMockCase") and strict-resolved their
closure under dag-only roots. The prefilter's comment argued a false
positive was safe because it 'cannot fabricate a key' -- true about keys,
false about builds: a dag/ module that merely MENTIONS the string and
imports src/v2 has a closure that cannot resolve under those roots, so
the precompute returned Err and the floor refused before running a
witness. Observed by execution on this PR (run 31353487916).

The substring scan stays as a candidate prefilter; the DECISION is now
the exact type-annotation check that already existed downstream, hoisted
ahead of the closure. An unparseable candidate refuses with a located
cause rather than being dropped as clean.

Controls, both executed: genuine declarers still yield 89 operation keys,
and doc_graph_roots -- a v2-importing dag/ module -- now carries a note
that mentions the type without declaring one, so restoring the substring
shortcut reds the floor there first.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant