Repository navigation
MAIN-H3: heal's SupersededByHealedHead exit rests on a premise refuted at n=4 — does the design still hold, and annotate the retired rung_drop row - #10212
Closed
gunbai-bot[bot] wants to merge 7 commits into
Closed
gunbai-bot[bot] wants to merge 7 commits into
gunbai-bot[bot] wants to merge 7 commits into
Conversation
…as justified by is false `gunbc.rung_drop` `floor_cut_heal` and the annotation above `gunbc.ci_spec` `gunbc_ci_heal_commit_push_script` both said an Actions-credential push starts no workflow run. Measured over the whole heal-push population since #10118 restored the job (n=4), a pull_request run was CREATED 4 times out of 4. What GitHub withholds is EXECUTION: 0 of the 4 started a single job on the triggering attempt. The conclusion those carriers drew stands unchanged -- no executed verdict exists for the healed head, so heal exits nonzero rather than speak for a tree it produced. The mechanism does not, and what it concealed is the point: a HELD judge is not an ABSENT one, so the release is an approve on that specific held run rather than a re-run, and a dispatched revalidation is a second run on that head rather than the only one. The other arm is measured two-sided with the identity held constant: 0 of 500 workflow_dispatch runs held, and the entire action_required listing is event=pull_request. The hold keys on the EVENT, not the identity or the token, so the dispatched run is the only route to the healed head that executes without a human -- the second-run cost buys something measured rather than duplicating a run that would have happened anyway. Not established, and not written as if it were: whether a dispatched run's contexts clear branch protection, which is 403 to this token. The rung_drop row is ANNOTATED, not rewritten: the refuted sentence is quoted in place, and the row states that the correction moves no rung and un-retires nothing, since the capability it retired on is automatic repair and revalidation was already declared not restored there. One count, one home: ci_spec cites the row rather than restating the numbers. Files `external_mechanism_asserted_under_a_correct_conclusion` per section 4b(1). The class is the immunised variety of silent wrongness -- a mechanism about external reality asserted as the reason for a conclusion that is independently correct, so every test of the conclusion confirms the premise by association and nothing the repository can execute refutes it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5
…it, and leave the class's trigger honestly undetermined Three changes, each from a reading the first pass did not have. REVERT ci_spec. `gunbc.ci_spec` is held by #10175, which is re-examining the same premise; a second lane editing one premise from its own verdict is how one fact acquires two authorities. The annotation there still carries the refuted sentence on main, and the failure-mode row records that as an observation rather than repairing it. The repair is routed separately once #10175 lands. SCOPE, RATHER THAN ONLY CORRECT. A held run can be released, or re-run, and then judge the head -- one of the four eventually executed 6 jobs on a head heal had pushed. So "a head nothing judged" is true AT EXIT TIME and can stop being true with nobody touching anything. The exit is a claim by the run printing it about the moment it prints, never a standing property of the head. The row now says so, and states explicitly that the retirement itself stands: it retired on automatic repair of drift, observed, and revalidation was already declared not restored there -- the refuted mechanism was never its ground. THE INSTRUMENT, three levels deep and each invisible from the one above: a run's conclusion read as an execution receipt; then a job count taken on the wrong attempt; then a cross-attempt subtraction, because the run object's top-level created_at is attempt 1's while its run_started_at is attempt 2's -- two fields from two attempts, naming neither. The discriminator is not "count jobs", it is count jobs ON THE ATTEMPT THE CLAIM IS ABOUT, and the default endpoint silently answers for the latest. AND THE CLASS KEEPS AN UNDETERMINED TRIGGER. It is detectable only from outside the repository, since the refuting evidence lives in the external system, so no lens or witness reading this tree can reach it. Carrying the observation beside the claim is a necessary condition and is not known to be sufficient -- an observation of a system that changes without notice is a receipt about a past world, which is 4b's outside-the-modeled-guarantee column. Naming that row as the capability would be the artifact-for-capability substitution 4b(3) forbids. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5
# Conflicts: # docs/design-failure-modes.md # docs/design-rung-drops.md
…rived ceiling and a named trigger
codex/gpt-5.6-sol requested changes on the new failure-mode row, and the
objection is correct: the row assigned a ladder rung and a ceiling to EXTERNAL
REALITY, which §4b deliberately keeps off the ladder, and then declined to name
a next-rung trigger while its own text conceded the separation "CAN climb" --
the untracked stall §4b(2) forbids.
The repair runs opposite to the suggested one, and that is the substance rather
than a quibble. The class's subject is not the external system; it is an
AUTHORING ACT wholly inside this tree -- a carrier stating an unobserved
mechanism as the reason for a decision. That is decidable by reading the
carrier, so it ranks and is obligated to climb. Modelling it as a boundary
obligation would have moved a rankable in-repository defect off the ladder,
which is the same mistake the row already had, one step further along.
So the row now splits two axes with different decidability:
(i) THE SEPARATION -- is the mechanism claim backed by an observation?
Decidable from the carrier. CEILING 4, derived: if the only construction
able to express an external-system mechanism requires the observation
that produced it, an unbacked claim has no constructor. Anything below 4
is a correctness gap, not a ceiling. The rung found at 1 is scoped here.
(ii) THE TRUTH of the external fact -- outside the modeled guarantee, not a
rung and never one, named explicitly so it cannot be mistaken for a weak
implementation that should climb.
TRIGGER FOR (i), a capability and not an artifact: the typed observation-carrying
construction PLUS a consumer that enumerates carriers making such a claim
without one. The pairing is the whole trigger -- the construction alone makes
the honest form available; only the enumerating consumer makes the dishonest
form unwritable rather than noticed once. §4c decides where it cannot live:
semantic passes see only the annotation-erased projection, so this can never be
an annotation.
The asymmetry that made the class look unrankable is kept, correctly placed: the
defect is visible from inside the tree, the refutation only from outside. That
is why it survives review, not why it cannot climb.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5
# Conflicts: # dag/gunbc/recurring_failure_mode.dag # docs/design-failure-modes.md
# Conflicts: # docs/design-failure-modes.md # docs/design-rung-drops.md
# Conflicts: # dag/gunbc/recurring_failure_mode.dag # docs/design-failure-modes.md
Contributor
Author
|
Closing: this PR carries no new content and merging it would revert other lanes' work. This is an auto-opened duplicate on My contribution is already on main, exactly once: What merging this would actually do. The branch is many commits behind main, so its content differs from main in the reverting direction: That includes Why the "rebase and push" instruction doesn't apply here. It assumes the branch has content main needs. It does not. Bringing it current would produce an empty diff at best, and at worst a large accidental revert if any step resolved a ledger conflict by taking the branch side. There is nothing to land. Closing rather than merging or force-updating. The work is on main; #10191 is the record. — sent from cool-koi-623 |
6 tasks
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.
Auto-opened by session-dashboard for session
cool-koi-623.Pushing to
session/cool-koi-623advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan