Repository navigation
Bind the insertion dissolution to the arm that landed: main carries a false machine-consumed fact - #9377
Merged
Conversation
… four claims #9359 falsified gunbc#9359 added NodeOccurrenceIdentity's OccurrenceProjected arm. Four claims in v2.workflow.legacy_binding_projection and its witness were true against the base that module was authored on and became false the moment #9359 merged. One is not prose. THE MACHINE-CONSUMED ONE, and it is live on main as of 96e8b62. legacy_binding_projection_insertion_dissolution is an UnboundDissolution whose description reads "unemittable while ... NodeOccurrenceIdentity carries no arm for a projector-created node's cause", in the same tree where that arm is declared. std.dissolution dissolution_status matches over DissolutionCondition, so this is a false FACT rather than a false comment: the debt reports UNBOUND while its binding declaration sits in the tree. It becomes bound_dissolution(decl_ref(std.occurrence_identity, OccurrenceProjected)). The row's own annotation named this trigger -- "the condition binds in the same change that rebases onto the arm, at which point the ref is verifiable at the moment it is written." The intent was to bind it inside #9359; the merge won the race by four minutes. Nothing about the argument weakened: the declaration is on main, so the citation resolves and the wall accepts it, where on the old base it would have been the §3 fabricated- citation class. THE THREE PROSE CLAIMS, corrected rather than deleted: - the module preamble asserting NodeOccurrenceIdentity "has two arms", that caused_by appears zero times across dag/std and src/v2/std, and that insertions are blocked on a named work item "until it lands" - the annotation saying the bound form's declaration "does not exist on this base" - the witness function name a_declared_insertion_refuses_because_no_carrier_can_express_ its_cause -> ..._because_this_projector_is_not_wired_to_the_cause_arm. A reader trusts a name without reading the body, so a false name outranks a true comment above it. WHAT DID NOT CHANGE: the refusal. ProjectionInsertionUnrepresentable still fires and the witness still passes. What the module cannot do is no longer EXPRESS an insertion's cause but EMIT one -- nothing there allocates a projected occurrence and names what caused it. That wiring, and the flip of the refusal to a regression control, belong to the change that does the wiring and are not claimed here. Found by crisp-crab-430, who checked #9359 against the merged tree rather than its diff -- the only read that reaches what a change makes false in files it does not touch. Verified: 4106 files parse-clean, citation debt unchanged at 42 with the new ref present, so it resolves rather than joining the debt roster; projection witnesses 8/8 PASS. No consumer asserts this row's unboundness, so nothing depended on the false state. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…tribution, and an instrument that measured a closed absence Both are the additive-invalidation class landing inside the repair for it, found by crisp-crab-430 reading the head rather than the diff. THE MERGE ATTRIBUTION. The annotation read "gunbc#9359 is that change. It lands the third arm and rebases this file onto it in one commit." That is not what happened: #9359 merged without the rebase, and this PR is the change that rebases the module's claims and authors the citation. The argument was never wrong -- the citation IS written at the first moment it can be written honestly -- but naming one commit for two independently landed facts erases the interval, and the interval is the interesting part: between them, main carried a dissolution row asserting the absence of an arm declared in the same tree. THE INSTRUMENT. The annotation closed by naming "grep caused_by across dag/std and src/v2/std" as the instrument for the claim, which was right when it was written and avoided transcribing a zero. But it measured an ABSENCE, and this PR's subject is the change that ended it: caused_by now returns hits in both trees, so a reader running the named instrument gets a nonzero answer and cannot distinguish a wrong annotation from a mis-run. It now names the facts that are TRUE -- NodeOccurrenceIdentity's OccurrenceProjected arm, and insertion_provenance_entry deriving ProjectedAsInsertion from it. That is a refinement of the standing name-the-instrument rule rather than an exception to it. The rule was derived against transcribed OUTPUT and implicitly assumes an instrument is stable under time; an instrument pointed at an absence is stable only until someone closes the absence, and then it inverts silently. The historical zero belongs in the PR record, where it dates itself. Annotation-only: no dissolution row, no executing code, no witness touched. Verified: 4106 files parse-clean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
gunbc#9359 added
NodeOccurrenceIdentity'sOccurrenceProjectedarm. Four claims inv2.workflow.legacy_binding_projectionand its witness were true against the base that module was authored on, and became false the moment #9359 merged. One of them is not prose.Main is currently wrong, and this is the disclosure
legacy_binding_projection_insertion_dissolutionis anUnboundDissolutionwhose description reads "ProjectedAsInsertion is unemittable while std.occurrence_identity NodeOccurrenceIdentity carries no arm for a projector-created node's cause" — in the same tree where that arm is declared.std.dissolutiondissolution_statusmatches overDissolutionCondition, so this is a false machine-consumed fact, not a false comment: the debt reportsDissolutionUnboundwhile its own binding declaration sits in the tree. A dissolution carrier exists precisely so that nobody has to notice this by hand, so the one interval where it was wrong belongs in the record rather than in someone's memory.Interval: from
96e8b623dd(#9359 merged 2026-08-27T00:33:23Z) until this PR merges. The correction was written and green four minutes after that merge and was intended to land inside #9359 — a DO NOT MERGE comment went up about a minute before the merge and did not win the race. No consumer asserts this row's unboundness, so nothing depended on the false state; the exposure is that a reader or adissolution_statusfold gets a wrong answer about one debt row.The fix
The row's own annotation named this trigger: "The condition binds in the same change that rebases onto the arm, at which point the ref is verifiable at the moment it is written." Merging #9359 did not weaken that argument — it removed the last reason to defer. The declaration is on main, so the citation resolves and the wall accepts it, where on the old base authoring it would have been the §3 fabricated-citation class.
The three prose claims, corrected rather than deleted
NodeOccurrenceIdentity"has two arms", thatcaused_byappears zero times acrossdag/stdandsrc/v2/std, and that insertions are blocked on a named work item "until it lands"a_declared_insertion_refuses_because_no_carrier_can_express_its_cause→..._because_this_projector_is_not_wired_to_the_cause_arm. A reader trusts a name without reading the body, so a false name outranks a true comment sitting directly above it.What did not change
The refusal.
ProjectionInsertionUnrepresentablestill fires and the witness still passes. What the module cannot do is no longer express an insertion's cause but emit one — nothing there allocates a projected occurrence and names what caused it. That wiring, and the flip of the refusal to a regression control, belong to the change that does the wiring and are not claimed here.Evidence
decl_refpresent, so it resolves rather than joining the debt rosterFound by crisp-crab-430, who checked #9359 against the merged tree rather than its diff — the only read that reaches what a change makes false in files it does not touch.