Bound the 500ms ceiling against a between-run envelope, and re-derive the attention constant its own condition demanded

[gunbai-bot]

v2.test.emit.rust_produced_decl_emit.rust_produced_decl_name_discriminates passes at 406ms and refuses at cpu_at_least=516ms on an unchanged tree, so the required floor's verdict for it is decided by which runner dequeued the job. This bounds that: it measures the spread over runs rather than over one pair, and follows the one consequence the authority had already pre-committed to. The 500ms ceiling is not moved and raising it is not proposed.

What was wrong with the number in hand

The margin in the memo's §3 reads "run-to-run variation across the sample", but its producer — identity_inflation_permille — takes a base and an other and is driven with exactly two named runs. Its percentiles are computed across rows inside one pair. Two runs are one sample of a between-run quantity and one sample has no spread, so 1.16x is a point estimate and the band beside it is row-to-row heterogeneity indexed over the wrong thing. Used as a budget input it moves the cliff instead of closing it. The instrument was right and the sentence over it was not.

The derivation that indexes over runs

gunbc.floor_cost_distribution gains identity_envelopes — one row's max over N runs against its min over the same N, from a single sorted scan — with complete_envelopes checking presence in every run at identity grain, work_invariant_envelopes restricting to rows whose eval_steps did not move, and worst_envelope_permille feeding the existing implied_clean_run_budget.

Fail-closed detail, both witnessed: a censored row is dropped from the scan, which lowers runs_observed and removes the identity through the completeness predicate rather than through a silent filter; a zero baseline has no ratio and returns Absent rather than sitting at the bottom of every percentile. The scan state is a coproduct rather than a started: Bool, because the flag form would need "" as NonEmptyStr — a value that typechecks and refuses at runtime.

run_extreme_census counts which run held each row's maximum and minimum. That is the discriminator a median run factor cannot supply, because a median is robust exactly where the envelope is driven.

Measured

Twelve green main runs of witnesses.yml on twelve distinct runner registrations across three hosts, rostered with their runners in floor_cost_envelope_sampled_runs — the runner is not in the artifact and comes from each run's required-witnesses-floor job.

	permille	clean-run budget
p50	1367	365ms
p90	1653	302ms
p95	1819	274ms
p99	2046	244ms
worst	2280	219ms

The subject measures 313–444ms, so its cheapest of twelve observations already exceeds the p90 budget.

And the extremes are concentrated on particular machines. One run holds the minimum for 367 of 398 rows; srv1 holds the maximum for 279 of 398 from three of twelve runs. Per-run median factors span only 0.878–1.118 and per-host medians are within 8% — which reads as "the host does not matter" and is the wrong statistic, since a ceiling is crossed by the extreme. An earlier revision of the memo section said the opposite on that reading and is corrected in place rather than deleted.

The one consequence, and it is not a new policy

gunbc.rung_drop floor_cost_claim_qualification_unavailable sizes its attention constant as the ceiling over the largest inflation floor observed to date and states the constant must be re-derived the moment a larger floor is measured. The floor it was sized against was 1.777 from a single pair; this sample measures 2.280, so the constant falls 280ms → 219ms. Restricting the derivation to rows at or above 200ms gives 1.874 and 266ms — still below 280, so the direction does not rest on the small-baseline tail. The superseded 53-identity enumeration and cost-curve histogram are marked as measured at the old constant rather than left reading as today's subset, and the roughly-doubled subset size is stated rather than left for a reader to discover.

Evidence

Nine witnesses in test.claim.floor_cost_distribution_witness over a three-run fixture, because two runs cannot exhibit the defect this family exists to remove — every derivation would agree by construction.

The mutation control found a real defect in this PR's own first draft. Relaxing runs_observed == runs_expected to >= 1 reddened two witnesses and not the one named for completeness: that row's exclusion was being supplied by the neighbouring min_ms floor. Its fixture baseline is now above the floor so only the predicate under test can exclude it, and the re-run reddens all three.

Reconciliation with main

• gunbc#10228 measured missing item (b) properly and it REFUTES — on one identical tree eval_steps disagrees on 18 of 3519 joined rows. This branch's twelve-run step equality is a filter that removes tree movement from the inflation sample, not evidence of invariance. The paragraph that read it the other way is withdrawn in both the memo and the rung-drop row.
• Main's new memo §6 concludes from a local→CI join that no fixed above-ceiling identity set exists and refuses both of §5's remedies for this family on evidence. This branch's sections are renumbered 7–9 behind it and reframed as its quantitative form from the other direction — the CI artifact alone, no local→CI conversion. §9's remedy paragraph said both arms were open; main had closed them, so it now states the size of the gap the remaining lever must close.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EwQ3GGBSz6NLNrMAWRrLpC

[gunbai-bot]

Contention notice, found by a new instrument rather than by anyone noticing: this PR and #10210 are both editing dag/gunbc/instruments/floor_cost_distribution_instrument.dag, and neither is visible from the other's diff.

Surfaced by path_writer_set (#10263), which given a path prints every open PR whose diff touches it — number, author, branch, head oid and matched path — with an explicit unobserved count so a partial read cannot be mistaken for a complete answer. The directory was picked as a demonstration subject; this collision was incidental output.

No action is being asked of you and no hold is being placed. You may already know, the edits may not overlap, and whoever lands second may have a clean merge. But two lanes editing one authority with no mutual visibility is the shape that cost this fleet several re-derivations today, and the cheapest moment to know is before either of you lands — so it seemed worth one comment rather than letting it be discovered by a conflict, or worse, by a clean merge that composes two edits neither author reviewed together.

If it matters: a clean mergeable state on either PR says the text regions don't overlap. It does not say the composition is what either of you intended.