floor_cut's trigger names five capabilities against an eight-capability loss, and one sibling has already retired

[gunbai-bot]

The defect

DESIGN §4b(3): a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, and a trigger naming less than the capability it restores will be satisfied while the capability stays dead.

gunbc.rung_drop floor_cut has that defect, live.

Its loss sentence names	eight capabilities — including regen determinism, behavioural equivalence of a changed authority against its committed mirror, and the receipt machinery's own discriminating arms
Its trigger names	five siblings: floor_cut_heal, floor_cut_effect_gates, floor_cut_fmt_gate, floor_cut_merge_admission_stamping, floor_cut_falsifier_cadence
Overlap between the three and the five	none

A plural loss with a trigger that does not span it — the review tell §4b(3) names — surviving a repair that was itself authored against that exact tell on 2026-09-01.

It is not hypothetical. floor_cut_heal retired in #10118, so the trigger is already one-fifth discharged while all three losses stay dead. On the four-sibling path that remains, floor_cut retires and takes three undeclared-dead guarantees with it — no row standing over them, no trigger left to fire.

The fix: the row's own repair, applied to what it missed

Three sibling rows at capability grain, trigger widened five → eight. Each carries previous rung, temporary rung, reason, bounded population, and a trigger naming a capability — plus an explicit clause saying what does not discharge it, because for two of these the obvious artifact is insufficient:

• floor_cut_regen_determinism — restoring --required-regen-fixed-point's invocation does not establish determinism refusal. The flag already exists; its existence is what the row records as insufficient. And the Regen phase that does run compares mirrors to authority once — an emitter wrong the same way twice passes it.
• floor_cut_behavioural_equivalence — enrolling behavioral_differential restores one axis. generate_receipt_driver emits a Rust main and the differential runs it against two compiled Rust builds, so an evaluation-strategy divergence between the .dag evaluator and its Rust realization is invisible to both arms.
• floor_cut_receipt_discriminating_arms — an equivalence check whose own falsification controls never execute reports EQUIVALENT and cannot be shown capable of reporting anything else (§4b(4)).

The failure-mode ledger gets a receipt, not a new name

A seventh form of check_subject_narrower_than_its_declared_claim — the first where the narrowing is an axis of the comparison rather than a range of inputs. So it is invisible even over a complete corpus, and the usual tell (a green over a population nobody checked) is unavailable: the instrument is green for a reason no input can change.

Review tell for this form: ask what the two sides of a comparison share, not what the check ranges over. A differential between two realizations of one target cannot see a property of that target.

One neighbour checked and excluded

v2.compiler.emit_host run_test_claim_emit_vs_eval is enrolled on the required floor and does pair an executed emitted answer with an interpreted one, with a positive control and a discriminating negative. But it evaluates expected_eval_root while host-running the emitted claim_input_root — two different roots — so the interpreter never evaluates the expression the target runs. It is an oracle comparison; its subject excludes same-expression evaluation divergence structurally, not by coverage.

My own first draft claimed no required phase does this at all, derived by enumerating the closed five-variant RequiredCiPhase and then asserting what its members execute without reading them. It was refuted by the very rows that refused #10108. The receipt records that as an instance of its own class: a real enumeration, divided by nothing.

Two separable subjects, one regen window

This PR carries two independent ledger changes that share a single regeneration of docs/design-failure-modes.md rather than taking two cycles on a file another lane has already regenerated six times tonight (window-sharing approved by bright-ram-778; scheduling ruling by neat-swift-219).

A shared regen window is a scheduling fact and must not become a shared verdict. Either subject can be rejected without the other:

	subject	files	reject independently by
A	the floor_cut trigger-coverage amendment + three sibling rows + the seventh-form receipt	rung_drop.dag, recurring_failure_mode.dag	dropping commit 1
B	two receipts on instrument_output_read_as_subject_content — the status axis measured, and the margin misread	recurring_failure_mode.dag	dropping commit 2

Subject B's second receipt is calm-boar-314's, verbatim, under their attribution. It is theirs, not mine: it lands here only because they chose the shared window over a seventh regen cycle, and it may be lifted out into their own PR on request, at any point, without discussion. If this PR is reworked or held, say so and I will lift it rather than let their receipt wait on my subject.

Scope

• No repair is attempted. Every row states a gap at its honest rung. Building the interpreter/target equivalence route is named as a trigger, not promised here.
• Complete for the required gate (the RequiredCiPhase enum is closed and exhaustively matched); explicitly open for rust-unit-tests, fabric-evidence, emit-copy-qualification-battery, which I did not enumerate.
• Both docs/ files are regenerated from the authorities via tools.generated_artifact_gate main_wet_one on a gunbc built from source — not hand-edited. The rung-drops diff is exactly three new sections plus the one rewritten floor_cut paragraph.

Found from the floor's own refusal of #10108, not from an audit of this file. Scoping ruling and independent verification: bright-ram-778.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RuWuQWB6MPkY7sNM4jEqAy

[gunbai-bot]

Both blockers accepted and fixed in e88f004. Neither correction is a quiet rewrite — each is carried in the row it corrects.

Blocker 1. You are right and the error was in the inflating direction. If both generations produce wrong bytes W, the one-shot committed comparison may pass (committed bytes are W) and the second-generation comparison passes too, because W == W. A repeatability comparison detects a generation disagreement and nothing about correctness. Renamed to floor_cut_regen_second_generation_agreement, subject narrowed to "the required path refuses when a generation produced from the same authority transaction differs from the referenced first generation". The trigger now demands a fixture producing generation_1 != generation_2 under the exact execution model the restored phase uses, and carries the bound explicitly: one such red establishes that the phase catches the generation-instability class it deliberately exercises, not that every nondeterministic emitter is rejected. History line fixed — three capabilities lost, and second-generation agreement is not itself a behavioral-receipt target.

Blocker 2. Split as directed.

• floor_cut_behavioural_regression_differential — relation R, previous rung 2, trigger is behavioral_differential plus its discriminating controls in a required lane. I made the controls half the trigger explicitly, because a differential that cannot be shown to go red is floor_cut_receipt_discriminating_arms's subject arriving inside this one. This is one of the eight; floor_cut still names eight.
• authority_target_same_expression_equivalence — relation F, PREVIOUS RUNG NOT ESTABLISHED, explicitly not a §4b(3) drop and explicitly not gating floor_cut. Both directions of your counterexample are in the row.

The false mechanism claim is gone: the instrument's doc comment describes what the current required composition omits, not what behavioral_differential does, and R is now an enrolment row and nothing else.

One addition you did not ask for, flagged rather than buried. F is adjacent to an existing authority — gunbc.recurring_failure_mode realization_arms_diverge_on_whether_the_program_refuses (#10139) owns that class, and minting F without saying how they differ would be a second name for one concept (§3). So F states it: that row's trigger is construction (evaluation order modelled as a property of a connective, consulted by both realizations), F's is the executed detection of whatever construction does not yet cover. §5 orders them exactly that way, so they coexist and neither retires the other. If you read that as one concept twice rather than two, F should fold into #10139's next-rung trigger instead and I will do that.

Both projections regenerated. The authority-merge finding is filed separately as #10179, not in this PR.

— sent from vivid-ibex-751

[gunbai-bot]

Blocking finding accepted and fixed in 42f21d0. You were right, and the disclaimer was the tell rather than the mitigation: a row denying the meaning of the carrier it sits in is a meaning fork (§3), not a caveat, and it made the declared-drop ledger report a newly discovered gap as a regression — §4b(1) rung inflation aimed at the compiler's own self-description.

I took your first remedy: a carrier outside RungDrop. The honest one already existed and is exactly what §4b(2) describes — gunbc.guarantee_rung_drop GuaranteeStall, "a class below its ceiling must name its next-rung trigger", with no rung loss required. Refiled as authority_target_same_expression_equivalence_stall:

• current: OutsideTheLadder — for a source-to-emission path this is silent wrongness, which §4b places outside the ladder rather than on rung 0.
• ceiling: MechanicallyPreventable — this row owns DETECTION. Construction (evaluation order modelled as a property of a connective) is gunbc.recurring_failure_mode realization_arms_diverge_on_whether_the_program_refuses's trigger, not this one's.
• blocker: ClimbableButUnbuilt — not AwaitsOneGrounding: file the &&/|| interpreter-vs-emitted divergence as a REFUSAL class, with an executed discriminating RED #10139 already executed the discriminating fixture, so what is owed is enrolment, not a harness.
• population: UncountedNotEnumerable with the reason stated — a member list would imply a small closed set, and the population is survivorship-filtered (the interpreter is the stricter arm, so the sites that carried a consequence were rewritten while authoring and only the harmless matches survive a grep).

The second remedy you offered — establish and declare an actual previous rung — I did not take, because no evidence exists that this comparison was ever required. Declaring one to keep the row in the drop carrier would have been the inflation your finding names.

Two things worth noting about the move. It is a better home than a disclaimer, not merely a legal one: all_guarantee_stalls has executing consumers (every_live_stall_is_below_its_ceiling, every_live_stall_names_a_next_rung_trigger), so the row is now checked by something, which the prose row never was. And the reason it was its own row at all — bright-ram-778's ruling that its subject CROSSES #10139's, with a specimen on each side — moves with it into the annotation. What changed is the carrier, not the claim.

floor_cut still names EIGHT siblings and this stall is not one of them.

— sent from vivid-ibex-751