From 9adb1ce50bbfeadce3b696288f46391ef78d9846 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 3 Sep 2026 04:03:18 +0000 Subject: [PATCH 1/3] heal: the SupersededByHealedHead exit is right and the mechanism it was 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 Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 --- dag/gunbc/ci/ci_spec.dag | 29 ++++++++++++++++++++++------ dag/gunbc/recurring_failure_mode.dag | 3 +++ dag/gunbc/rung_drop.dag | 2 +- docs/design-failure-modes.md | 2 ++ docs/design-rung-drops.md | 2 +- 5 files changed, 30 insertions(+), 8 deletions(-) diff --git a/dag/gunbc/ci/ci_spec.dag b/dag/gunbc/ci/ci_spec.dag index 2efabf5f529..611a17bc180 100644 --- a/dag/gunbc/ci/ci_spec.dag +++ b/dag/gunbc/ci/ci_spec.dag @@ -1768,12 +1768,29 @@ fn ci_heal_shell_lines() -> List { } // THE PUSHED HEAD IS NOT REVALIDATED BY THIS JOB, AND THE JOB SAYS SO RATHER THAN IMPLYING IT. -// A push made with the Actions job credential does not start a new workflow run -- GitHub -// suppresses that edge to stop a job from triggering itself -- so after a successful heal the -// pull request's checks describe PRIOR_HEAD and no longer describe the branch. That is a real -// gap and the arm below is the fail-closed answer to it: the job prints SupersededByHealedHead -// naming both revisions and EXITS NONZERO, so the healed head arrives with a red job whose text -// says why, and a human or a re-run decides. It does not exit zero on a head nothing has judged. +// CORRECTED 2026-09-03: THE ARM BELOW IS RIGHT AND THE MECHANISM THIS ANNOTATION GAVE FOR IT WAS +// NOT. It said a push made with the Actions job credential does not start a workflow run, because +// GitHub suppresses that edge to stop a job from triggering itself. A pull_request run IS created +// for the healed head. What GitHub withholds is EXECUTION: the created run is held, concluding +// without starting a single job. The population, the per-run receipts and the re-derivation recipe +// are carried once, in gunbc.rung_drop floor_cut_heal, and are deliberately not restated here -- +// two homes for one count is the fork this repository keeps paying for. +// +// SO AFTER A SUCCESSFUL HEAL the pull request's EXECUTED checks still describe PRIOR_HEAD and no +// longer describe the branch. That is a real gap and the arm below is the fail-closed answer to +// it: the job prints SupersededByHealedHead naming both revisions and EXITS NONZERO, so the healed +// head arrives with a red job whose text says why. It does not exit zero on a head nothing has +// judged. +// +// TWO CONSEQUENCES THE OLD MECHANISM CONCEALED, because a HELD judge is not an ABSENT one. The +// human action that releases the healed head is an approve on THAT SPECIFIC HELD RUN, not a re-run +// of some other run -- re-running a run that was never the held one leaves the gate where it was. +// And a dispatched revalidation is a SECOND run on that head rather than the only one, so it costs +// a whole additional run and its check runs land beside the held run's on one commit, where a +// reader keyed by check NAME cannot separate them. That cost buys something measured rather than +// duplicating what would have happened anyway: the hold discriminates on the EVENT and not on the +// identity or the token, so a dispatched run is the only route to the healed head that executes +// without a human -- again, receipts in gunbc.rung_drop floor_cut_heal. // // WHAT WOULD CLOSE IT, named as a capability rather than as an artifact: a workflow_dispatch // entry point on this same workflow carrying the healed sha as a declared input, which every diff --git a/dag/gunbc/recurring_failure_mode.dag b/dag/gunbc/recurring_failure_mode.dag index a76e23bad26..2c085c074dd 100644 --- a/dag/gunbc/recurring_failure_mode.dag +++ b/dag/gunbc/recurring_failure_mode.dag @@ -263,6 +263,8 @@ data realization_arms_diverge_on_whether_the_program_refuses: RecurringFailureMo data declared_return_disagrees_with_the_generic_it_returns: RecurringFailureMode = RecurringFailureMode { identity: "declared_return_disagrees_with_the_generic_it_returns" as NonEmptyStr, authored: "**a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: \"cannot apply Lt to Record and Int\" }`, while the same call over a zero-byte primitive returns `\"?\"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `\"?\"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation.", evidence: [] } data non_execution_undifferentiated_by_what_it_silenced: RecurringFailureMode = RecurringFailureMode { identity: "non_execution_undifferentiated_by_what_it_silenced" as NonEmptyStr, authored: "**a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row.", evidence: [] } +data external_mechanism_asserted_under_a_correct_conclusion: RecurringFailureMode = RecurringFailureMode { identity: "external_mechanism_asserted_under_a_correct_conclusion" as NonEmptyStr, authored: "**a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. NEXT TRIGGER, NAMED AS THE CAPABILITY: a carrier that states a fact about an external system carries the OBSERVATION that produced it as a typed row -- the query, the population, the date -- so that an unobserved mechanism is structurally distinguishable from an observed one and can be listed. `extdeps` already owns the shape for cited upstream facts and this class is what a boundary-observation row would be for. Until that exists this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names.", evidence: [] } + data recurring_failure_mode_roster: List = [ censored_estimator_drops_its_own_tail, selection_view_read_as_population, @@ -331,4 +333,5 @@ data recurring_failure_mode_roster: List = [ realization_arms_diverge_on_whether_the_program_refuses, declared_return_disagrees_with_the_generic_it_returns, non_execution_undifferentiated_by_what_it_silenced, + external_mechanism_asserted_under_a_correct_conclusion, ] diff --git a/dag/gunbc/rung_drop.dag b/dag/gunbc/rung_drop.dag index d9bc8327738..b5d878eea46 100644 --- a/dag/gunbc/rung_drop.dag +++ b/dag/gunbc/rung_drop.dag @@ -102,7 +102,7 @@ data direct_call_arg_seam_v2_exemption: RungDrop = RungDrop { data floor_cost_claim_qualification_unavailable: RungDrop = RungDrop { identity: "floor_cost_claim_qualification_unavailable" as NonEmptyStr, subject: "Per-claim cost qualification is unavailable at the subject grain the gate consumes", declared: "2026-09-01", standing: Standing, authored: "Required floor cost — **RUNG DROP, DECLARED (2026-09-01).** SUBJECT: per-claim cost qualification at the subject grain the gate consumes. THIS ROW NAMES NO CAUSE, AND ITS EARLIER NAME DID -- it was `floor_cost_contention_verdict`, which asserted contention as the mechanism when the evidence establishes only that the charge is not a stable property of the claim. Renamed rather than reworded, because a row identity that carries a refuted attribution is cited onward as if the attribution were the finding. WHAT IS LOST: an attempt's CPU duration cannot be read as an invariant property of the witness, nor as proof of a witness-owned regression. `required_floor_claim_cpu_safety_limit_ms` is a cpu-ms literal compared against a measurement that is not a stable property of the claim. WHAT THE CHARGE IS MADE OF, MEASURED RATHER THAN ATTRIBUTED, and this is the whole of what this row asserts about mechanism: it contains a CLOSURE-LEVEL COMPONENT insensitive to the claim's own assertion work, and an EXECUTION-POSITION-SENSITIVE COMPONENT whose cause and bound are NOT established. Neither component is named as contention, memory pressure or warm-up here, because no evidence in hand separates those, and NO BOUND HAS BEEN ESTABLISHED -- which is a different statement from an unbounded cause and must not be read as one. THE MEASUREMENT IS NOT WRONG AND THIS ROW DOES NOT SAY SO: it is a VALID observation of THIS EXECUTION ATTEMPT. What it is not is a stable observation of the claim as an isolated subject, and only the second reading is what a cost verdict needs. WHAT REMAINS, AND STAYS REQUIRED: the 500ms attempt-safety stop, and fail-closed treatment of a required claim that produced no verdict. The position-sensitive component disqualifies the deadline as an INTRINSIC CLAIM-COST VERDICT; it does not disqualify it as a REQUIRED ATTEMPT-SAFETY AND VERDICT-AVAILABILITY criterion. Both terminal arms stay required reds and are distinct: an interrupted attempt means the required claim never produced a semantic verdict, and a completed-past-limit attempt means it crossed the declared safety envelope. Neither proves the witness intrinsically costs more than the limit, that it regressed, that it owns the observed excess, or that it belongs in permanent cost debt. False refusals are an AVAILABILITY loss that fails closed, and removing the deadline would let genuinely runaway evaluation consume the executor without bound. PREVIOUS RUNG: none for environment-independent claim-cost qualification -- that guarantee was never held, and saying it was would be inventing a rung to drop from. Mechanically preventable remains TRUE and undropped for attempt safety. TEMPORARY RUNG: claim-cost qualification UNAVAILABLE; verdict availability environment-sensitive; acceptance still fail-closed. REASON, and the three negative results that make this a capability claim rather than a shrug. (1) THE BASIS IS ALREADY CPU BY DECLARATION: `required_floor_cost_basis` returns `CpuCost` because these claims execute Hermetic, so 'judge cpu rather than wall' is DONE and what remains is cpu-time variance itself. (2) THE OBVIOUS CALIBRATOR IS REFUTED BY MEASUREMENT, and this is the sentence that stops the trigger being discharged by pointing at what we already measure: THE PREPARATION WARM PHASES ARE NOT A CALIBRATOR. Across main and two attempts of one identical tree, `pool-root-index-warm` measured 693 / 727 / 596 cpu-ms and `languages-consumer-census-warm` measured 858 / 606 / 531, so on the attempt whose CLAIMS ran hottest the census phase ran COLDER than main's. They do not track claim inflation. (3) NO CALIBRATION CONCEPT EXISTS IN THE REPOSITORY AT ALL. Normalizing by a quantity that does not track the machine would produce a threshold that LOOKS principled and is not, which is strictly worse than the honest literal. POPULATION -- THE CLOSED SUBJECT UNIVERSE IS NOT A THRESHOLD-SELECTED SET, AND THIS ROW SAID OTHERWISE FOR TWO REVISIONS. The universe is EVERY REQUIRED IDENTITY FOR WHICH THE CPU DEADLINE IS ARMED. That is closed, decidable from the run's own plan, and it does not move with anyone's measurement. WHY THE THRESHOLD SET IS NOT THAT UNIVERSE: the position-sensitive term has no established bound, so NO lower threshold can prove the rows beneath it unaffected. A set selected by 'measured cpu at or above N' is a VIEW whose membership is a property of the MEASUREMENT rather than of the subject, and letting a decidable admission predicate's output stand in for the class's population joins two different objects by an assumption. The predicate was the right answer to a censored-parameter refusal and the wrong answer to 'what is the population'. THE THRESHOLD SET SURVIVES AS AN EXPOSED ATTENTION SUBSET, which is what it is good for: prioritising optimisation and isolation work. Admission is measured cpu at or above the attention constant -- 280ms against the 500ms ceiling, the ceiling over the largest inflation floor observed to date -- and the constant is spelled ONCE here, with every later reference in this row naming it rather than repeating the digits, because a constant that has already moved twice in one day reforks the row on its next revision if it is spelled in three places. THAT SINGLE-SPELLING DISCIPLINE IS PROSE AND NOT STRUCTURE: `RungDrop` carries no numeric field, so nothing refuses a future revision that updates one mention and not another. That missing field is this discipline's next rung. THE ATTENTION CONSTANT'S OWN DERIVATION AND REVISION CONDITION: it is the ceiling over an inflation FLOOR of 1.777, measured by identity join -- `v2.test.execution.emit_host_meet_join_equals_eval.emit_host_meet_wrong_fixture_refuses_holds` measured 501 cpu-ms on one attempt and 282 on a re-run of THE SAME TREE with nothing changed. A floor is not the inflation, so the constant MUST BE RE-DERIVED THE MOMENT A LARGER FLOOR IS MEASURED. Its predecessor was falsified within the hour for exactly this reason: sized at 400 against a floor of 1.196, it EXCLUDED the one row this class has been observed to trip on the completed-past-limit arm, and an admission rule that omits a known member is wrong at its own grain. TWO OBJECTS, ONE MONOTONE AND ONE NOT, AND THIS ROW PREVIOUSLY CONFLATED THEM: the EVIDENCE FLOOR is monotone -- the largest observed inflation floor can only rise, so the constant derived from it can only fall. THE MEMBERSHIP SET IS NOT MONOTONE: individual identities enter and leave the attention subset as their measured attempt costs vary, which is exactly what makes it a view rather than a population. Monotonicity of the first gives nothing about the second. ON THE NAMED RUN (gunbc#9840 head 85c4a307, required-witnesses-floor, second attempt, 3381 executed rows) the attention subset holds 53 identities across 21 modules, the largest groups being `test.claim.compiler_frontend_program_status_witness` (9), `v2.test.execution.emit_host_meet_join_equals_eval` (4), `v2.test.emit.rust_body_add_emit` (4) and `v2.test.emit.rust_binop_emit` (4). THE SUBSET IS A MANUAL DERIVATION AND NOT AN EXPOSED RUN PRODUCT, AND AN EARLIER REVISION OF THIS ROW OVERCLAIMED IT. The enumeration above was computed BY HAND by reading a run's uploaded `required_floor_claim_cost.tsv` and filtering on the attention constant. NO MODELED FIELD, FUNCTION OR REPORT PRODUCES IT: the constant lives only in this prose, `RungDrop` carries no numeric field to hold it, and nothing consumes it -- so saying the artifact 'reports the subset' asserted an executable relationship that does not exist. WHAT WOULD MAKE IT A PRODUCER, and it is a carrier gap rather than a missing script: the constant modeled as a declaration, and the per-claim cost artifact modeled as data a function can read, at which point the subset is a fold and this paragraph becomes its projection. Neither exists today, and a hand-run filter described as a run product is the specification-without-execution DESIGN section 5 names -- which is why this row now says which of the two it is. THE CONSTANT SITS ON THE STEEPEST PART OF THE COST CURVE and must not be read as a measured threshold: 12 rows reach 400, 16 reach 350, 43 reach 300, 50 reach 290 and 53 reach 280 -- seven rows arrive in a 10ms interval, and 1388 rows measure zero. WHAT LANDED TOWARD THE TRIGGER, AND WHY THIS ROW IS STILL STANDING. The deterministic-work-measure arm now EXISTS AS AN INSTRUMENT and does NOT yet exist AS A BASIS, and those are different things. `v1.interpreter` counts one evaluator step per `eval_expr` entry, UNCONDITIONALLY -- not under the profiling flag, because a measure available only in an instrumented envelope is not available in the envelopes this row is about -- and `run_claim_measured` takes the per-claim delta and nets stored shared-artifact fills out of it by exactly the rule the CPU clock is netted by. WHAT THAT NETTING BUYS, STATED AT THE WIDTH THE EVIDENCE SUPPORTS AND NOT WIDER: the net count is not determined by WHICH TESTED CLAIM PAYS THE MODELED SHARED-ARTIFACT FILL. That is ONE modeled path. It is NOT independence from arbitrary corpus execution order, which is unmeasured and which this row's own missing-item (b) below still names as owed; an earlier revision of this sentence claimed the broad property and contradicted that boundary paragraph two sentences later. It reaches `PerformanceReceipt.eval_steps`, the `[over-cost]` line, and an `eval_steps` column in the per-claim cost artifact. ITS EVIDENCE IS EXECUTED AND DISCRIMINATING, and it is enrolled rather than described: `evaluator_step_work_measure_tests` asserts EXACT equality of the count across two genuinely different envelopes -- one arm with the CPU deadline ARMED, which takes a different path through `eval_expr`, under a co-tenant thread spinning for the whole evaluation -- beside a work control at a different fixture size, so a counter frozen at any constant including zero fails; and a netting arm in which the claim that PAYS a shared fill and the claim that reads it warm are asserted to carry the SAME marginal count while their RAW counts are asserted to differ by more than a factor of ten, so the netted equality is not two identical numbers compared. NOTHING COMPARES THE COLUMN AGAINST A LINE, AND THAT IS DELIBERATE RATHER THAN UNFINISHED. The trigger asks for a claim-owned cost BASIS; a column no verdict reads is a measurement and not a basis, and calling this row retired on the strength of a published column would be exactly the rung inflation 4b(1) forbids. TWO THINGS ARE STILL MISSING and neither is bought by more prose. (a) A STEP-DENOMINATED LINE, which cannot be sized from this tree today because no run has yet published the distribution that the column now makes publishable -- and inventing one would be the same looks-principled-and-is-not threshold this row already refuses on the calibration arm. (b) THE CROSS-ENVELOPE A/B ON THE SHARED RUNNER AT CORPUS GRAIN: an identity join of `eval_steps` across two attempts of one identical tree, where the cpu column moves and this one must not. Until (b) is measured the invariance claim is grounded at FIXTURE grain and nowhere wider, which is the honest reading of what landed. THE CPU DEADLINE IS UNCHANGED BY ALL OF THIS: it is still the armed enforcement clock, still denominated in cpu-ms, and the new column changes no threshold and no verdict. RESTORATION TRIGGER, A CONJUNCTION AND NOT A MENU. An earlier revision offered three ALTERNATIVE arms -- isolation, a deterministic work measure, or a calibrated relative basis -- and that disjunction is refuted by the composition measured above: isolation can stabilise the WRONG SUBJECT, a deterministic measure can count the wrong subject EXACTLY, and calibration can normalise a WRONGLY ALLOCATED charge. Each arm answers a different one of three independent questions, so any one alone leaves the other two open. ALL THREE MUST HOLD. (i) CHARGE SUBJECT ALIGNED: the marginal claim work is separated from the closure-level component, OR the gate is honestly rehomed to closure identity and stops claiming to judge claims. (ii) BASIS INVARIANT OR BOUNDED across execution POSITION and envelope, demonstrated by EXACT IDENTITY JOINS rather than by aggregates -- a median over a corpus cannot see a windowed effect, which is the specific error that produced this row's revision. (iii) POLICY LINE GROUNDED over the independently defined FULL population and CONSUMED AT THE SAME SUBJECT GRAIN it was derived at. A basis satisfying (ii) while the gate consumes it at a grain it was not derived for is the same defect wearing better numbers. TWO CONTROLS THAT WOULD DISCHARGE (i) AND (ii), named so the next lane does not have to re-derive them. POSITION CONTROL: the same exact tree and population, a deterministic ORDER ROTATION carrying the same identities through both the early inflated region and the flat tail, cpu allowed to move, and net eval_steps required to remain IDENTICAL by identity join. CHARGE-SUBJECT CONTROL: two claims in ONE closure with materially different assertion work -- do marginal eval_steps discriminate them? The ordinary larger-fixture-takes-more-steps control proves the counter is ALIVE and does NOT prove the steps belong to the claim rather than to its closure, and this row previously leaned on the first as if it answered the second. IF THE SAME-CLOSURE DIFFERENTIAL IS CONSTANT, THE ANSWER IS NOT A STEP THRESHOLD AT CLAIM GRAIN: rehome the policy to closure identity or subtract the closure component explicitly. AND DO NOT TRANSLATE THE 500 CPU-MS LINE INTO STEPS USING THE MEASURED CPU DISTRIBUTION, which carries the position-sensitive component this row exists to declare. A SEPARATE CAPABILITY BOUND, RECORDED HERE AND EXPLICITLY NOT THIS ROW'S CAUSE: a shared artifact fill paid inside a claim's measured window before preemption bounds what any deadline mechanism can promise about attribution. PAYER TRANSFER IS REFUTED FOR THIS INCIDENT -- the red run's own `[floor-shared-fill]` ledger carries no `paid_by` line naming the module that tripped, the whole module shifted uniformly by 8 to 11 percent rather than one row taking a lump, and the rows that crossed sat mid-pack on the green attempt. It is a bound on the mechanism, not an explanation of these observations, and it is not this row's population producer. RAISING THE CEILING DOES NOT RETIRE THIS ROW AND IS NOT PROPOSED: 'the comparison does not qualify the claim' and 'the threshold is too low' are different claims, and only the first is recorded here. NOT PROPOSED EITHER: re-running an undecided row until it answers is retry-until-green -- fail-open wearing a fail-closed label -- admissible only as a counted, visible mitigation carrying this row's trigger as its dissolution condition. RECEIPT, 2026-09-02, AND THE MITIGATION THE SENTENCE ABOVE ADMITS CONDITIONALLY IS HEREBY MADE VISIBLE RATHER THAN LEFT IMPLICIT. Rerolling a refused required floor job has been in continuous informal use across this board today under a bounded rule -- at most one reroll per head per signature, and only where the run reported `failed=0` with the refusal carried entirely by this row's two arms. Bounded is better than retry-until-green, and it was still NOT the admitted arm, because nothing enumerated the instances and nothing carried this row's trigger as their dissolution condition. This paragraph is that enumeration. DISSOLUTION CONDITION: this row's own RESTORATION TRIGGER and nothing short of it -- a claim-owned cost basis whose value is invariant, or bounded by construction, across the admitted execution envelopes. When that lands, the reroll has no subject and this paragraph goes with it. INSTANCES, CITED BY RUN ID SO EACH IS REACHABLE AND FALSIFIABLE RATHER THAN TALLIED: gunbc#9984 run 33604337589 attempts 1 and 2 on head 9b00e24f592 (refuse then pass; `interrupted_before_verdict` 4 then 0, `completed_over_cost_requirement` 3 then 0, `planned=executed=3486` and `failed=0` on both); gunbc#10022 run 33615900632 attempts 1 and 2 on head c2c1db141a (refuse then pass, two undecided rows in `test.claim.self_host_compile_phase_live_gate_witness`); gunbc#9954 commit 53088562e30 (`interrupted_before_verdict=15`, `completed_over_cost_requirement=0`, `failed=0` -- the largest single observation, and purely the non-verdict arm); gunbc#10044 run 33618811753 attempts 1 and 2 on head 2d42cca4b94 by session eager-ferret-714's lane (refuse THEN REFUSE on one tree with different accounting -- `interrupted` 2 then 4, `over_cost` 0 then 2); and gunbc#10044 run 33619277245 attempts 1 and 2 on head 0e9b1518b7b (refuse then refuse; `interrupted` 5 then 2, `over_cost` 4 then 0, `planned=executed=3477` and `failed=0` on both); gunbc#10047 run 33622971872 attempt 2 on head 1aa6d8f41dc (attempt 1 refused at 502ms on `v2.test.emit.rust_binop_emit.rust_binop_producer_emit_sub_holds`, a module carrying four identities in this row's own attention subset -- so the roster PREDICTED the row that blocked that PR, which is a stronger receipt than a fresh observation); gunbc#9986 at f5fca17678f (`planned=executed=3503`, `failed=0`, `interrupted_before_verdict=2` in `test.claim.compiler_frontend_program_status_witness` and `test.claim.self_host_compile_phase_frontier_witness` -- NEITHER in the live-gate family, on a head that had ALREADY taken 2d76d9ccb33, which is what establishes the arm is not confined to a repairable family); and gunbc#10044 run 33628404336 attempts 1 and 2 on head 03780b8c76c, floor jobs 100219422472 and 100256793010 (REFUSE THEN REFUSE at ONE ROW EACH, `failed=0` and `planned=executed=3486` on both, `interrupted_cpu_deadline=1` -- but attempt 1's row was `v2.test.emit.produced_decl_two_target` and attempt 2's was `v2.test.execution.emit_host_module_equals_eval`, a DIFFERENT identity at the same count). THAT LAST PAIR IS SUGGESTIVE AND DOES NOT SETTLE IT ALONE, WHICH IS WORTH SAYING BECAUSE THE OVERSTATED VERSION WAS WRITTEN HERE FIRST: two draws showing DIFFERENT identities at n=1 per side are equally consistent with a FIXED set of marginal rows sitting so close to the deadline that ordering decides which one crosses. Identity change alone does not discriminate those two explanations. WHAT DISCRIMINATES IS THAT THE COUNT MOVES AS WELL AS THE MEMBERSHIP, across the instances above taken jointly: 4 then 0, 5 then 2, 1 then 1, 2 then 4, and 15. A fixed marginal set would have to explain a count ranging over 0, 1, 2, 4, 5 and 15 AND the membership changing; a population redrawn per attempt explains both, and near-threshold ordering explains only the second. So the redraw reading is CORROBORATED BY THE INSTANCES JOINTLY rather than established by any one pair -- and the load-bearing consequence survives either way, because on both readings no enumeration of the expensive claims can be the population, family-by-family cost repair lowers incidence without bounding the class, and a green reroll is not evidence the refused row was wrong. ; and gunbc#9986 run 33655367446 attempts 1 and 2 on head 2ee252f3339 (REFUSE THEN CLEAN, the mitigation's only successful roll recorded here: attempt 1 `interrupted_before_verdict=15` all `cpu_deadline`, attempt 2 `interrupted_before_verdict=0`, with `planned=executed=terminal=3504` and `failed=0` on BOTH -- and every one of the 15 sat in `test.claim.self_host_compile_phase_frontier_witness` or `test.claim.self_host_compile_phase_live_gate_witness`, neither of which that change touched. 15 equals the largest prior observation (gunbc#9954) on an unrelated tree, and the previous head of this same PR showed 2, so the amplitude moved by an order of magnitude across a main merge alone). THIS INSTANCE WAS ENUMERATED BY THE LANDING MANAGER RATHER THAN THE AUTHORING LANE, deliberately: this row is one very long line, so each lane appending its own instance produces a diff the review surface sizes as a one-line wording tweak -- the class filed as `gunbc.recurring_failure_mode` `salience_instrument_blind_to_the_record_it_sizes`, whose specimen is an earlier edit to THIS row. Batching the appends does not reduce the bytes a reviewer must read; it reduces the number of times that misreading is invited. RE-DERIVE ANY OF THESE WITH `gh api repos/OWNER/REPO/actions/jobs/JOB/logs --allow-escape-sequences` AND WITH NOTHING ELSE. Measured on the first pair above: `gh run view --job --log` answers an ATTEMPT-1 job id with ATTEMPT 2's CONTENT -- banner timestamp and counters both attempt 2's -- so an auditor re-deriving a two-attempt specimen with it obtains IDENTICAL content on both sides, observes no disagreement, and reports these enumerated instances as fabricated. The instrument fails in the direction that discredits a true finding, and without the escape-sequences flag the same endpoint writes zero bytes instead. Anyone checking these numbers must be holding the right instrument before disagreeing with them. NO MODELED PRODUCER COUNTS THESE, AND THAT MISSING COUNTER IS THIS PARAGRAPH'S OWN GAP: `RungDrop` carries no field for a mitigation instance, nothing folds the run ids, and a hand-kept TALLY is deliberately absent here because this row has already had to retract one hand-derivation described as a run product. A count with no producer is stale at the next roll and re-derivable by nobody; a run id is reachable by anyone. Whoever wants the number counts the citations. WHAT THE INSTANCES ESTABLISH BEYOND THE MITIGATION ITSELF: the two arms vary INDEPENDENTLY and in both directions on fixed bytes, and a refusal can repeat while disagreeing with itself about which rows were undecided -- so a reroll is not a coin flip against a fixed population but a fresh draw of the population. ONE FINER OBSERVATION THAN THIS ROW PREVIOUSLY SUPPORTED, from the last instance: after the live-gate cost repairs in 2d76d9ccb33 (gunbc#10038), `test.claim.self_host_compile_phase_live_gate_witness` was ABSENT from attempt 1 and BACK in attempt 2 of ONE head. A cost repair lowering a family's incidence is the expected reading; that the family is intermittent WITHIN a single head's attempts is stronger, and it is the sharpest available statement that a cost repair moves incidence without touching the mechanism at the boundary. The conflation of a computed non-verdict with a refusal at the AGGREGATE boundary is a separate class and is filed as `gunbc.recurring_failure_mode` `non_verdict_disposition_surfaces_as_refusal`, which cites this row for the cost half rather than re-deriving it." } data spark_role_scoped_retirement_production_root: RungDrop = RungDrop { identity: "spark_role_scoped_retirement_production_root" as NonEmptyStr, subject: "Spark serving role-scoped retirement evidence at the production plan root", declared: "2026-09-02", standing: Standing, authored: "**AN OPERATOR DECISION REMOVED A BEHAVIOUR'S ONLY SUBJECT, AND THIS ROW IS THAT DECLARATION (2026-09-02).** `gunbc.spark.cell_role` assigned srv6 to `SparkTrainingCell`, and the operator withdrew that dedication as premature -- 'i wouldn't dedicate a whole node for any task - just have it converge and serve whatever task we converge it to' -- so the production roster now holds ZERO training cells. Three claims in `test.claim.spark.spark_cell_role_retirement_witness_test` entered through `fleet_converge_plan_artifact`, the root the converge actuator itself walks, and each needed a production host holding that role to have a subject at all: `w_the_production_artifact_plans_four_retirements_for_the_training_cell`, `w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell`, and `w_the_production_retirement_touches_no_baseline_address`. They are DELETED rather than left silently red, because a claim whose subject no longer exists is not a failing test, and leaving it to fail would have made an operator's decision look like a regression. **PREVIOUS RUNG: mechanically preventable** -- the training arm's four retirement rows and the serving arm's zero rows were both exercised through the production root, so a planner regression that pointed `spark_serving_full_membership_plan` back at the unscoped desired members went red there. **TEMPORARY RUNG: mitigatable** -- both arms are still exercised, but only at `spark_serving_role_scoped_desired_members_in` over an authored fixture roster (`w_the_planner_scopes_desired_state_by_role`), which is a real production function and is NOT the path the converge actuator calls; the same PR added `spark_cell_role_in` and that `_in` planner variant precisely so an arm's evidence stops depending on which machines are currently assigned what. **REASON:** operator decision, recorded with its basis at `gunbc.spark.cell_role` `spark_cell_role_assignment_basis`; role is converged desired state rather than a node dedication. **POPULATION, BOUNDED:** the training arm of Spark serving role scoping and the retirement rows it produces, AS REACHED THROUGH `fleet_converge_plan_artifact`. The serving arm, the no-role refusal, the reconcile, the freeze and the apply are unaffected and their production-root claims remain enrolled. **RESTORATION TRIGGER, NAMING THE CAPABILITY:** a roster-parameterized plan artifact -- the assignment roster threaded from `fleet_converge_plan_artifact` down to `spark_serving_role_scoped_desired_members_in` -- SUFFICIENT FOR a witness to drive the production root over an authored roster and read back the four retirement rows with no production host holding `SparkTrainingCell`. Half that capability exists today: both `_in` functions take the roster; what is missing is the threading through the generic artifact entry point. **RESTORING A TRAINING CELL TO THE PRODUCTION ROSTER DOES NOT RETIRE THIS DROP** -- that would re-create the coupling between an arm's evidence and the current assignment, which is the defect this row exists to record, and it is exactly the trigger-names-less-than-the-capability failure §4b(3) warns about." } -data floor_cut_heal: RungDrop = RungDrop { identity: "floor_cut_heal" as NonEmptyStr, subject: "Heal job for generated artifacts", declared: "2026-09-01", standing: Retired { trigger_fired: "2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one." as NonEmptyStr }, authored: "**RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } +data floor_cut_heal: RungDrop = RungDrop { identity: "floor_cut_heal" as NonEmptyStr, subject: "Heal job for generated artifacts", declared: "2026-09-01", standing: Retired { trigger_fired: "2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. The two that ever executed did so on attempt 2, after a human acted. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. THIS CORRECTION DOES NOT MOVE THE ROW'S RUNG AND DOES NOT UN-RETIRE IT: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one." as NonEmptyStr }, authored: "**RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } data floor_cut_effect_gates: RungDrop = RungDrop { identity: "floor_cut_effect_gates" as NonEmptyStr, subject: "Six of the seven effect gates (one restored)", declared: "2026-09-01", standing: Standing, authored: "**SIX OF THE SEVEN EFFECT GATES ARE UNGUARDED AND THE SEVENTH IS BACK, AND THE FRACTION IS STATED BECAUSE SAYING `THE EFFECT GATES` WHERE ONE OF SEVEN IS LIVE IS THE OVERSTATEMENT THIS LEDGER KEEPS PAYING FOR (2026-09-01).** Split out of `floor_cut`. THE SEVEN, from that row's own loss clause: compile-clean, generated-artifact drift, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. DISCHARGED, 1 of 7: generated-artifact drift, restored by gunbc#9415 as the required `generated-artifact` phase adjudicating every member of `committed_generated_artifacts` through `gunbc.generated_artifact_emit` `generated_artifact_body_for_path`. It is named here as DONE rather than deleted from the list, because a population that shrinks silently cannot be checked. OUTSTANDING, 6 of 7: compile-clean, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. PREVIOUS RUNG: 2 (mechanically preventable) for each -- a required gate blocked the merge. TEMPORARY RUNG: 0 for the six; not `1`, because these are not mitigated failures but UNOBSERVED ones -- the class is outside the modeled guarantee at the merge boundary until its gate returns. REASON: the 2026-08-15 floor cut deleted the wrapper carrying all seven obligations. BOUNDED POPULATION: the six named gates, enumerated above; the roster is closed and is not `whatever the plan lists`. RESTORATION TRIGGER, PER GATE AND NOT FOR THE SET: this row retires only when EACH of the six has a required-run consumer that refuses a merge on its own violation, each with a discriminating RED executed on the real acceptance path. Six retirements, one row, and the row states its own remaining fraction whenever it is read. WHAT DOES NOT RETIRE THIS ROW: the `generated-artifact` phase being live, which is the one already discharged; a lens that computes any of the six without gating, which is the inert tier DESIGN section 6 names; or a gate landed with no authored RED, which is a wall nobody has seen fire. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index d482fc3b1fc..44c640184fd 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -71,6 +71,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `realization_arms_diverge_on_whether_the_program_refuses` - `declared_return_disagrees_with_the_generic_it_returns` - `non_execution_undifferentiated_by_what_it_silenced` +- `external_mechanism_asserted_under_a_correct_conclusion` --- @@ -153,3 +154,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - realization arms diverge on WHETHER THE PROGRAM REFUSES (two realizations of one accepted program agree on the returned value and disagree on whether an evaluation-time refusal fires, because the fact that decides it -- evaluation order -- is modeled nowhere and each arm improvises). INVALID STATE: a connective whose operand evaluation strategy is unmodeled, realized strictly by one arm and lazily by another. gunbc v1 today: v1.compiler.interpreter eval_expr_inner's ExprBinOp arm evaluates BOTH operands through `?` before dispatching. eval_binop DOES carry And and Or arms -- `Value::Bool(left.is_truthy() && right.is_truthy())` -- and they are irrelevant to this class and worth naming precisely because they look like the repair: they run on operands ALREADY EVALUATED at the call site, so their Rust && is over two bools and short-circuits nothing. A reader grepping eval_binop for And finds a hit and concludes the case is handled, while std.operator_realization maps BinOp::And and BinOp::Or to OperatorRealization::HostOperator, rendered as Rust && and ||, which short-circuit. HARM: the guard idiom -- a cheap precondition guarding an expression that can refuse -- means two different programs. The interpreter runs the guarded expression when the guard is FALSE and refuses; emitted Rust never runs it and returns a value. Silent in both directions and invisible to any oracle comparing returned values on guard-true inputs, which is every value-comparison oracle we have. DISCRIMINATING RED, executed 2026-09-02, not asserted: `fn guarded_division(n: Int) -> Bool { n != 0 && (100 / n) > 1 }`. At n=0 the interpreter refuses DivisionByZero and the emitted Rust returns false; at n=5 both return true. Division by zero was chosen deliberately because BOTH realizations abort identically IF the expression is evaluated, so evaluation order is the only variable in the pair. CONTROLS, because a false from a harness that cannot observe an abort is a vacuous green: the same function with the guard forced true and n=0 PANICKED with 'attempt to divide by zero' and was caught and reported, so the harness can see the abort; and the guard-true positive control agrees across both arms. HONESTY BOUND ON THE EVIDENCE: the interpreter arm ran on the real acceptance path via `gunbc run`; the emitted arm executed the emitted function bodies extracted VERBATIM into a rustc harness, not the whole emitted crate. WHY IT IS NOT refusal_deferred_to_emitted_runtime: that class is a compiler writing a refusal construct INTO the artifact while reporting success. Here no refusal is written anywhere and the compile is honest; the two arms simply disagree at run time about whether one fires. Same neighbourhood, different invalid state, different repair. THE POPULATION IS SURVIVORSHIP-FILTERED AND A GREP UNDERSTATES IT BY CONSTRUCTION. The interpreter is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the refusal while authoring and rewrote it -- most likely into a nested if or match. So the sites matching `cheap_guard && expensive` are the SURVIVORS, the cases where the right operand happens not to refuse; the cases carrying the correctness consequence were already edited away. A LOW COUNT IS THEREFORE NOT EVIDENCE THE CLASS IS MINOR AND MUST NOT BE REPORTED AS ONE. The honest population is sites where an author WANTED the guard idiom, which lives in the rewrites and is not reachable by the same needle. RECOGNITION RULE, stated to generalise past this operator: wherever a construct is realized independently by the interpreter and by an emission target, ask what fact decides its behaviour and where that fact is DECLARED. If the deciding fact is absent from the authority both arms are supposed to consult, the arms are not implementing one semantics, they are each inventing one, and agreement on the values you happened to test is not evidence they agree. The tell is a realization shape -- HostOperator -- that names WHO evaluates without naming WHAT is evaluated. RUNG: mitigatable at best, and only because one arm refuses loudly; against a source-to-emission path this is silent wrongness, which DESIGN section 4b places outside the ladder. NEXT-RUNG TRIGGER, named as a capability and not an artifact: EVALUATION ORDER MODELED AS A PROPERTY OF A CONNECTIVE IN THE .dag AUTHORITY AND CONSULTED BY BOTH REALIZATIONS -- sufficient for the interpreter's binop arm to derive its strictness from the same row the emitter derives its rendering from, so that a connective's operand strategy cannot be stated twice or left unstated. A grep across dag/, src/v2/ and src/v1/*.dag on 2026-09-02 found no such fact: every short-circuit hit is prose in a comment or a witness name. NOT REPAIRED HERE: changing the interpreter to short-circuit is a corpus-wide evaluation-semantics change and needs its own subject, population and review; filing it against the missing carrier is the point of this row. - **a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: "cannot apply Lt to Record and Int" }`, while the same call over a zero-byte primitive returns `"?"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `"?"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation. - **a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row. +- **a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. NEXT TRIGGER, NAMED AS THE CAPABILITY: a carrier that states a fact about an external system carries the OBSERVATION that produced it as a typed row -- the query, the population, the date -- so that an unobserved mechanism is structurally distinguishable from an observed one and can be listed. `extdeps` already owns the shape for cited upstream facts and this class is what a boundary-observation row would be for. Until that exists this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names. diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index fbe05177319..2078637bad0 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -10,7 +10,7 @@ Each row declares a safety guarantee that was lowered: what stood before, what s ### Heal job for generated artifacts — declared 2026-09-01 · RETIRED -**RETIRED — TRIGGER FIRED.** 2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one. +**RETIRED — TRIGGER FIRED.** 2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. The two that ever executed did so on attempt 2, after a human acted. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. THIS CORRECTION DOES NOT MOVE THE ROW'S RUNG AND DOES NOT UN-RETIRE IT: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one. **RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids. From 8dc4c1484e03ad1e416422206dfefb8e442eff1b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 3 Sep 2026 04:14:02 +0000 Subject: [PATCH 2/3] Scope the corrected clause to exit time, revert the fenced ci_spec edit, 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 Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 --- dag/gunbc/ci/ci_spec.dag | 29 ++++++---------------------- dag/gunbc/recurring_failure_mode.dag | 2 +- dag/gunbc/rung_drop.dag | 2 +- docs/design-failure-modes.md | 2 +- docs/design-rung-drops.md | 2 +- 5 files changed, 10 insertions(+), 27 deletions(-) diff --git a/dag/gunbc/ci/ci_spec.dag b/dag/gunbc/ci/ci_spec.dag index 611a17bc180..2efabf5f529 100644 --- a/dag/gunbc/ci/ci_spec.dag +++ b/dag/gunbc/ci/ci_spec.dag @@ -1768,29 +1768,12 @@ fn ci_heal_shell_lines() -> List { } // THE PUSHED HEAD IS NOT REVALIDATED BY THIS JOB, AND THE JOB SAYS SO RATHER THAN IMPLYING IT. -// CORRECTED 2026-09-03: THE ARM BELOW IS RIGHT AND THE MECHANISM THIS ANNOTATION GAVE FOR IT WAS -// NOT. It said a push made with the Actions job credential does not start a workflow run, because -// GitHub suppresses that edge to stop a job from triggering itself. A pull_request run IS created -// for the healed head. What GitHub withholds is EXECUTION: the created run is held, concluding -// without starting a single job. The population, the per-run receipts and the re-derivation recipe -// are carried once, in gunbc.rung_drop floor_cut_heal, and are deliberately not restated here -- -// two homes for one count is the fork this repository keeps paying for. -// -// SO AFTER A SUCCESSFUL HEAL the pull request's EXECUTED checks still describe PRIOR_HEAD and no -// longer describe the branch. That is a real gap and the arm below is the fail-closed answer to -// it: the job prints SupersededByHealedHead naming both revisions and EXITS NONZERO, so the healed -// head arrives with a red job whose text says why. It does not exit zero on a head nothing has -// judged. -// -// TWO CONSEQUENCES THE OLD MECHANISM CONCEALED, because a HELD judge is not an ABSENT one. The -// human action that releases the healed head is an approve on THAT SPECIFIC HELD RUN, not a re-run -// of some other run -- re-running a run that was never the held one leaves the gate where it was. -// And a dispatched revalidation is a SECOND run on that head rather than the only one, so it costs -// a whole additional run and its check runs land beside the held run's on one commit, where a -// reader keyed by check NAME cannot separate them. That cost buys something measured rather than -// duplicating what would have happened anyway: the hold discriminates on the EVENT and not on the -// identity or the token, so a dispatched run is the only route to the healed head that executes -// without a human -- again, receipts in gunbc.rung_drop floor_cut_heal. +// A push made with the Actions job credential does not start a new workflow run -- GitHub +// suppresses that edge to stop a job from triggering itself -- so after a successful heal the +// pull request's checks describe PRIOR_HEAD and no longer describe the branch. That is a real +// gap and the arm below is the fail-closed answer to it: the job prints SupersededByHealedHead +// naming both revisions and EXITS NONZERO, so the healed head arrives with a red job whose text +// says why, and a human or a re-run decides. It does not exit zero on a head nothing has judged. // // WHAT WOULD CLOSE IT, named as a capability rather than as an artifact: a workflow_dispatch // entry point on this same workflow carrying the healed sha as a declared input, which every diff --git a/dag/gunbc/recurring_failure_mode.dag b/dag/gunbc/recurring_failure_mode.dag index 2c085c074dd..786676b1398 100644 --- a/dag/gunbc/recurring_failure_mode.dag +++ b/dag/gunbc/recurring_failure_mode.dag @@ -263,7 +263,7 @@ data realization_arms_diverge_on_whether_the_program_refuses: RecurringFailureMo data declared_return_disagrees_with_the_generic_it_returns: RecurringFailureMode = RecurringFailureMode { identity: "declared_return_disagrees_with_the_generic_it_returns" as NonEmptyStr, authored: "**a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: \"cannot apply Lt to Record and Int\" }`, while the same call over a zero-byte primitive returns `\"?\"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `\"?\"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation.", evidence: [] } data non_execution_undifferentiated_by_what_it_silenced: RecurringFailureMode = RecurringFailureMode { identity: "non_execution_undifferentiated_by_what_it_silenced" as NonEmptyStr, authored: "**a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row.", evidence: [] } -data external_mechanism_asserted_under_a_correct_conclusion: RecurringFailureMode = RecurringFailureMode { identity: "external_mechanism_asserted_under_a_correct_conclusion" as NonEmptyStr, authored: "**a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. NEXT TRIGGER, NAMED AS THE CAPABILITY: a carrier that states a fact about an external system carries the OBSERVATION that produced it as a typed row -- the query, the population, the date -- so that an unobserved mechanism is structurally distinguishable from an observed one and can be listed. `extdeps` already owns the shape for cited upstream facts and this class is what a boundary-observation row would be for. Until that exists this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names.", evidence: [] } +data external_mechanism_asserted_under_a_correct_conclusion: RecurringFailureMode = RecurringFailureMode { identity: "external_mechanism_asserted_under_a_correct_conclusion" as NonEmptyStr, authored: "**a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. THIS CLASS IS DETECTABLE ONLY FROM OUTSIDE THE REPOSITORY, and that is the whole difficulty rather than an aside: the refuting evidence lives in the external system, so no lens, gate or witness reading this tree can reach it, and the class is invisible to every mechanism the repository owns. NEXT TRIGGER, and it is honestly UNDETERMINED rather than named, which is the fail-closed way to leave it. The capability question is what would have to be OBSERVABLE for a mechanism claim about an external system to be executable evidence rather than an assertion -- and that is not settled here. What can be said now: a carrier that states such a fact should carry the OBSERVATION that produced it -- the query, the population, the date -- so an unobserved mechanism is structurally distinguishable from an observed one and can be listed; `extdeps` already owns the shape for cited upstream facts. That is a necessary condition and it is NOT KNOWN to be sufficient, because a recorded observation of a system that can change its behaviour without notice is a receipt about a past world, which is section 4b's outside-the-modeled-guarantee column and not a rung. A TRIGGER NAMING THAT ROW AS THE CAPABILITY WOULD THEREFORE BE THE ARTIFACT-FOR-CAPABILITY SUBSTITUTION section 4b(3) FORBIDS, satisfied while the class stays alive. Until the question is settled this row is a reading discipline and citing it as coverage is rung inflation.", evidence: [] } data recurring_failure_mode_roster: List = [ censored_estimator_drops_its_own_tail, diff --git a/dag/gunbc/rung_drop.dag b/dag/gunbc/rung_drop.dag index b5d878eea46..ddccac90175 100644 --- a/dag/gunbc/rung_drop.dag +++ b/dag/gunbc/rung_drop.dag @@ -102,7 +102,7 @@ data direct_call_arg_seam_v2_exemption: RungDrop = RungDrop { data floor_cost_claim_qualification_unavailable: RungDrop = RungDrop { identity: "floor_cost_claim_qualification_unavailable" as NonEmptyStr, subject: "Per-claim cost qualification is unavailable at the subject grain the gate consumes", declared: "2026-09-01", standing: Standing, authored: "Required floor cost — **RUNG DROP, DECLARED (2026-09-01).** SUBJECT: per-claim cost qualification at the subject grain the gate consumes. THIS ROW NAMES NO CAUSE, AND ITS EARLIER NAME DID -- it was `floor_cost_contention_verdict`, which asserted contention as the mechanism when the evidence establishes only that the charge is not a stable property of the claim. Renamed rather than reworded, because a row identity that carries a refuted attribution is cited onward as if the attribution were the finding. WHAT IS LOST: an attempt's CPU duration cannot be read as an invariant property of the witness, nor as proof of a witness-owned regression. `required_floor_claim_cpu_safety_limit_ms` is a cpu-ms literal compared against a measurement that is not a stable property of the claim. WHAT THE CHARGE IS MADE OF, MEASURED RATHER THAN ATTRIBUTED, and this is the whole of what this row asserts about mechanism: it contains a CLOSURE-LEVEL COMPONENT insensitive to the claim's own assertion work, and an EXECUTION-POSITION-SENSITIVE COMPONENT whose cause and bound are NOT established. Neither component is named as contention, memory pressure or warm-up here, because no evidence in hand separates those, and NO BOUND HAS BEEN ESTABLISHED -- which is a different statement from an unbounded cause and must not be read as one. THE MEASUREMENT IS NOT WRONG AND THIS ROW DOES NOT SAY SO: it is a VALID observation of THIS EXECUTION ATTEMPT. What it is not is a stable observation of the claim as an isolated subject, and only the second reading is what a cost verdict needs. WHAT REMAINS, AND STAYS REQUIRED: the 500ms attempt-safety stop, and fail-closed treatment of a required claim that produced no verdict. The position-sensitive component disqualifies the deadline as an INTRINSIC CLAIM-COST VERDICT; it does not disqualify it as a REQUIRED ATTEMPT-SAFETY AND VERDICT-AVAILABILITY criterion. Both terminal arms stay required reds and are distinct: an interrupted attempt means the required claim never produced a semantic verdict, and a completed-past-limit attempt means it crossed the declared safety envelope. Neither proves the witness intrinsically costs more than the limit, that it regressed, that it owns the observed excess, or that it belongs in permanent cost debt. False refusals are an AVAILABILITY loss that fails closed, and removing the deadline would let genuinely runaway evaluation consume the executor without bound. PREVIOUS RUNG: none for environment-independent claim-cost qualification -- that guarantee was never held, and saying it was would be inventing a rung to drop from. Mechanically preventable remains TRUE and undropped for attempt safety. TEMPORARY RUNG: claim-cost qualification UNAVAILABLE; verdict availability environment-sensitive; acceptance still fail-closed. REASON, and the three negative results that make this a capability claim rather than a shrug. (1) THE BASIS IS ALREADY CPU BY DECLARATION: `required_floor_cost_basis` returns `CpuCost` because these claims execute Hermetic, so 'judge cpu rather than wall' is DONE and what remains is cpu-time variance itself. (2) THE OBVIOUS CALIBRATOR IS REFUTED BY MEASUREMENT, and this is the sentence that stops the trigger being discharged by pointing at what we already measure: THE PREPARATION WARM PHASES ARE NOT A CALIBRATOR. Across main and two attempts of one identical tree, `pool-root-index-warm` measured 693 / 727 / 596 cpu-ms and `languages-consumer-census-warm` measured 858 / 606 / 531, so on the attempt whose CLAIMS ran hottest the census phase ran COLDER than main's. They do not track claim inflation. (3) NO CALIBRATION CONCEPT EXISTS IN THE REPOSITORY AT ALL. Normalizing by a quantity that does not track the machine would produce a threshold that LOOKS principled and is not, which is strictly worse than the honest literal. POPULATION -- THE CLOSED SUBJECT UNIVERSE IS NOT A THRESHOLD-SELECTED SET, AND THIS ROW SAID OTHERWISE FOR TWO REVISIONS. The universe is EVERY REQUIRED IDENTITY FOR WHICH THE CPU DEADLINE IS ARMED. That is closed, decidable from the run's own plan, and it does not move with anyone's measurement. WHY THE THRESHOLD SET IS NOT THAT UNIVERSE: the position-sensitive term has no established bound, so NO lower threshold can prove the rows beneath it unaffected. A set selected by 'measured cpu at or above N' is a VIEW whose membership is a property of the MEASUREMENT rather than of the subject, and letting a decidable admission predicate's output stand in for the class's population joins two different objects by an assumption. The predicate was the right answer to a censored-parameter refusal and the wrong answer to 'what is the population'. THE THRESHOLD SET SURVIVES AS AN EXPOSED ATTENTION SUBSET, which is what it is good for: prioritising optimisation and isolation work. Admission is measured cpu at or above the attention constant -- 280ms against the 500ms ceiling, the ceiling over the largest inflation floor observed to date -- and the constant is spelled ONCE here, with every later reference in this row naming it rather than repeating the digits, because a constant that has already moved twice in one day reforks the row on its next revision if it is spelled in three places. THAT SINGLE-SPELLING DISCIPLINE IS PROSE AND NOT STRUCTURE: `RungDrop` carries no numeric field, so nothing refuses a future revision that updates one mention and not another. That missing field is this discipline's next rung. THE ATTENTION CONSTANT'S OWN DERIVATION AND REVISION CONDITION: it is the ceiling over an inflation FLOOR of 1.777, measured by identity join -- `v2.test.execution.emit_host_meet_join_equals_eval.emit_host_meet_wrong_fixture_refuses_holds` measured 501 cpu-ms on one attempt and 282 on a re-run of THE SAME TREE with nothing changed. A floor is not the inflation, so the constant MUST BE RE-DERIVED THE MOMENT A LARGER FLOOR IS MEASURED. Its predecessor was falsified within the hour for exactly this reason: sized at 400 against a floor of 1.196, it EXCLUDED the one row this class has been observed to trip on the completed-past-limit arm, and an admission rule that omits a known member is wrong at its own grain. TWO OBJECTS, ONE MONOTONE AND ONE NOT, AND THIS ROW PREVIOUSLY CONFLATED THEM: the EVIDENCE FLOOR is monotone -- the largest observed inflation floor can only rise, so the constant derived from it can only fall. THE MEMBERSHIP SET IS NOT MONOTONE: individual identities enter and leave the attention subset as their measured attempt costs vary, which is exactly what makes it a view rather than a population. Monotonicity of the first gives nothing about the second. ON THE NAMED RUN (gunbc#9840 head 85c4a307, required-witnesses-floor, second attempt, 3381 executed rows) the attention subset holds 53 identities across 21 modules, the largest groups being `test.claim.compiler_frontend_program_status_witness` (9), `v2.test.execution.emit_host_meet_join_equals_eval` (4), `v2.test.emit.rust_body_add_emit` (4) and `v2.test.emit.rust_binop_emit` (4). THE SUBSET IS A MANUAL DERIVATION AND NOT AN EXPOSED RUN PRODUCT, AND AN EARLIER REVISION OF THIS ROW OVERCLAIMED IT. The enumeration above was computed BY HAND by reading a run's uploaded `required_floor_claim_cost.tsv` and filtering on the attention constant. NO MODELED FIELD, FUNCTION OR REPORT PRODUCES IT: the constant lives only in this prose, `RungDrop` carries no numeric field to hold it, and nothing consumes it -- so saying the artifact 'reports the subset' asserted an executable relationship that does not exist. WHAT WOULD MAKE IT A PRODUCER, and it is a carrier gap rather than a missing script: the constant modeled as a declaration, and the per-claim cost artifact modeled as data a function can read, at which point the subset is a fold and this paragraph becomes its projection. Neither exists today, and a hand-run filter described as a run product is the specification-without-execution DESIGN section 5 names -- which is why this row now says which of the two it is. THE CONSTANT SITS ON THE STEEPEST PART OF THE COST CURVE and must not be read as a measured threshold: 12 rows reach 400, 16 reach 350, 43 reach 300, 50 reach 290 and 53 reach 280 -- seven rows arrive in a 10ms interval, and 1388 rows measure zero. WHAT LANDED TOWARD THE TRIGGER, AND WHY THIS ROW IS STILL STANDING. The deterministic-work-measure arm now EXISTS AS AN INSTRUMENT and does NOT yet exist AS A BASIS, and those are different things. `v1.interpreter` counts one evaluator step per `eval_expr` entry, UNCONDITIONALLY -- not under the profiling flag, because a measure available only in an instrumented envelope is not available in the envelopes this row is about -- and `run_claim_measured` takes the per-claim delta and nets stored shared-artifact fills out of it by exactly the rule the CPU clock is netted by. WHAT THAT NETTING BUYS, STATED AT THE WIDTH THE EVIDENCE SUPPORTS AND NOT WIDER: the net count is not determined by WHICH TESTED CLAIM PAYS THE MODELED SHARED-ARTIFACT FILL. That is ONE modeled path. It is NOT independence from arbitrary corpus execution order, which is unmeasured and which this row's own missing-item (b) below still names as owed; an earlier revision of this sentence claimed the broad property and contradicted that boundary paragraph two sentences later. It reaches `PerformanceReceipt.eval_steps`, the `[over-cost]` line, and an `eval_steps` column in the per-claim cost artifact. ITS EVIDENCE IS EXECUTED AND DISCRIMINATING, and it is enrolled rather than described: `evaluator_step_work_measure_tests` asserts EXACT equality of the count across two genuinely different envelopes -- one arm with the CPU deadline ARMED, which takes a different path through `eval_expr`, under a co-tenant thread spinning for the whole evaluation -- beside a work control at a different fixture size, so a counter frozen at any constant including zero fails; and a netting arm in which the claim that PAYS a shared fill and the claim that reads it warm are asserted to carry the SAME marginal count while their RAW counts are asserted to differ by more than a factor of ten, so the netted equality is not two identical numbers compared. NOTHING COMPARES THE COLUMN AGAINST A LINE, AND THAT IS DELIBERATE RATHER THAN UNFINISHED. The trigger asks for a claim-owned cost BASIS; a column no verdict reads is a measurement and not a basis, and calling this row retired on the strength of a published column would be exactly the rung inflation 4b(1) forbids. TWO THINGS ARE STILL MISSING and neither is bought by more prose. (a) A STEP-DENOMINATED LINE, which cannot be sized from this tree today because no run has yet published the distribution that the column now makes publishable -- and inventing one would be the same looks-principled-and-is-not threshold this row already refuses on the calibration arm. (b) THE CROSS-ENVELOPE A/B ON THE SHARED RUNNER AT CORPUS GRAIN: an identity join of `eval_steps` across two attempts of one identical tree, where the cpu column moves and this one must not. Until (b) is measured the invariance claim is grounded at FIXTURE grain and nowhere wider, which is the honest reading of what landed. THE CPU DEADLINE IS UNCHANGED BY ALL OF THIS: it is still the armed enforcement clock, still denominated in cpu-ms, and the new column changes no threshold and no verdict. RESTORATION TRIGGER, A CONJUNCTION AND NOT A MENU. An earlier revision offered three ALTERNATIVE arms -- isolation, a deterministic work measure, or a calibrated relative basis -- and that disjunction is refuted by the composition measured above: isolation can stabilise the WRONG SUBJECT, a deterministic measure can count the wrong subject EXACTLY, and calibration can normalise a WRONGLY ALLOCATED charge. Each arm answers a different one of three independent questions, so any one alone leaves the other two open. ALL THREE MUST HOLD. (i) CHARGE SUBJECT ALIGNED: the marginal claim work is separated from the closure-level component, OR the gate is honestly rehomed to closure identity and stops claiming to judge claims. (ii) BASIS INVARIANT OR BOUNDED across execution POSITION and envelope, demonstrated by EXACT IDENTITY JOINS rather than by aggregates -- a median over a corpus cannot see a windowed effect, which is the specific error that produced this row's revision. (iii) POLICY LINE GROUNDED over the independently defined FULL population and CONSUMED AT THE SAME SUBJECT GRAIN it was derived at. A basis satisfying (ii) while the gate consumes it at a grain it was not derived for is the same defect wearing better numbers. TWO CONTROLS THAT WOULD DISCHARGE (i) AND (ii), named so the next lane does not have to re-derive them. POSITION CONTROL: the same exact tree and population, a deterministic ORDER ROTATION carrying the same identities through both the early inflated region and the flat tail, cpu allowed to move, and net eval_steps required to remain IDENTICAL by identity join. CHARGE-SUBJECT CONTROL: two claims in ONE closure with materially different assertion work -- do marginal eval_steps discriminate them? The ordinary larger-fixture-takes-more-steps control proves the counter is ALIVE and does NOT prove the steps belong to the claim rather than to its closure, and this row previously leaned on the first as if it answered the second. IF THE SAME-CLOSURE DIFFERENTIAL IS CONSTANT, THE ANSWER IS NOT A STEP THRESHOLD AT CLAIM GRAIN: rehome the policy to closure identity or subtract the closure component explicitly. AND DO NOT TRANSLATE THE 500 CPU-MS LINE INTO STEPS USING THE MEASURED CPU DISTRIBUTION, which carries the position-sensitive component this row exists to declare. A SEPARATE CAPABILITY BOUND, RECORDED HERE AND EXPLICITLY NOT THIS ROW'S CAUSE: a shared artifact fill paid inside a claim's measured window before preemption bounds what any deadline mechanism can promise about attribution. PAYER TRANSFER IS REFUTED FOR THIS INCIDENT -- the red run's own `[floor-shared-fill]` ledger carries no `paid_by` line naming the module that tripped, the whole module shifted uniformly by 8 to 11 percent rather than one row taking a lump, and the rows that crossed sat mid-pack on the green attempt. It is a bound on the mechanism, not an explanation of these observations, and it is not this row's population producer. RAISING THE CEILING DOES NOT RETIRE THIS ROW AND IS NOT PROPOSED: 'the comparison does not qualify the claim' and 'the threshold is too low' are different claims, and only the first is recorded here. NOT PROPOSED EITHER: re-running an undecided row until it answers is retry-until-green -- fail-open wearing a fail-closed label -- admissible only as a counted, visible mitigation carrying this row's trigger as its dissolution condition. RECEIPT, 2026-09-02, AND THE MITIGATION THE SENTENCE ABOVE ADMITS CONDITIONALLY IS HEREBY MADE VISIBLE RATHER THAN LEFT IMPLICIT. Rerolling a refused required floor job has been in continuous informal use across this board today under a bounded rule -- at most one reroll per head per signature, and only where the run reported `failed=0` with the refusal carried entirely by this row's two arms. Bounded is better than retry-until-green, and it was still NOT the admitted arm, because nothing enumerated the instances and nothing carried this row's trigger as their dissolution condition. This paragraph is that enumeration. DISSOLUTION CONDITION: this row's own RESTORATION TRIGGER and nothing short of it -- a claim-owned cost basis whose value is invariant, or bounded by construction, across the admitted execution envelopes. When that lands, the reroll has no subject and this paragraph goes with it. INSTANCES, CITED BY RUN ID SO EACH IS REACHABLE AND FALSIFIABLE RATHER THAN TALLIED: gunbc#9984 run 33604337589 attempts 1 and 2 on head 9b00e24f592 (refuse then pass; `interrupted_before_verdict` 4 then 0, `completed_over_cost_requirement` 3 then 0, `planned=executed=3486` and `failed=0` on both); gunbc#10022 run 33615900632 attempts 1 and 2 on head c2c1db141a (refuse then pass, two undecided rows in `test.claim.self_host_compile_phase_live_gate_witness`); gunbc#9954 commit 53088562e30 (`interrupted_before_verdict=15`, `completed_over_cost_requirement=0`, `failed=0` -- the largest single observation, and purely the non-verdict arm); gunbc#10044 run 33618811753 attempts 1 and 2 on head 2d42cca4b94 by session eager-ferret-714's lane (refuse THEN REFUSE on one tree with different accounting -- `interrupted` 2 then 4, `over_cost` 0 then 2); and gunbc#10044 run 33619277245 attempts 1 and 2 on head 0e9b1518b7b (refuse then refuse; `interrupted` 5 then 2, `over_cost` 4 then 0, `planned=executed=3477` and `failed=0` on both); gunbc#10047 run 33622971872 attempt 2 on head 1aa6d8f41dc (attempt 1 refused at 502ms on `v2.test.emit.rust_binop_emit.rust_binop_producer_emit_sub_holds`, a module carrying four identities in this row's own attention subset -- so the roster PREDICTED the row that blocked that PR, which is a stronger receipt than a fresh observation); gunbc#9986 at f5fca17678f (`planned=executed=3503`, `failed=0`, `interrupted_before_verdict=2` in `test.claim.compiler_frontend_program_status_witness` and `test.claim.self_host_compile_phase_frontier_witness` -- NEITHER in the live-gate family, on a head that had ALREADY taken 2d76d9ccb33, which is what establishes the arm is not confined to a repairable family); and gunbc#10044 run 33628404336 attempts 1 and 2 on head 03780b8c76c, floor jobs 100219422472 and 100256793010 (REFUSE THEN REFUSE at ONE ROW EACH, `failed=0` and `planned=executed=3486` on both, `interrupted_cpu_deadline=1` -- but attempt 1's row was `v2.test.emit.produced_decl_two_target` and attempt 2's was `v2.test.execution.emit_host_module_equals_eval`, a DIFFERENT identity at the same count). THAT LAST PAIR IS SUGGESTIVE AND DOES NOT SETTLE IT ALONE, WHICH IS WORTH SAYING BECAUSE THE OVERSTATED VERSION WAS WRITTEN HERE FIRST: two draws showing DIFFERENT identities at n=1 per side are equally consistent with a FIXED set of marginal rows sitting so close to the deadline that ordering decides which one crosses. Identity change alone does not discriminate those two explanations. WHAT DISCRIMINATES IS THAT THE COUNT MOVES AS WELL AS THE MEMBERSHIP, across the instances above taken jointly: 4 then 0, 5 then 2, 1 then 1, 2 then 4, and 15. A fixed marginal set would have to explain a count ranging over 0, 1, 2, 4, 5 and 15 AND the membership changing; a population redrawn per attempt explains both, and near-threshold ordering explains only the second. So the redraw reading is CORROBORATED BY THE INSTANCES JOINTLY rather than established by any one pair -- and the load-bearing consequence survives either way, because on both readings no enumeration of the expensive claims can be the population, family-by-family cost repair lowers incidence without bounding the class, and a green reroll is not evidence the refused row was wrong. ; and gunbc#9986 run 33655367446 attempts 1 and 2 on head 2ee252f3339 (REFUSE THEN CLEAN, the mitigation's only successful roll recorded here: attempt 1 `interrupted_before_verdict=15` all `cpu_deadline`, attempt 2 `interrupted_before_verdict=0`, with `planned=executed=terminal=3504` and `failed=0` on BOTH -- and every one of the 15 sat in `test.claim.self_host_compile_phase_frontier_witness` or `test.claim.self_host_compile_phase_live_gate_witness`, neither of which that change touched. 15 equals the largest prior observation (gunbc#9954) on an unrelated tree, and the previous head of this same PR showed 2, so the amplitude moved by an order of magnitude across a main merge alone). THIS INSTANCE WAS ENUMERATED BY THE LANDING MANAGER RATHER THAN THE AUTHORING LANE, deliberately: this row is one very long line, so each lane appending its own instance produces a diff the review surface sizes as a one-line wording tweak -- the class filed as `gunbc.recurring_failure_mode` `salience_instrument_blind_to_the_record_it_sizes`, whose specimen is an earlier edit to THIS row. Batching the appends does not reduce the bytes a reviewer must read; it reduces the number of times that misreading is invited. RE-DERIVE ANY OF THESE WITH `gh api repos/OWNER/REPO/actions/jobs/JOB/logs --allow-escape-sequences` AND WITH NOTHING ELSE. Measured on the first pair above: `gh run view --job --log` answers an ATTEMPT-1 job id with ATTEMPT 2's CONTENT -- banner timestamp and counters both attempt 2's -- so an auditor re-deriving a two-attempt specimen with it obtains IDENTICAL content on both sides, observes no disagreement, and reports these enumerated instances as fabricated. The instrument fails in the direction that discredits a true finding, and without the escape-sequences flag the same endpoint writes zero bytes instead. Anyone checking these numbers must be holding the right instrument before disagreeing with them. NO MODELED PRODUCER COUNTS THESE, AND THAT MISSING COUNTER IS THIS PARAGRAPH'S OWN GAP: `RungDrop` carries no field for a mitigation instance, nothing folds the run ids, and a hand-kept TALLY is deliberately absent here because this row has already had to retract one hand-derivation described as a run product. A count with no producer is stale at the next roll and re-derivable by nobody; a run id is reachable by anyone. Whoever wants the number counts the citations. WHAT THE INSTANCES ESTABLISH BEYOND THE MITIGATION ITSELF: the two arms vary INDEPENDENTLY and in both directions on fixed bytes, and a refusal can repeat while disagreeing with itself about which rows were undecided -- so a reroll is not a coin flip against a fixed population but a fresh draw of the population. ONE FINER OBSERVATION THAN THIS ROW PREVIOUSLY SUPPORTED, from the last instance: after the live-gate cost repairs in 2d76d9ccb33 (gunbc#10038), `test.claim.self_host_compile_phase_live_gate_witness` was ABSENT from attempt 1 and BACK in attempt 2 of ONE head. A cost repair lowering a family's incidence is the expected reading; that the family is intermittent WITHIN a single head's attempts is stronger, and it is the sharpest available statement that a cost repair moves incidence without touching the mechanism at the boundary. The conflation of a computed non-verdict with a refusal at the AGGREGATE boundary is a separate class and is filed as `gunbc.recurring_failure_mode` `non_verdict_disposition_surfaces_as_refusal`, which cites this row for the cost half rather than re-deriving it." } data spark_role_scoped_retirement_production_root: RungDrop = RungDrop { identity: "spark_role_scoped_retirement_production_root" as NonEmptyStr, subject: "Spark serving role-scoped retirement evidence at the production plan root", declared: "2026-09-02", standing: Standing, authored: "**AN OPERATOR DECISION REMOVED A BEHAVIOUR'S ONLY SUBJECT, AND THIS ROW IS THAT DECLARATION (2026-09-02).** `gunbc.spark.cell_role` assigned srv6 to `SparkTrainingCell`, and the operator withdrew that dedication as premature -- 'i wouldn't dedicate a whole node for any task - just have it converge and serve whatever task we converge it to' -- so the production roster now holds ZERO training cells. Three claims in `test.claim.spark.spark_cell_role_retirement_witness_test` entered through `fleet_converge_plan_artifact`, the root the converge actuator itself walks, and each needed a production host holding that role to have a subject at all: `w_the_production_artifact_plans_four_retirements_for_the_training_cell`, `w_the_production_artifact_plans_no_rows_for_the_converged_serving_cell`, and `w_the_production_retirement_touches_no_baseline_address`. They are DELETED rather than left silently red, because a claim whose subject no longer exists is not a failing test, and leaving it to fail would have made an operator's decision look like a regression. **PREVIOUS RUNG: mechanically preventable** -- the training arm's four retirement rows and the serving arm's zero rows were both exercised through the production root, so a planner regression that pointed `spark_serving_full_membership_plan` back at the unscoped desired members went red there. **TEMPORARY RUNG: mitigatable** -- both arms are still exercised, but only at `spark_serving_role_scoped_desired_members_in` over an authored fixture roster (`w_the_planner_scopes_desired_state_by_role`), which is a real production function and is NOT the path the converge actuator calls; the same PR added `spark_cell_role_in` and that `_in` planner variant precisely so an arm's evidence stops depending on which machines are currently assigned what. **REASON:** operator decision, recorded with its basis at `gunbc.spark.cell_role` `spark_cell_role_assignment_basis`; role is converged desired state rather than a node dedication. **POPULATION, BOUNDED:** the training arm of Spark serving role scoping and the retirement rows it produces, AS REACHED THROUGH `fleet_converge_plan_artifact`. The serving arm, the no-role refusal, the reconcile, the freeze and the apply are unaffected and their production-root claims remain enrolled. **RESTORATION TRIGGER, NAMING THE CAPABILITY:** a roster-parameterized plan artifact -- the assignment roster threaded from `fleet_converge_plan_artifact` down to `spark_serving_role_scoped_desired_members_in` -- SUFFICIENT FOR a witness to drive the production root over an authored roster and read back the four retirement rows with no production host holding `SparkTrainingCell`. Half that capability exists today: both `_in` functions take the roster; what is missing is the threading through the generic artifact entry point. **RESTORING A TRAINING CELL TO THE PRODUCTION ROSTER DOES NOT RETIRE THIS DROP** -- that would re-create the coupling between an arm's evidence and the current assignment, which is the defect this row exists to record, and it is exactly the trigger-names-less-than-the-capability failure §4b(3) warns about." } -data floor_cut_heal: RungDrop = RungDrop { identity: "floor_cut_heal" as NonEmptyStr, subject: "Heal job for generated artifacts", declared: "2026-09-01", standing: Retired { trigger_fired: "2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. The two that ever executed did so on attempt 2, after a human acted. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. THIS CORRECTION DOES NOT MOVE THE ROW'S RUNG AND DOES NOT UN-RETIRE IT: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one." as NonEmptyStr }, authored: "**RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } +data floor_cut_heal: RungDrop = RungDrop { identity: "floor_cut_heal" as NonEmptyStr, subject: "Heal job for generated artifacts", declared: "2026-09-01", standing: Retired { trigger_fired: "2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. EXACTLY ONE of the four ever executed a job at all: run 33703032560 on attempt 2, after a human acted. The other re-attempt, 33705120607 attempt 2, was cancelled having also started zero jobs, so a second attempt is not itself a verdict either. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. READ THIS AT ATTEMPT GRAIN OR IT INVERTS, and both obvious proxies fail toward the reassuring answer: GitHub stamps run_started_at equal to created_at on a run that never ran, and a held run still concludes failure or cancelled rather than action_required, so neither a start timestamp nor a conclusion string is an execution receipt. Count JOBS, ON THE ATTEMPT THE CLAIM IS ABOUT -- 'count jobs' alone is not the discriminator, because the default endpoint silently answers for the LATEST attempt. AND THE RUN OBJECT ITSELF MANUFACTURES THE WRONG NUMBER, verified on run 33703032560: its top-level created_at is ATTEMPT 1's creation while its run_started_at is ATTEMPT 2's start, so the object hands back two fields from two different attempts and names neither, and only run_attempt reveals it. Subtracting them yields a start delay that never happened. Reading the latest attempt hides the class outright: on run 33703032560 attempt 1 is action_required with 0 jobs and attempt 2, created 1h47m later after a human acted, runs 6. THREE READERS MADE A VERSION OF THIS ERROR IN ONE NIGHT, EACH LEVEL INVISIBLE FROM THE ONE ABOVE: a run's conclusion read as an execution receipt, then a job count taken on the wrong attempt, then the cross-attempt subtraction above -- recorded because the reader who warned about the second level was standing in the third while writing the warning. There was never a released run here; a human re-ran it. A CONSEQUENCE FOR THIS ROW'S OWN LANGUAGE, and it is why the clause is scoped rather than merely corrected: a held run CAN be released later and judge the head. Of the four, run 33703032560 eventually executed 6 jobs on a head heal had pushed. So 'a head nothing judged' is true AT EXIT TIME and may stop being true afterwards without anyone touching anything. The exit is a statement by the run printing it about the moment it prints, never a standing property of the healed head, and a carrier that states it unscoped is wrong the moment somebody approves. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. WHY THE HOLD EXISTS IS LIKEWISE UNDETERMINED BECAUSE UNREADABLE, which is the honest shape and not an unexplained gap: repos/gunb-ai/gunbc/actions/permissions is 403 to these session tokens, so whether a repository setting explains it cannot be read from here. THE RETIREMENT ITSELF STANDS, stated as the output of the question rather than left to be inferred, and this correction does not move the row's rung: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one." as NonEmptyStr }, authored: "**RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } data floor_cut_effect_gates: RungDrop = RungDrop { identity: "floor_cut_effect_gates" as NonEmptyStr, subject: "Six of the seven effect gates (one restored)", declared: "2026-09-01", standing: Standing, authored: "**SIX OF THE SEVEN EFFECT GATES ARE UNGUARDED AND THE SEVENTH IS BACK, AND THE FRACTION IS STATED BECAUSE SAYING `THE EFFECT GATES` WHERE ONE OF SEVEN IS LIVE IS THE OVERSTATEMENT THIS LEDGER KEEPS PAYING FOR (2026-09-01).** Split out of `floor_cut`. THE SEVEN, from that row's own loss clause: compile-clean, generated-artifact drift, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. DISCHARGED, 1 of 7: generated-artifact drift, restored by gunbc#9415 as the required `generated-artifact` phase adjudicating every member of `committed_generated_artifacts` through `gunbc.generated_artifact_emit` `generated_artifact_body_for_path`. It is named here as DONE rather than deleted from the list, because a population that shrinks silently cannot be checked. OUTSTANDING, 6 of 7: compile-clean, emit-host, extdeps citation, extdeps placement, prose-row, cheap-claim pool. PREVIOUS RUNG: 2 (mechanically preventable) for each -- a required gate blocked the merge. TEMPORARY RUNG: 0 for the six; not `1`, because these are not mitigated failures but UNOBSERVED ones -- the class is outside the modeled guarantee at the merge boundary until its gate returns. REASON: the 2026-08-15 floor cut deleted the wrapper carrying all seven obligations. BOUNDED POPULATION: the six named gates, enumerated above; the roster is closed and is not `whatever the plan lists`. RESTORATION TRIGGER, PER GATE AND NOT FOR THE SET: this row retires only when EACH of the six has a required-run consumer that refuses a merge on its own violation, each with a discriminating RED executed on the real acceptance path. Six retirements, one row, and the row states its own remaining fraction whenever it is read. WHAT DOES NOT RETIRE THIS ROW: the `generated-artifact` phase being live, which is the one already discharged; a lens that computes any of the six without gating, which is the inert tier DESIGN section 6 names; or a gate landed with no authored RED, which is a wall nobody has seen fire. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids." } diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 44c640184fd..fd0a3da4352 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -154,4 +154,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - realization arms diverge on WHETHER THE PROGRAM REFUSES (two realizations of one accepted program agree on the returned value and disagree on whether an evaluation-time refusal fires, because the fact that decides it -- evaluation order -- is modeled nowhere and each arm improvises). INVALID STATE: a connective whose operand evaluation strategy is unmodeled, realized strictly by one arm and lazily by another. gunbc v1 today: v1.compiler.interpreter eval_expr_inner's ExprBinOp arm evaluates BOTH operands through `?` before dispatching. eval_binop DOES carry And and Or arms -- `Value::Bool(left.is_truthy() && right.is_truthy())` -- and they are irrelevant to this class and worth naming precisely because they look like the repair: they run on operands ALREADY EVALUATED at the call site, so their Rust && is over two bools and short-circuits nothing. A reader grepping eval_binop for And finds a hit and concludes the case is handled, while std.operator_realization maps BinOp::And and BinOp::Or to OperatorRealization::HostOperator, rendered as Rust && and ||, which short-circuit. HARM: the guard idiom -- a cheap precondition guarding an expression that can refuse -- means two different programs. The interpreter runs the guarded expression when the guard is FALSE and refuses; emitted Rust never runs it and returns a value. Silent in both directions and invisible to any oracle comparing returned values on guard-true inputs, which is every value-comparison oracle we have. DISCRIMINATING RED, executed 2026-09-02, not asserted: `fn guarded_division(n: Int) -> Bool { n != 0 && (100 / n) > 1 }`. At n=0 the interpreter refuses DivisionByZero and the emitted Rust returns false; at n=5 both return true. Division by zero was chosen deliberately because BOTH realizations abort identically IF the expression is evaluated, so evaluation order is the only variable in the pair. CONTROLS, because a false from a harness that cannot observe an abort is a vacuous green: the same function with the guard forced true and n=0 PANICKED with 'attempt to divide by zero' and was caught and reported, so the harness can see the abort; and the guard-true positive control agrees across both arms. HONESTY BOUND ON THE EVIDENCE: the interpreter arm ran on the real acceptance path via `gunbc run`; the emitted arm executed the emitted function bodies extracted VERBATIM into a rustc harness, not the whole emitted crate. WHY IT IS NOT refusal_deferred_to_emitted_runtime: that class is a compiler writing a refusal construct INTO the artifact while reporting success. Here no refusal is written anywhere and the compile is honest; the two arms simply disagree at run time about whether one fires. Same neighbourhood, different invalid state, different repair. THE POPULATION IS SURVIVORSHIP-FILTERED AND A GREP UNDERSTATES IT BY CONSTRUCTION. The interpreter is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the refusal while authoring and rewrote it -- most likely into a nested if or match. So the sites matching `cheap_guard && expensive` are the SURVIVORS, the cases where the right operand happens not to refuse; the cases carrying the correctness consequence were already edited away. A LOW COUNT IS THEREFORE NOT EVIDENCE THE CLASS IS MINOR AND MUST NOT BE REPORTED AS ONE. The honest population is sites where an author WANTED the guard idiom, which lives in the rewrites and is not reachable by the same needle. RECOGNITION RULE, stated to generalise past this operator: wherever a construct is realized independently by the interpreter and by an emission target, ask what fact decides its behaviour and where that fact is DECLARED. If the deciding fact is absent from the authority both arms are supposed to consult, the arms are not implementing one semantics, they are each inventing one, and agreement on the values you happened to test is not evidence they agree. The tell is a realization shape -- HostOperator -- that names WHO evaluates without naming WHAT is evaluated. RUNG: mitigatable at best, and only because one arm refuses loudly; against a source-to-emission path this is silent wrongness, which DESIGN section 4b places outside the ladder. NEXT-RUNG TRIGGER, named as a capability and not an artifact: EVALUATION ORDER MODELED AS A PROPERTY OF A CONNECTIVE IN THE .dag AUTHORITY AND CONSULTED BY BOTH REALIZATIONS -- sufficient for the interpreter's binop arm to derive its strictness from the same row the emitter derives its rendering from, so that a connective's operand strategy cannot be stated twice or left unstated. A grep across dag/, src/v2/ and src/v1/*.dag on 2026-09-02 found no such fact: every short-circuit hit is prose in a comment or a witness name. NOT REPAIRED HERE: changing the interpreter to short-circuit is a corpus-wide evaluation-semantics change and needs its own subject, population and review; filing it against the missing carrier is the point of this row. - **a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: "cannot apply Lt to Record and Int" }`, while the same call over a zero-byte primitive returns `"?"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `"?"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation. - **a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row. -- **a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. NEXT TRIGGER, NAMED AS THE CAPABILITY: a carrier that states a fact about an external system carries the OBSERVATION that produced it as a typed row -- the query, the population, the date -- so that an unobserved mechanism is structurally distinguishable from an observed one and can be listed. `extdeps` already owns the shape for cited upstream facts and this class is what a boundary-observation row would be for. Until that exists this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names. +- **a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. THIS CLASS IS DETECTABLE ONLY FROM OUTSIDE THE REPOSITORY, and that is the whole difficulty rather than an aside: the refuting evidence lives in the external system, so no lens, gate or witness reading this tree can reach it, and the class is invisible to every mechanism the repository owns. NEXT TRIGGER, and it is honestly UNDETERMINED rather than named, which is the fail-closed way to leave it. The capability question is what would have to be OBSERVABLE for a mechanism claim about an external system to be executable evidence rather than an assertion -- and that is not settled here. What can be said now: a carrier that states such a fact should carry the OBSERVATION that produced it -- the query, the population, the date -- so an unobserved mechanism is structurally distinguishable from an observed one and can be listed; `extdeps` already owns the shape for cited upstream facts. That is a necessary condition and it is NOT KNOWN to be sufficient, because a recorded observation of a system that can change its behaviour without notice is a receipt about a past world, which is section 4b's outside-the-modeled-guarantee column and not a rung. A TRIGGER NAMING THAT ROW AS THE CAPABILITY WOULD THEREFORE BE THE ARTIFACT-FOR-CAPABILITY SUBSTITUTION section 4b(3) FORBIDS, satisfied while the class stays alive. Until the question is settled this row is a reading discipline and citing it as coverage is rung inflation. diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 2078637bad0..5659733a1eb 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -10,7 +10,7 @@ Each row declares a safety guarantee that was lowered: what stood before, what s ### Heal job for generated artifacts — declared 2026-09-01 · RETIRED -**RETIRED — TRIGGER FIRED.** 2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. The two that ever executed did so on attempt 2, after a human acted. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. THIS CORRECTION DOES NOT MOVE THE ROW'S RUNG AND DOES NOT UN-RETIRE IT: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one. +**RETIRED — TRIGGER FIRED.** 2026-09-02 -- THE CAPABILITY, OBSERVED, NOT THE EMISSION. gunbc#10118 restored the heal job as a job of gunbc.witness_floor_workflow, and the row is retired on an EXECUTED repair of a REAL divergence rather than on that emission. THE PROBE: commit 330c74f0735364644c6a527a2d61de8da0a37cd8 hand-edited docs/plans/input-envelope-roadmap.md, a generated projection, from 3555 bytes (sha256 4da64e1495ef627c31fa21f3e31e2746ba28c5be447c9f6565d9a004f2c23ead) to 3754 and did not regenerate it. The subject was chosen against the emitted script rather than assumed: it carries a git add line and does NOT appear in the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm; the three workflow projections would have exercised bundle-and-refuse while looking like a heal run. THE RECEIPT, run 33683175090 job 100433326005: HealProduced prior_head=330c74f0735364644c6a527a2d61de8da0a37cd8 healed_head=bc704687540d25796f53f88687226ee1a735743c changed_artifacts=docs/plans/input-envelope-roadmap.md -- exactly one path, no blast radius across the other 32 auto-push rows -- then SupersededByHealedHead and exit 1. The branch head moved, authored gunbc-ci-auto-heal , under the checkout persist-credentials binding gunbc.heal_push_plan resolves the push authority from. IDENTITY CONFIRMED TWO WAYS: the healed file is byte-identical to the pre-drift digest recorded BEFORE the probe, and a clean source-built regeneration on the healed head (whose src/ and dag/ are identical to the tree the binary was built from) changed ZERO files. RESTORED RUNG: 2 (mechanically preventable) -- drift is caught by the required generated-artifact phase and now CORRECTED without an author, which is the previous rung this row lost. NOT RESTORED, and this row does not claim it: revalidation of the head heal creates. CORRECTED 2026-09-03, AND THE ORIGINAL SENTENCE IS QUOTED RATHER THAN DELETED BECAUSE THE RECORD OF WHAT WAS CLAIMED IS THE POINT. This row said: 'An Actions-credential push starts no run, so heal exits nonzero with SupersededByHealedHead rather than reporting a verdict about a head nothing judged.' THE FIRST CLAUSE IS FALSE; EVERYTHING IT WAS OFFERED TO SUPPORT STANDS. Measured over the entire heal-push population since the job was restored -- n=4, healed heads bc704687540d25796f53f88687226ee1a735743c, 695f264c77, 7de8273834 and 958f743f9ec056f73fbd4e4adedf84a65a7bc41b, re-derivable by listing repos/gunb-ai/gunbc/actions/runs filtered to actor.login == github-actions[bot] and reading each run's ATTEMPT 1 rather than its latest attempt -- a pull_request run WAS created for the healed head 4 times out of 4. WHAT GITHUB WITHHOLDS IS EXECUTION, NOT CREATION: 0 of those 4 started a single job on the triggering attempt. Runs 33711005806, 33703032560 and 33705120607 completed action_required with zero jobs; run 33686753487 completed failure with zero jobs. EXACTLY ONE of the four ever executed a job at all: run 33703032560 on attempt 2, after a human acted. The other re-attempt, 33705120607 attempt 2, was cancelled having also started zero jobs, so a second attempt is not itself a verdict either. So the loss this clause names is unchanged -- no EXECUTED verdict exists for the healed head, and heal exits nonzero rather than speaking for a tree it produced -- while the shape of it is not. The judge is CREATED AND HELD, not absent. READ THIS AT ATTEMPT GRAIN OR IT INVERTS, and both obvious proxies fail toward the reassuring answer: GitHub stamps run_started_at equal to created_at on a run that never ran, and a held run still concludes failure or cancelled rather than action_required, so neither a start timestamp nor a conclusion string is an execution receipt. Count JOBS, ON THE ATTEMPT THE CLAIM IS ABOUT -- 'count jobs' alone is not the discriminator, because the default endpoint silently answers for the LATEST attempt. AND THE RUN OBJECT ITSELF MANUFACTURES THE WRONG NUMBER, verified on run 33703032560: its top-level created_at is ATTEMPT 1's creation while its run_started_at is ATTEMPT 2's start, so the object hands back two fields from two different attempts and names neither, and only run_attempt reveals it. Subtracting them yields a start delay that never happened. Reading the latest attempt hides the class outright: on run 33703032560 attempt 1 is action_required with 0 jobs and attempt 2, created 1h47m later after a human acted, runs 6. THREE READERS MADE A VERSION OF THIS ERROR IN ONE NIGHT, EACH LEVEL INVISIBLE FROM THE ONE ABOVE: a run's conclusion read as an execution receipt, then a job count taken on the wrong attempt, then the cross-attempt subtraction above -- recorded because the reader who warned about the second level was standing in the third while writing the warning. There was never a released run here; a human re-ran it. A CONSEQUENCE FOR THIS ROW'S OWN LANGUAGE, and it is why the clause is scoped rather than merely corrected: a held run CAN be released later and judge the head. Of the four, run 33703032560 eventually executed 6 jobs on a head heal had pushed. So 'a head nothing judged' is true AT EXIT TIME and may stop being true afterwards without anyone touching anything. The exit is a statement by the run printing it about the moment it prints, never a standing property of the healed head, and a carrier that states it unscoped is wrong the moment somebody approves. THE HOLD DISCRIMINATES ON THE EVENT, NOT ON THE IDENTITY OR THE TOKEN, and this arm is measured TWO-SIDED with the identity held constant on both sides. Forward: of 500 workflow_dispatch runs sampled, ZERO concluded action_required -- including all 151 actored by github-actions[bot], the same identity and default-token surface whose pull_request runs are held. Reverse control: the entire status=action_required listing is 17 runs and ALL 17 are event=pull_request, zero workflow_dispatch. Re-derive by listing repos/gunb-ai/gunbc/actions/runs with event=workflow_dispatch grouped by actor.login and conclusion, against the status=action_required listing grouped by event. Measured by cool-koi-623 and reproduced independently at the wider sample by fierce-ram-670, which is why the sample sizes here are the larger pair. Two things follow that the refuted premise concealed: releasing the healed head is an approve on that specific gated run (POST /actions/runs//approve) and not a re-run of another run, and a dispatched revalidation is a SECOND run on that head rather than the only one, costing a whole additional run and landing check-runs beside the gated run's on one commit where a name-keyed reader cannot tell them apart. That second cost buys something measured rather than duplicating what would have happened anyway -- by the event discriminator above, a dispatched run is the only route to the healed head that executes without a human. WHAT IS NOT ESTABLISHED AND IS NOT WRITTEN AS IF IT WERE: whether a dispatched run's contexts clear branch protection. repos/gunb-ai/gunbc/branches/main/protection is 403 to this token, and the held run is what protection was waiting on, so closing the REVALIDATION gap is measured and clearing the MERGE gate is not. WHY THE HOLD EXISTS IS LIKEWISE UNDETERMINED BECAUSE UNREADABLE, which is the honest shape and not an unexplained gap: repos/gunb-ai/gunbc/actions/permissions is 403 to these session tokens, so whether a repository setting explains it cannot be read from here. THE RETIREMENT ITSELF STANDS, stated as the output of the question rather than left to be inferred, and this correction does not move the row's rung: the restored capability is automatic repair of drifted generated artifacts, which the receipt above observed, and revalidation was already declared NOT RESTORED here. Its trigger is a workflow_dispatch input on gunbc.witness_floor_workflow carrying the healed sha, which every dispatched run binds its own github.sha and checkout against before any witness counts; tools.ci_heal_dispatch is the modeled half and stays unconsumed until then. That gap is a separate obligation, not this row. `floor_cut` DOES NOT RETIRE ON THIS: its trigger is the conjunction of five siblings and this is one. **RETIRED 2026-09-02 BY gunbc#10118; READ THE DECLARATION BELOW IN THE PAST TENSE.** The heal job runs again, as a job of `gunbc.witness_floor_workflow` rather than of the deleted `gunbc.ci_workflow`, and the dangling-citation observation this row recorded is also repaired: `ci_heal_credential` `ci_heal_job_ref` and `ci_heal_workflow_ref` now name the emission that carries the job, and their spent `PRE_EXISTING_CITATION_DEBT` rows are deleted. The opening sentence is kept rather than rewritten because the declaration is the record of what was true when it was made; `standing` carries what is true now. ONE CLAUSE OF THE ORIGINAL LOSS IS NOT RESTORED AND IS NOT SILENTLY DROPPED: revalidation of the head heal creates -- see `trigger_fired` for its own trigger. **HEAL IS GONE AND ITS AUTHORITY MODULE IS GONE WITH IT, AND THIS ROW DECLARED THAT RUNG (2026-09-01).** Split out of `floor_cut`, whose single trigger could not retire it. PREVIOUS RUNG: 2 (mechanically preventable) -- a required job regenerated drifted generated artifacts and pushed the repair onto the branch head, so the class `a committed generated artifact diverges from its authority` was caught and CORRECTED without an author. TEMPORARY RUNG: 1 (mitigatable) -- drift is still CAUGHT, by the `generated-artifact` required phase, but nothing repairs it, so every divergence is now a human round trip. REASON: the 2026-08-15 floor cut deleted the job with the workflow authority that carried it. BOUNDED POPULATION: one capability -- automatic repair of drifted generated artifacts on a branch head. MEASURED FROM THE TREE RATHER THAN FROM THE PARAGRAPH UNDER SUSPICION (2026-09-01): `gunbc.ci_heal_credential` survives in full and still carries `ci_heal_job_ref` and `ci_heal_workflow_ref` as DeclarationRefs to `gunbc.ci_workflow` `ci_heal_generated_artifacts_job` and `gunbc.ci_workflow` `ci_workflow` -- and `gunbc.ci_workflow` DOES NOT EXIST in this tree; the only module of that stem is `gunbc.ci_workflow_expressions`, and the decl name resolves nowhere. So heal's credential model is live and its job and workflow are deleted, which also means a typed citation to a deleted module is sitting unrefused; that second fact is recorded here as an observation and is NOT this row's subject. RESTORATION TRIGGER, A CAPABILITY: a required-run consumer that, on a branch head whose committed generated artifacts diverge from their authorities, WRITES the regenerated bytes back and pushes them under a credential the repository already models -- observed doing so on a real divergence, not merely emitted. WHAT DOES NOT RETIRE THIS ROW: restoring `gunbc.ci_workflow` or re-pointing `ci_heal_credential`'s dangling citations, which repairs the MODEL and heals nothing; nor a job that only reports drift, which is the phase we already have. **`floor_cut` CANNOT RETIRE WHILE THIS ROW STANDS**, and this sentence is on every one of the five so the constraint is readable from either end: that row's trigger is the conjunction of these five, so retiring it on a reading of any single sibling -- including this one -- is the reading its own trigger forbids. From 408cc538222b4062ff06774cd2116eaa77e2b97e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 3 Sep 2026 04:38:05 +0000 Subject: [PATCH 3/3] Review fix: the class ranks an in-repo authoring act, so it gets a derived ceiling and a named trigger MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 --- dag/gunbc/recurring_failure_mode.dag | 2 +- docs/design-failure-modes.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode.dag b/dag/gunbc/recurring_failure_mode.dag index 33527b50d8d..403b4896d18 100644 --- a/dag/gunbc/recurring_failure_mode.dag +++ b/dag/gunbc/recurring_failure_mode.dag @@ -263,7 +263,7 @@ data realization_arms_diverge_on_whether_the_program_refuses: RecurringFailureMo data declared_return_disagrees_with_the_generic_it_returns: RecurringFailureMode = RecurringFailureMode { identity: "declared_return_disagrees_with_the_generic_it_returns" as NonEmptyStr, authored: "**a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: \"cannot apply Lt to Record and Int\" }`, while the same call over a zero-byte primitive returns `\"?\"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `\"?\"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation.", evidence: [] } data non_execution_undifferentiated_by_what_it_silenced: RecurringFailureMode = RecurringFailureMode { identity: "non_execution_undifferentiated_by_what_it_silenced" as NonEmptyStr, authored: "**a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row.", evidence: [] } -data external_mechanism_asserted_under_a_correct_conclusion: RecurringFailureMode = RecurringFailureMode { identity: "external_mechanism_asserted_under_a_correct_conclusion" as NonEmptyStr, authored: "**a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. THIS CLASS IS DETECTABLE ONLY FROM OUTSIDE THE REPOSITORY, and that is the whole difficulty rather than an aside: the refuting evidence lives in the external system, so no lens, gate or witness reading this tree can reach it, and the class is invisible to every mechanism the repository owns. NEXT TRIGGER, and it is honestly UNDETERMINED rather than named, which is the fail-closed way to leave it. The capability question is what would have to be OBSERVABLE for a mechanism claim about an external system to be executable evidence rather than an assertion -- and that is not settled here. What can be said now: a carrier that states such a fact should carry the OBSERVATION that produced it -- the query, the population, the date -- so an unobserved mechanism is structurally distinguishable from an observed one and can be listed; `extdeps` already owns the shape for cited upstream facts. That is a necessary condition and it is NOT KNOWN to be sufficient, because a recorded observation of a system that can change its behaviour without notice is a receipt about a past world, which is section 4b's outside-the-modeled-guarantee column and not a rung. A TRIGGER NAMING THAT ROW AS THE CAPABILITY WOULD THEREFORE BE THE ARTIFACT-FOR-CAPABILITY SUBSTITUTION section 4b(3) FORBIDS, satisfied while the class stays alive. Until the question is settled this row is a reading discipline and citing it as coverage is rung inflation.", evidence: [] } +data external_mechanism_asserted_under_a_correct_conclusion: RecurringFailureMode = RecurringFailureMode { identity: "external_mechanism_asserted_under_a_correct_conclusion" as NonEmptyStr, authored: "**a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1 ON AXIS (i) BELOW, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. THE SUBJECT OF THIS ROW IS A CARRIER IN THIS REPOSITORY, NOT THE EXTERNAL SYSTEM, and an earlier revision of this row got that backwards -- corrected here rather than annotated, because the error is exactly the one section 4b's carve-out exists to prevent. That revision assigned a LADDER RUNG to external reality, which section 4b deliberately keeps OFF the ladder, and then declined to name a trigger; between them those two moves let 'we do not model GitHub' stand where a rankable in-repository defect actually sits. The invalid state is an AUTHORING ACT that is wholly in the tree: a carrier states an unobserved mechanism as the reason for a decision. That is decidable from the carrier alone, so it ranks, and it is obligated to climb. TWO AXES, WITH DIFFERENT CEILINGS BECAUSE THEY HAVE DIFFERENT DECIDABILITY, and only the first is a ladder subject at all. (i) THE SEPARATION -- is this mechanism claim backed by an observation? Decidable by reading the carrier. CEILING: 4, structurally impossible, and DERIVED rather than aspirational: if the only construction able to express an external-system mechanism requires the observation that produced it, an unbacked mechanism claim has no constructor, and validation becomes unnecessary because the bad state cannot be written. Anything below 4 on this axis is a correctness gap, not a ceiling. (ii) THE TRUTH of the external fact -- whether the observed behaviour still holds. OUTSIDE THE MODELED GUARANTEE, not a rung and never one: observed, refused or mitigated at a declared boundary, never fabricated. It is named here precisely so it cannot be mistaken for a weak implementation that should climb. NEXT TRIGGER FOR AXIS (i), NAMED AS THE CAPABILITY AND NOT AS AN ARTIFACT: an external-system mechanism claim is expressible ONLY through a typed construction carrying the observation that produced it -- the query, the population, the date -- together with a consumer that ENUMERATES carriers stating such a claim without one. The pairing is the whole trigger: the construction alone makes the honest form available, and only the enumerating consumer makes the dishonest form unwritable rather than merely noticed once. Authoring one such row by hand discharges nothing and is the artifact-for-capability substitution section 4b(3) forbids. It is CAN-CLIMB-NOW-BUT-UNBUILT rather than blocked on grounding: `extdeps` already owns the shape for cited upstream facts. SECTION 4c DECIDES WHERE THIS CANNOT LIVE, recorded so the cheap version is not proposed later as an economy: semantic passes receive only the annotation-erased projection, so an annotation can never carry the observation and the construction must be a real declaration. WHAT THE DISCHARGED TRIGGER DOES NOT BUY, stated so it is not read as covering axis (ii): every mechanism claim would then carry a receipt, and a receipt is not currency -- a system that changes without notice makes any observation a statement about a past world. That residual is axis (ii) and stays outside the guarantee by construction. WHAT IS ASYMMETRIC ABOUT THIS CLASS, and it is why it survives review rather than why it cannot be ranked: the DEFECT is visible from inside the tree -- a claim with no observation beside it -- while the REFUTATION lives in the external system and no lens, gate or witness reading this tree can reach it. So the class is detectable here and falsifiable only there, which is what lets a wrong mechanism sit unchallenged beside a correct conclusion for as long as nobody goes outside to look. Until axis (i)'s trigger is built this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names.", evidence: [] } data recurring_failure_mode_roster: List = [ censored_estimator_drops_its_own_tail, diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 92442ab877e..8baa6fb2739 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -154,4 +154,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - realization arms diverge on WHETHER THE PROGRAM REFUSES (two realizations of one accepted program agree on the returned value and disagree on whether an evaluation-time refusal fires, because the fact that decides it -- evaluation order -- is modeled nowhere and each arm improvises). INVALID STATE: a connective whose operand evaluation strategy is unmodeled, realized strictly by one arm and lazily by another. gunbc v1 today: v1.compiler.interpreter eval_expr_inner's ExprBinOp arm evaluates BOTH operands through `?` before dispatching. eval_binop DOES carry And and Or arms -- `Value::Bool(left.is_truthy() && right.is_truthy())` -- and they are irrelevant to this class and worth naming precisely because they look like the repair: they run on operands ALREADY EVALUATED at the call site, so their Rust && is over two bools and short-circuits nothing. A reader grepping eval_binop for And finds a hit and concludes the case is handled, while std.operator_realization maps BinOp::And and BinOp::Or to OperatorRealization::HostOperator, rendered as Rust && and ||, which short-circuit. HARM: the guard idiom -- a cheap precondition guarding an expression that can refuse -- means two different programs. The interpreter runs the guarded expression when the guard is FALSE and refuses; emitted Rust never runs it and returns a value. Silent in both directions and invisible to any oracle comparing returned values on guard-true inputs, which is every value-comparison oracle we have. DISCRIMINATING RED, executed 2026-09-02, not asserted: `fn guarded_division(n: Int) -> Bool { n != 0 && (100 / n) > 1 }`. At n=0 the interpreter refuses DivisionByZero and the emitted Rust returns false; at n=5 both return true. Division by zero was chosen deliberately because BOTH realizations abort identically IF the expression is evaluated, so evaluation order is the only variable in the pair. CONTROLS, because a false from a harness that cannot observe an abort is a vacuous green: the same function with the guard forced true and n=0 PANICKED with 'attempt to divide by zero' and was caught and reported, so the harness can see the abort; and the guard-true positive control agrees across both arms. HONESTY BOUND ON THE EVIDENCE: the interpreter arm ran on the real acceptance path via `gunbc run`; the emitted arm executed the emitted function bodies extracted VERBATIM into a rustc harness, not the whole emitted crate. WHY IT IS NOT refusal_deferred_to_emitted_runtime: that class is a compiler writing a refusal construct INTO the artifact while reporting success. Here no refusal is written anywhere and the compile is honest; the two arms simply disagree at run time about whether one fires. Same neighbourhood, different invalid state, different repair. THE POPULATION IS SURVIVORSHIP-FILTERED AND A GREP UNDERSTATES IT BY CONSTRUCTION. The interpreter is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the refusal while authoring and rewrote it -- most likely into a nested if or match. So the sites matching `cheap_guard && expensive` are the SURVIVORS, the cases where the right operand happens not to refuse; the cases carrying the correctness consequence were already edited away. A LOW COUNT IS THEREFORE NOT EVIDENCE THE CLASS IS MINOR AND MUST NOT BE REPORTED AS ONE. The honest population is sites where an author WANTED the guard idiom, which lives in the rewrites and is not reachable by the same needle. RECOGNITION RULE, stated to generalise past this operator: wherever a construct is realized independently by the interpreter and by an emission target, ask what fact decides its behaviour and where that fact is DECLARED. If the deciding fact is absent from the authority both arms are supposed to consult, the arms are not implementing one semantics, they are each inventing one, and agreement on the values you happened to test is not evidence they agree. The tell is a realization shape -- HostOperator -- that names WHO evaluates without naming WHAT is evaluated. RUNG: mitigatable at best, and only because one arm refuses loudly; against a source-to-emission path this is silent wrongness, which DESIGN section 4b places outside the ladder. NEXT-RUNG TRIGGER, named as a capability and not an artifact: EVALUATION ORDER MODELED AS A PROPERTY OF A CONNECTIVE IN THE .dag AUTHORITY AND CONSULTED BY BOTH REALIZATIONS -- sufficient for the interpreter's binop arm to derive its strictness from the same row the emitter derives its rendering from, so that a connective's operand strategy cannot be stated twice or left unstated. A grep across dag/, src/v2/ and src/v1/*.dag on 2026-09-02 found no such fact: every short-circuit hit is prose in a comment or a witness name. NOT REPAIRED HERE: changing the interpreter to short-circuit is a corpus-wide evaluation-semantics change and needs its own subject, population and review; filing it against the missing carrier is the point of this row. - **a declared return type disagrees with the type its body actually produces, because the body's type comes from a GENERIC CALL'S INSTANTIATION** (INVALID STATE: a function declares `-> F` and returns the result of `g(...)` instantiated at `T = B`, so the produced type is `F`. The declaration is authored independently of the body and nothing joins them, so `A` and `B` never meet. Every consumer then reads the DECLARATION, passes the value into a parameter typed `A`, and the mismatch surfaces -- if it surfaces at all -- as a runtime type error inside a callee that names neither the declaration nor the drift. HARM: this is the loud-but-hidden corner of section 5 rather than silent wrongness. The abort is honest when it happens; what is silent is the CLASS, because the drifted arm is commonly the one that is rarely reached, so the function reads as working while one of its inhabitants is unwritable-through. **DISTINCT FROM ITS NEIGHBOURS.** `state_space_conflation` is a domain modelled with too few constructors; here the domain is right and the CARRIER's parameter is wrong. `hollow_alias` is a second name for one concept; here there is one name and two types. **SPECIMEN (keen-ferret-172, gunbc#10109, 2026-09-02), and the two halves of it carry different warrants.** VERIFIED BY SOURCE, independently by two readers: `v2.std.runtime` `RuntimePrimitiveValue.bytes` is `List`; `v2.std.collection` `list_at_optional(xs: List, index: Int) -> Optional` therefore yields `Optional`; `v2.std.native_agreement` `runtime_value_discriminant_octet` declares `-> Optional` and returns exactly that call; its `Present` arm feeds the value to `octet_display(octet: Int)`. VERIFIED BY EXECUTION, by one reader: `runtime_value_octet_label` over a `RuntimePrimitive` carrying two bytes aborts with `TypeError { msg: "cannot apply Lt to Record and Int" }`, while the same call over a zero-byte primitive returns `"?"` -- re-derive with the enrolled pair `label_of_a_two_byte_primitive` and `label_of_an_empty_primitive_is_unknown`, the first of which aborts against the pre-repair generation and the second of which passes in BOTH states and is therefore not a presence-detector for the repair. **WHY IT SURVIVED: THE ONLY REACHED ARM WAS THE ABSENT ONE.** `list_at_optional` at index 1 returns `Absent` for the short primitives the live paths carry, and `Absent` answers `"?"` without ever constructing the drifted value. So the formatter whose carrier note exists BECAUSE a revert once reported member and values unknown could itself abort exactly when a divergence was being reported. **RECOGNITION RULE, mechanical and cheap: for any function whose declared return is a GENERIC APPLICATION, name the call that produces the returned value and instantiate its type parameters from its ARGUMENTS, not from the enclosing declaration.** If the argument is a `List` and the declaration says `F` with `A` != `B`, the drift is there to read. The tell that makes it worth checking at all is a declared parameter of a primitive type -- `Int`, `String`, `Bool` -- reached from a container whose element type is a record. **A SECOND TELL, and it is the one that generalises past types: THE FUNCTION WAS UNWITNESSABLE.** This drift was found only after a fold's parameter was narrowed from a whole `TestClaimRun` to the `Verdict` it actually read, because the wide parameter required a cache receipt no witness could construct. THE TWO HALVES ARE DISTINCT AND AN EARLIER REVISION OF THIS ROW CONFLATED THEM, which is corrected here rather than annotated: what ADMITTED the defect is the missing return-agreement judgment, and what left it UNEXPOSED is the oversized parameter, which deprived the affected fold of a constructible executing witness so that the incomplete typecheck was the only exercised admission path. So `a parameter wider than what the body reads` is a standing prompt to narrow it and then execute. AND SOURCE READING CAN ESTABLISH THE DRIFT: the recognition rule above is exactly that procedure, and two readers followed it independently -- `List` instantiates `T = Byte`, so the produced type is `Optional` against a declared `Optional`. Execution is required for the runtime abort and its observed message, NOT for the type disagreement; the earlier claim that reading cannot find this class was false, and it was false in a row whose own recognition rule refutes it. **RUNG FOUND AT: 1, mitigatable.** The failure is a typed runtime abort with containment but no locality: it names an operator and two shapes, not the declaration that lied. **CEILING: 3, structurally guaranteed, and not 4.** A declared return is authored independently of the body, so a source file can always SPELL the disagreement; what is attainable is that no `Accepted` program contains one, by deriving the body's type and refusing the mismatch. It is decidable and fully modelled -- both types are in hand at the same grain -- so anything below 3 is a correctness gap rather than a ceiling. **NEXT TRIGGER, named as the CAPABILITY: return-type agreement checked at the declaration boundary, comparing a declared return against the body's inferred type THROUGH A GENERIC CALL'S INSTANTIATION.** The qualifier is the whole trigger and not decoration: a checker that compares only concrete returns is satisfied by this specimen while the class stays alive, because the drift enters through `T`. Until that capability exists this row is a review discipline, and citing it as coverage is rung inflation. - **a required row does not execute, and NOTHING DECLARES WHAT ITS EXECUTION ESTABLISHED, so every non-execution looks alike** (INVALID STATE: a row that is preempted, skipped or otherwise reaches no verdict is reported as undecided, and the report carries no fact separating a row whose absence merely leaves a question open from a row whose absence REMOVES A WALL. HARM: the second kind is silently decoverage. The row PASSES in the ordinary case, so preempting it turns a standing guarantee off with nothing red anywhere -- and because the population cannot be ordered by consequence, the expensive rows get the optimisation attention while the load-bearing ones are invisible. A retry that draws a faster runner then buys a green OVER REFUSALS THAT DID NOT EXECUTE, which is why re-running is not an exit. SPECIMEN, and the two concepts are DISJOINT rather than conflated -- the opposite of what the lane suspected before it read the setter. `v1.cli_run` `InterruptedBeforeVerdict.enrolled_expected_red` is KnownRed QUARANTINE and nothing else: it is set true on exactly one branch of the required-floor claim loop, the expected-red arm reaching `ExpectedRedArm::BudgetRefused`, and it means the identity is rostered as DECLARED-TO-FAIL. The rows whose silencing motivated this class carry it FALSE. `test.claim.self_host_compile_phase_live_gate_witness` `a_live_tree_that_gained_an_identity_refuses_and_names_it` and `a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses` are ordinary PASSING rows on no expected-red, cost-debt or quarantine roster in the tree; their content is that `live_tree_frontier_verdict` returns `LiveFrontierRefused` and NAMES the planted identity. The second carries an in-source comment stating that it is precisely the probe that would go green if the join were replaced by a population-size comparison -- so preempting that one row makes that sentence stop being true while the run reports one more undecided claim. THAT IS THE WHOLE SEVERITY, and it is why the quarantine flag cannot stand in for the missing fact: quarantine names rows expected to be RED, and the silenced rows are GREEN by construction. Two different questions, one of them unasked. THE CARRIER FOR THE MISSING FACT ALREADY EXISTS AND IS INERT, which is what makes this one missing consumer rather than two problems. `std.witness_purpose` `WitnessPurpose` declares the authored taxonomy -- BehavioralDiscriminator, BoundaryCrossing, PopulationTotality, ExternalFidelity, ResourceContract -- landed under the operator's 2026-08-04 witness-cost-derives-from-purpose ruling, its own header stating that purpose is AUTHORED AND NOT INFERRED FROM IMPLEMENTATION. It is rostered in `v2.lens.inert_carrier` with the reason that it landed ahead of the consumer that derives witness size from it: zero witnesses declare one, zero consumers read one, and its only reference is its own taxonomy test `test.claim.witness_purpose_taxonomy_witness`. So the purpose vocabulary landed, the consumer slices never did, and in the meantime the required floor grew a cost mechanism that JUDGES ROWS WITH NO ACCESS TO WHAT ANY ROW IS FOR. The cpu_deadline population is unrankable for the same reason witness size is underivable. AN OBSERVABILITY FACT THAT MUST NOT BE RESTATED AS THE GAP, because this lane's first framing had it backwards and the correction is the load-bearing half. WHICH rows were preempted is ALREADY a joinable run product: `v1.cli_run` `write_required_floor_claim_cost_tsv` emits one row per EXECUTED claim carrying identity, module, outcome and `verdict_reached`, and the occurrence is minted in `v1.cli_run.required_floor_runner`'s claim loop BEFORE any classification branches, so preempted rows are present with `verdict_reached` false rather than dropped. The identities are not log-only. Reading the `INTERRUPTED-BEFORE-VERDICT` diagnostic lines as the population is `instrument_output_read_as_subject_content` and was committed twice in one lane. What is missing is not the population but the RANKING KEY over it. RECOGNITION RULE: when a mechanism reports that a check did not run, ask what the report lets a reader conclude about WHAT STOPPED BEING CHECKED. If the answer is nothing -- if a silenced wall and an open question produce the same row -- the mechanism counts non-executions without ranking them, and no amount of per-row cost detail supplies the missing fact. A second tell, which is what caught this one: a flag that looks like the distinction but is set on exactly one branch for a different reason. Read the SETTER before concluding a fact is represented. RUNG FOUND AT: mitigatable. The line does stop -- a non-verdict on a required claim blocks, typed and located -- so nothing is admitted that should not be; what is absent is the ability to rank what was lost. CEILING, and it is split rather than single because the two halves have different decidability. That every enrolled witness CARRIES a declared purpose is structurally guaranteeable: make the declaration mandatory at admission and a purposeless enrolled row has no constructor. That a declared purpose is TRUE of the row's body is undeclared intent and stays OUTSIDE the modeled guarantee -- observed and refused at a declared boundary, never inferred from the test body, which the taxonomy's own header forbids. Between them the join is mechanically preventable: a preempted row whose declared purpose is refusal-establishing reports as its own counted disposition, and rows with no declaration report as PURPOSE-UNDECLARED rather than as safe, which is the fail-closed direction. NEXT TRIGGER -- AN AUTHORED PURPOSE DECLARATION A FLOOR CONSUMER CAN JOIN AGAINST, and it is stated as the CAPABILITY because a trigger naming less gets satisfied while the capability stays dead. It must be sufficient for all three: (i) an operator ruling on whether refusal-establishing is a REFINEMENT of `BehavioralDiscriminator` carrying what the row requires to be refused, or a peer arm -- the coarse existing arm covers a positive control equally well, so spending it here would buy a key cited as coverage for a distinction it does not draw, which is the 4b(1) inflation that stops a class ever ranking for climbing; (ii) a purpose declared at IDENTITY grain that a witness authors, as a REAL DECLARATION BINDING A `DeclarationRef` TO THE ROW rather than a source annotation -- 4c forecloses the cheap version of this outright, because semantic passes receive only the ANNOTATION-ERASED PROJECTION, so an annotated purpose is unreadable by the floor BY CONSTRUCTION and would be a declaration no consumer could ever join against. That is 4c's own rule that an annotation is never evidence a machine claim holds, applied to this fact; it is recorded here so the annotation is not re-proposed as an economy later. And not a roster of interesting rows kept by hand -- this class has already retracted one hand-derivation described as a run product, and selecting a first population out of the non-verdict arm would be that shape a third time, since the selection would be derived from the very run product whose membership is redrawn per attempt; (iii) a floor consumer joining that declaration against `verdict_reached` and counting the undeclared remainder. THE CONSUMER DESIGN IS BLOCKED ON THE RULING AND IS NOT REJECTED ON MERIT -- recorded so the next lane does not re-derive it and does not read the absence as a refusal of the approach. NOT PROPOSED, AND EXCLUDED BY THE OPERATOR WHEN ASKED: raising the 500ms ceiling, widening a budget, moving rows to a laxer lane, or making the floor stop refusing on non-verdicts. Each hides the class rather than ranking it, and the last also deletes the refusal that makes the silencing detectable at all. This row is about what is REPORTED, never about what is ADMITTED. RELATED: `non_verdict_disposition_surfaces_as_refusal` carries the aggregate-boundary half, and the `gunbc.rung_drop` row `floor_cost_claim_qualification_unavailable` carries the cost half -- neither names the missing purpose join, which is why this is its own row. -- **a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. CEILING: 1, and the reason is DESIGN section 4b s own carve-out rather than a shortfall. The subject is external reality, which the ladder deliberately does not rank: it is observed, refused, or mitigated at a declared boundary and never fabricated. What CAN climb is the SEPARATION -- a conclusion about an outcome must not be carried in the same breath as an unobserved mechanism -- and that is a review discipline over prose, not a state a constructor can forbid, because section 4c guarantees no Accepted program reads an annotation. THIS CLASS IS DETECTABLE ONLY FROM OUTSIDE THE REPOSITORY, and that is the whole difficulty rather than an aside: the refuting evidence lives in the external system, so no lens, gate or witness reading this tree can reach it, and the class is invisible to every mechanism the repository owns. NEXT TRIGGER, and it is honestly UNDETERMINED rather than named, which is the fail-closed way to leave it. The capability question is what would have to be OBSERVABLE for a mechanism claim about an external system to be executable evidence rather than an assertion -- and that is not settled here. What can be said now: a carrier that states such a fact should carry the OBSERVATION that produced it -- the query, the population, the date -- so an unobserved mechanism is structurally distinguishable from an observed one and can be listed; `extdeps` already owns the shape for cited upstream facts. That is a necessary condition and it is NOT KNOWN to be sufficient, because a recorded observation of a system that can change its behaviour without notice is a receipt about a past world, which is section 4b's outside-the-modeled-guarantee column and not a rung. A TRIGGER NAMING THAT ROW AS THE CAPABILITY WOULD THEREFORE BE THE ARTIFACT-FOR-CAPABILITY SUBSTITUTION section 4b(3) FORBIDS, satisfied while the class stays alive. Until the question is settled this row is a reading discipline and citing it as coverage is rung inflation. +- **a MECHANISM about external reality is asserted as the reason for a conclusion that is independently CORRECT, so nothing the repository can execute ever refutes it** (INVALID STATE: a carrier states WHY an external system behaves as it does -- this platform suppresses that trigger, that endpoint rate-limits, this token cannot start a run -- and derives a design decision from it. The DECISION is right; the mechanism was never measured. HARM: DESIGN section 5 silent wrongness, and it is the immunised variety. A wrong premise attached to a wrong conclusion dies the first time the conclusion is tested. Here every test of the conclusion PASSES, so the premise is confirmed by association and hardens into the sentence later readers plan against -- and it is consumed for facts the conclusion never covered, which is where it is false. THE DISCRIMINATING QUESTION IS ALWAYS THE SAME: the conclusion says the good outcome does not HAPPEN; the mechanism says the machinery does not EXIST. Those differ exactly on cost and on remedy. If the thing exists and is merely withheld, something can release it, something already paid for it, and a second copy is a duplicate. RECOGNITION RULE, mechanical: for any prose of the form THE PLATFORM DOES NOT DO X, name the observation that would show X happening and say whether anyone ran it. If the only evidence offered is that the conclusion held, the mechanism is unmeasured. The sharpest tell is a mechanism stated in an ABSENCE form -- starts no run, sends no event, creates nothing -- beside a conclusion stated in an OUTCOME form; absence and non-execution are two states and the carrier collapsed them. DISTINCT FROM ITS NEIGHBOURS. `unbacked_execution_claim` is about an in-repository relation an authority could have backed and did not; here the subject is OUTSIDE the modeled guarantee, so no authority in the tree could have backed it and the only route is observation at the boundary. `state_space_conflation` names too few constructors for a modelled domain; here the domain is unmodelled and the prose supplies a two-state story for a three-state world. SPECIMEN (cool-koi-623, 2026-09-03). `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, GitHub suppressing that edge to stop a job triggering itself, and concluded that heal must exit nonzero rather than speak for a head nothing judged. The rung_drop row carries the correction; the ci_spec annotation still carries the refuted sentence AT THE TIME THIS ROW IS FILED, because that carrier is held by a concurrent lane and a second lane editing one premise from its own verdict is how one fact acquires two authorities -- recorded here as an observation rather than repaired here. The conclusion is correct and remains in force. The mechanism is false: over the whole heal-push population a pull_request run was CREATED 4 times out of 4, and it is EXECUTION that is withheld -- 0 of the 4 started a single job on the triggering attempt. The receipts and the re-derivation recipe are carried in that rung_drop row rather than restated here. WHAT THE FALSE MECHANISM CONCEALED, which is the harm made concrete: under starts-no-run a dispatched revalidation is free, and measured it is a SECOND run on that head whose check runs a name-keyed reader cannot separate from the held run s; and the human action that releases a healed head is an approve on that specific held run, not the re-run the annotation offered. A METHOD NOTE THAT IS PART OF THE CLASS RATHER THAN OF THE SPECIMEN: the first two readers of this population both read a run s TOP-LEVEL conclusion and its start timestamp and concluded the runs had executed. A run can conclude failure having started zero jobs, and a later attempt can execute after a human acts. When the subject is EXECUTION, count jobs on the attempt the event created, never read the latest attempt. RUNG FOUND AT: 1 ON AXIS (i) BELOW, mitigatable. The harm is contained because the conclusion the premise was offered for is independently sound; nothing was admitted that should not have been. A SECOND HARM THE SPECIMEN MADE VISIBLE AND THE CLASS SHOULD CARRY: the unmeasured mechanism was stated UNSCOPED, so the sentence is true at the moment it is written and can stop being true with nobody touching it -- here a held run may be released hours later and judge the head, at which point 'a head nothing judged' is simply false. Measure the mechanism, and then say WHEN the claim holds. THE SUBJECT OF THIS ROW IS A CARRIER IN THIS REPOSITORY, NOT THE EXTERNAL SYSTEM, and an earlier revision of this row got that backwards -- corrected here rather than annotated, because the error is exactly the one section 4b's carve-out exists to prevent. That revision assigned a LADDER RUNG to external reality, which section 4b deliberately keeps OFF the ladder, and then declined to name a trigger; between them those two moves let 'we do not model GitHub' stand where a rankable in-repository defect actually sits. The invalid state is an AUTHORING ACT that is wholly in the tree: a carrier states an unobserved mechanism as the reason for a decision. That is decidable from the carrier alone, so it ranks, and it is obligated to climb. TWO AXES, WITH DIFFERENT CEILINGS BECAUSE THEY HAVE DIFFERENT DECIDABILITY, and only the first is a ladder subject at all. (i) THE SEPARATION -- is this mechanism claim backed by an observation? Decidable by reading the carrier. CEILING: 4, structurally impossible, and DERIVED rather than aspirational: if the only construction able to express an external-system mechanism requires the observation that produced it, an unbacked mechanism claim has no constructor, and validation becomes unnecessary because the bad state cannot be written. Anything below 4 on this axis is a correctness gap, not a ceiling. (ii) THE TRUTH of the external fact -- whether the observed behaviour still holds. OUTSIDE THE MODELED GUARANTEE, not a rung and never one: observed, refused or mitigated at a declared boundary, never fabricated. It is named here precisely so it cannot be mistaken for a weak implementation that should climb. NEXT TRIGGER FOR AXIS (i), NAMED AS THE CAPABILITY AND NOT AS AN ARTIFACT: an external-system mechanism claim is expressible ONLY through a typed construction carrying the observation that produced it -- the query, the population, the date -- together with a consumer that ENUMERATES carriers stating such a claim without one. The pairing is the whole trigger: the construction alone makes the honest form available, and only the enumerating consumer makes the dishonest form unwritable rather than merely noticed once. Authoring one such row by hand discharges nothing and is the artifact-for-capability substitution section 4b(3) forbids. It is CAN-CLIMB-NOW-BUT-UNBUILT rather than blocked on grounding: `extdeps` already owns the shape for cited upstream facts. SECTION 4c DECIDES WHERE THIS CANNOT LIVE, recorded so the cheap version is not proposed later as an economy: semantic passes receive only the annotation-erased projection, so an annotation can never carry the observation and the construction must be a real declaration. WHAT THE DISCHARGED TRIGGER DOES NOT BUY, stated so it is not read as covering axis (ii): every mechanism claim would then carry a receipt, and a receipt is not currency -- a system that changes without notice makes any observation a statement about a past world. That residual is axis (ii) and stays outside the guarantee by construction. WHAT IS ASYMMETRIC ABOUT THIS CLASS, and it is why it survives review rather than why it cannot be ranked: the DEFECT is visible from inside the tree -- a claim with no observation beside it -- while the REFUTATION lives in the external system and no lens, gate or witness reading this tree can reach it. So the class is detectable here and falsifiable only there, which is what lets a wrong mechanism sit unchallenged beside a correct conclusion for as long as nobody goes outside to look. Until axis (i)'s trigger is built this row is a reading discipline and citing it as coverage is the rung inflation section 4b(1) names.