Record that the floor-crosser premise is measured false, where the next reader of "the floor is a coin flip" will hit it

[gunbai-bot]

Documentation only — one section appended to docs/plans/floor-cost-distribution-near-the-ceiling.md, which is a hand-authored plan (the floor_cost_distribution modules reference it; it is not generated from them). No .dag change, no code change.

Why this exists

The work item behind the #10133 follow-up was "three (later seven) self-host witness modules sit above the 500ms hard CPU ceiling, making the required floor lane a coin flip." Measured, no fixed above-ceiling identity set exists — completed green runs place this family's band below 500ms, while run variance can carry its top across (four completed-over-cost rows were observed at 506–515ms). What is retired is that the family is intrinsically above the ceiling; a row does not stably "sit" on either side of an attempt-safety boundary. The crossings themselves are real and recur. Both remedies v2.workflow.required_floor names are refused for this family on evidence, and the ceiling is correctly denominated.

That result existed only in a session thread, and session threads archive. It is written into §5's own open question because the reader who re-forms this belief will arrive from the same symptom — a red floor lane naming a handful of emit rows — and re-deriving it is a night's work.

What the section records

Three misreadings, each with the control that exposes it. These are the reusable part; the ratios are not.

• An interrupted_before_verdict figure is the budget, not the row. The deadline preempted the measurement, so every interrupted row reports approximately whatever ceiling stopped it — a set of them looks like a tight cluster "just over" regardless of the true costs. Only completed_over_cost_requirement rows carry costs.
• The crossing set is not the expensive set. The row that passed on CI in one module is the most expensive of its four siblings. Repairing "the rows that crossed" fits noise; the non-crossing siblings are what reveal the band.
• A one-anchor local→CI factor does not transfer. A factor from a single identity predicted a row comfortably under the ceiling that CI had in fact interrupted.

Both remedies refused for this family. Reduce-what-it-reaches-for is refused by measurement — no component is unneeded, the fixture is free, and both cost-shape defects were looked for and are absent. Enroll-in-a-lane has no home: every candidate either withholds rows from execution (floor_cost_debt, shrink-only and closed to new crossers) or names a cadence with no workflow.

The subject, restated. The surface sits at roughly two-thirds to four-fifths of budget on a normal run, with CI run-to-run variance large enough to carry its top across the line — so which rows cross is a property of the run, not the rows.

Conventions observed

• §6 name the instrument, do not transcribe. The join needs an axis the §5 instrument does not read, and no authority owns it — so the recipe is given at identity grain and that absence is stated as a gap rather than papered over. Ratios are described by shape and stability across named run classes.
• The attribution hedge is preserved verbatim: the projection term is measured at the target_project_arrow_body_to_value_expression frame and attributed by elimination to the primitive-apply step beneath it, with each neighbouring candidate named as measuring zero (the two table-shaped ones tested with inputs that would expose a build even on a miss).
• The live lead is left undetermined on purpose — a memo keyed above the body vs a one-time warm want different providers, so the mechanism must be separated before any provider is proposed. Both prior sharing attempts are recorded with their refutations so neither is re-proposed.

A value check is recorded too: x + y and y + x project to different values, carrying a positive control that the equality works and a by-construction-false row proving the harness reports failures at all — a cheaper-looking result that lost operand order would have been a correctness defect, not a saving.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WEFMasGn2cAGCMJW2694pb

[briansrls]

HOLD on exact head 3d25d7a for one false stable-subject sentence. The opening and PR body say, “Measured, no row in that family sits above the ceiling.” The section's own evidence later says the failed-run inflation carries the top of that same band across 500 ms, and its central finding is that cost/crossing is attempt-dependent while interrupted rows are unmeasured. A row therefore does not stably “sit” above or below this attempt-safety boundary.

Please replace that claim everywhere it appears with the proposition actually established: no fixed above-ceiling identity set exists; completed green runs place the family's band below 500 ms, while failed-run variance can carry its top across. Equivalently, retire the claim that the family is intrinsically above the ceiling, not the observed crossings. The rest of the memo—including the interrupted-reading and crossing-set controls—stands.

[gunbai-bot]

Fixed in 297d61b, and the finding is correct — the verb was the whole defect.

"Measured, no row in that family sits above the ceiling" asserts a stable row property, while the section's central finding is that crossing is attempt-dependent. So the opening claimed exactly the shape the body spends four subsections dismantling, and its own evidence refutes it: failed-run inflation carries the top of the band across 500ms, and completed-over-cost rows were observed at 506–515ms.

The section and the PR body now say the proposition actually established: no fixed above-ceiling identity set exists — completed green runs place the family's band below 500ms, while run variance can carry its top across. What is retired is that the family is intrinsically above the ceiling; the observed crossings are real and recur, and the 506–515ms figures are named inside the retraction so the correction cannot be read as denying them. The heading changed for the same reason ("the crossers are not above the ceiling" was the same stable-subject shape one line up).

Nothing else moved. The two other scoped statements were already bounded correctly — the restated subject says "on a normal run" and "a property of the run, not of the rows", and the emit_host_fold example is scoped to "every green run in the join". The re-derivation recipe, the three misreading controls, the eval_steps axis and the producer-share caveat all stand.

Worth recording as a class rather than a slip: when a subject's true form is a distribution, ordinary language keeps snapping it back to a property, and it does so in both directions — the same data produced "the rows are genuinely under budget" elsewhere within the hour. Neither sentence survives its own evidence.

— sent from warm-ibex-636