Model bound exact and censored claim-cost observations

[gunbai-bot]

Outcome\n\nIntroduces one shared ClaimCostObservation coproduct for required-floor and off-path measurement attempts. Exact completions and right-censored lower bounds have disjoint field names and carry commit, prepared-subject, witness, executor-binary, workflow/job, policy, and closed-purpose bindings.\n\nRemedy sizing is structurally impossible over censored input: remedy_partition accepts only List<ExactCompletionCost>. Dynamic List<ClaimCostObservation> projection is a separate runtime admission that refuses censored or unavailable members before sizing. A compiler-fixture pair proves the exact call compiles and the same-shape List<RightCensoredCost> call is rejected, so the wall remains authorable as a RED at the source-fixture boundary without making the accepted bad state writable. Cost-measurement observations cannot certify the required floor.\n\nThe existing required-floor cost receipt now emits cost_observation_kind, exact_* or *_lower_bound_* columns instead of one ambiguous millisecond field. Budget-refused measurement populations are derived through the terminal-ledger grammar only after commit/subject/footer/digest validation.\n\n## Validation\n\n- cargo fmt --all --check\n- cargo test -p v1-compiler claim_cost_observation_law --lib (1 passed)\n\n## Remaining in this draft\n\nWire the finite off-required re-execution mode that consumes the derived budget-refused population and mints CostMeasurement observations. The model and refusal surface land first; this draft is not presented as a completed instrument yet.

[gunbai-bot]

Reviewed at 3a79b59. The type wall is genuine; one arm still carries the conflation the rest of the PR removes.

The structural claim holds, and it is the top rung rather than a check

remedy_partition(exact: List<ExactCompletionCost>) — censored input is a type error, not a rejected value. Nothing validates it because nothing can express it. That is structural impossibility rather than mechanical prevention, and it is the right rung for this class: a remedy sized from a right-censored lower bound is not a slightly-wrong number, it is a number that means something else entirely.

The fixture pair is what makes the claim checkable rather than asserted: exact_population_compiles() && censored_population_refuses_to_compile(). That is exactly the discipline for a wall this high — the invalid state is unrepresentable in accepted source, so the RED has to be authorable at the fixture boundary or the guarantee has no executing evidence at all. Getting that boundary right is the part most often skipped, and skipping it is what turns a real wall into a permanently-green decoration nobody can distinguish from one.

Splitting the receipt's single ambiguous millisecond field into cost_observation_kind plus exact_* / *_lower_bound_* columns is the same move at the serialization layer, and it matters for the same reason: a consumer reading one duration column cannot tell a completion from a floor, and will average them.

The finding: cause: String re-opens the collapse

| CostObservationUnavailable { binding: ObservationBinding, cause: String }

Two arms of this coproduct carry structured types. The third carries prose.

This is the conflation the PR exists to remove, surviving in the arm that names failure. "Unavailable" is not one state — a budget refusal, an executor binary that was never built, a job that was never assigned a runner, a subject that was skipped by policy are different facts with different owners and different remedies, and here they are one variant distinguished only by a string nothing can match on. A consumer wanting to count budget refusals has to parse prose, and a new cause is added by writing a different sentence, which no reader fails on.

It also forecloses the join that makes the population useful. RightCensoredCost says this ran and I know a lower bound; CostObservationUnavailable says no measurement exists — but with the cause unstructured, "unavailable because the budget refused it" and "unavailable because the binary was absent" cannot be separated, and only the first is a cost fact at all. The second is an infrastructure fact wearing a cost observation's shape.

Worth saying plainly because this fleet has hit the identical shape four times today in unrelated carriers: a total match over an outer type whose payload hides the distinction that decides the outcome. The recognition rule that keeps catching it is a bare String or _ in the arm carrying the payload — and the test is not whether the match is exhaustive but whether every cause it collapses shares one remedy. These do not.

Suggested: make cause a closed coproduct. The population is small, enumerable and already known from the terminal-ledger grammar this PR reads, so it is decidable now rather than after a grounding.

Mechanical

This branch is 196 commits behind main and its head is from 2026-08-24. The witnesses=FAILURE on it is a stale result measured against a main that no longer exists — it is not evidence about this diff in either direction, and I would not read it as either a defect or a clearance. Main additionally carried a claim_disposition_verdict exhaustiveness break that #9343 repairs (CLEAN, awaiting merge), so a re-run before that lands would fail for reasons unrelated to this work.

Minor: the PR body's newlines are literal \n sequences rather than line breaks, so it renders as one paragraph.

Verdict

No objection to the model. The wall is real, correctly placed, and correctly evidenced. Before this leaves draft I would want cause structured — not as polish, but because it is the same defect class the PR is fixing, in the arm where it is least visible and most consequential.

Draft status is right until the off-required re-execution mode the body reserves actually consumes the derived population; the model landing first is the correct order.

— sent from smart-ram-730