Skip to content

Demand-side contention: delete priority_class, rank demands by derived margin per billed second - #9395

Merged
briansrls merged 8 commits into
mainfrom
session/keen-bat-142
Aug 27, 2026
Merged

briansrls merged 8 commits into
mainfrom
session/keen-bat-142

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 27, 2026 •

Copy link
Copy Markdown
Contributor

The finding

AdmissionTerms.priority_class was a NonEmptyStr. Nothing read it, nothing could
compare two of them, and SupplySelectionPolicy had one member — so the fabric could
not say which demand wins scarce capacity.

The move: delete, do not brand

The tempting repair is a closed PriorityClass coproduct, or a branded scalar. Both are
DESIGN §2's anemic leaf one layer up: a bare ordinal is a nickname for a number, and it
still tells you nothing about why one demand outranks another. So priority_class is
deleted, and rank is derived from facts the two sides already state:

  • the buyer's reservation_price and maximum_buy_order (demand.dag, unchanged),
  • the supplier's quote and billing quantum (supply.dag, unchanged — the hard boundary
    with the supply lane was not crossed; SupplySelectionPolicy is untouched).

New module product.fabric.contention, ~1 file, plus 21 witnesses.

The ranking key

Buyer headroom per billed second.

  • buyer_headroom = the buyer's ceiling minus the projected bill for this offer. It is a
    fact about the BUYER's remaining willingness to pay, not the fabric's margin — an earlier
    revision of this PR called it a margin and that was an overclaim (review 56530), since the
    fabric has no authoritative buyer-charge carrier to compute a margin against.
  • the denominator is billed_seconds, which reads the offer's quantum. A 90-second job
    on an hourly machine occupies 3600 billed seconds; on a quantum-0 continuous machine it
    occupies 90. That is why the ordering is a property of the pair, not of the demand:
    the same two bidders rank oppositely on continuous and hourly supply, and that is the
    flagship witness.
  • comparison is cross-multiplied integer arithmetic (h_a * b_b vs h_b * b_a) — exact, no
    division, no rounding, and it routes through std.pareto's axis_comparison under
    HigherIsBetter rather than minting a second ordering authority.

What refuses instead of answering

Every arm is typed and located; none widens, none defaults.

  • DemandNotAffordable — carries the supply lane's own affordability refusal, matched arm
    by arm rather than collapsed to a Bool.
  • QuoteExceedsReservationPrice — clearing the grant ceiling is not clearing the buyer's
    own price. Two different facts, two different refusals.
  • GrantOccupiesNoBilledTime — a grant that bills no time is refused, not ranked at zero.
  • DemandsIndistinguishable — a tie refuses rather than letting arrival order decide.
  • DuplicateCandidateIdentity, CandidatesJudgedAgainstDifferentOffers — a field that was
    never a field refuses instead of comparing incomparables.
  • OrderingContingentOnUnreadOpportunityCost — the one worth reading. When the rate
    leader is not also the total-headroom leader, the two orderings disagree, and which one
    is right depends on a fact the fabric does not hold: what the machine would earn in the
    time the bigger job forgoes. The fold does not pick one and annotate it. It refuses, and
    names both the rate leader and everyone who outbids it on total. Selecting and annotating
    was the first shape and it was wrong — an annotation cannot authorize.

Unknown duration

Per the operator ruling: the fold does not assume a known duration in its signature. It
reads GrantDuration's own arms and classifies provenance into OccupancyBasis
(MeasuredOccupancy / ProjectedOccupancy), which inhabits BoundedLattice with
ProjectedOccupancy as bottom — so a field's basis is a meet fold, and one estimated
member degrades the whole selection's evidence. That is the DescentEvidence precedent,
fail-closed at bottom, not a conjoined Bool.

Provenance is read from the duration, not from the affordability verdict: measured,
offer_affordability_for answers plain Affordable for an EstimatedGrantDuration under
QuotedFlatPerGrant, so inferring estimate-ness from affordability was a real defect and is
fixed. The match is deliberate so a third GrantDuration arm breaks the fold loudly.

Scope boundary, declared

This ranks demands against one offer. It is not the assignment problem: a joint field
over many offers and many demands is a separate construction and is not claimed here.
Likewise the remainder/spill question — what a 7-minute remainder is worth against an
unbounded job — is priced by the supply lane's CommitmentHorizon, and the witness that
retires this lane's declared absence lands with it, not here.

Evidence

21 witnesses in test.claim.fabric_contention_witness_test, every run paired with a
deliberately-false instrument control that must return false in the same invocation.

Mutation, measured against this tree (not transcribed from an earlier one): forcing the
comparator back to total headroom turns three of the twenty-one red —
a_larger_total_margin_loses_to_a_larger_margin_per_billed_second,
a_free_offer_is_still_ranked_by_bid_per_second_not_by_bid, and
a_contingent_ordering_refuses_and_names_both_candidates — with eighteen green and the
control still false. The third one only reds because the contingent case moved its answer
into the refusal payload; the comparator is observable there too.

Call sites

AdmissionTerms had 5 match/literal sites; all 5 are edited. The 7 new types have zero
match sites outside this PR's two files.

Merge order

#9397 lands first. It puts the estimate/exact distinction on GrantDuration itself and
adds UnobservedGrantDuration. After it merges I rebase, let this fold break, and answer
that arm with a typed refusal naming the measurement obligation — a spill bound is the right
answer for pricing and the wrong answer for a denominator, since it would manufacture
DemandsIndistinguishable out of unmeasured.

Brian Searls added 2 commits August 27, 2026 03:00
… per billed second

The fabric could say which offer serves one demand and had no vocabulary at all
for which demand wins one offer. Scarce is the normal state, so the choice fell
to whichever caller folded first.

AdmissionTerms.priority_class was a bare NonEmptyStr that declared an ordering
and carried none. It is DELETED rather than branded or replaced by an ordinal
tier: a brand leaves a magic value agreed between producer and consumer (the
shape gunbc.fabric_capacity_class_gap already refuses for the supplier-side
capacity class), and High/Medium/Low is a nickname for a number that says one
demand outranks another and never why. A requester-stated rank is fail-open by
construction.

product.fabric.contention is a PEER of SupplySelectionPolicy, not a second
member of it: supply ranks OFFERS for one demand, contention ranks DEMANDS for
one offer. supply.dag is unmodified.

The rank is derived from the pair: reservation_price minus what serving this
demand from THIS offer bills, over the BILLED seconds it occupies. Billed
rather than elapsed is what makes it one derivation instead of a mode switch --
under an hourly quantum two jobs inside one hour have equal denominators and
the rate ordering collapses onto the total-margin ordering, which is correct
there because the rounded-up hour is not resellable; under a continuous quantum
the offer is released when the grant ends, so occupancy is the scarce thing and
the rate is right. Comparing total margin always would be the hourly answer
applied to every mode.

AdmittedDemand is sole_constructor with admit_demand_for_offer as its only
route, so "a class must not admit a demand that cannot afford it" stops being a
prose note beside a string and becomes unwritable. Admission also enforces
reservation_price, which nothing consulted before -- supply.dag screens
maximum_buy_order only, so a quote could sit above the price the buyer named
and still read as affordable -- and that is what keeps the margin representable
over Nat rather than underflowing.

Every case the policy cannot decide refuses: a tie, a duplicated candidate, a
field judged against two offers, a grant billing no time. No deadline or
urgency axis ships, because Timestamp is a String alias with no order.
…he affordability verdict

The rank's denominator is billed seconds, derived from the grant duration, so
an estimated duration makes the denominator a projection and the rank a weaker
claim. This carried that fact from the wrong authority.

offer_affordability_for answers plain Affordable for an EstimatedGrantDuration
whenever the quote is QuotedFlatPerGrant -- correctly, because a flat per-grant
quote does not depend on how long the grant runs. The occupancy denominator
does. So that pair produced a projected denominator carrying a verdict saying
nothing had been projected: one authority borrowed to answer another's
question, both halves individually true and only the arrow between them
invented. OccupancyBasis is now classified from GrantDuration's own arms.

THE CLASSIFICATION IS A MATCH WHERE A CALL WOULD HAVE BEEN SHORTER, and that is
its whole purpose. grant_duration_seconds already extracts seconds from either
arm. Matching means that when supply.dag gains an unobserved-duration arm --
which the operator's 7-minute-VM ruling requires and which has no spelling in
GrantDuration today -- this fold STOPS COMPILING and someone has to decide what
contention does with a duration nobody measured. A call would keep working and
keep answering with a number: the absorbing fallback, where the deficit's
frequency is zero by construction. The unobserved arm is not modeled ahead of
its carrier, because a refusal for a state with no spelling would be
permanently unreachable and would read as coverage. It is declared as the
next-rung trigger, owned by the supply lane.

The selection carries the basis of the WHOLE FIELD, not of its winner: a winner
with an exact duration can still have beaten a rival whose denominator was
projected, in which case the ordering rested on a projection though the
selected demand did not, and reading the winner's own basis gives the opposite
answer. Reported rather than refused, because an estimate is frequently all
anyone has; what must not happen is the projection going unrecorded.

Also corrects a prose claim this branch got wrong. The note on the
margin-versus-rate witness said reverting the comparator to total margin turns
that one witness red and leaves every other green. Measured by running the
mutation: TWO go red -- that one and the paid-through zero-quote witness -- with
the other twelve green and the instrument control still false.
…ency it rests on

The paid-through witness showed the rate comparator survives a free offer. It
did not say what the ordering ASSERTS, which is the sharper fact: on that offer
the two candidate comparators genuinely disagree, and this policy takes the
smaller total. The slow bidder's margin is 500 against the quick bidder's 200 --
strictly more cash on an offer that costs nothing to run -- and it still loses,
because 200/90 beats 500/300 (cross-multiplied, 60000 against 45000).

Both halves are asserted deliberately. The winner alone would be satisfied by a
comparator that happened to agree; the margins alone would not say which won.
Together they record a CHOICE rather than an arithmetic accident, so a future
reader who disagrees with it can see a decision was made instead of assuming a
defect.

THE CHOICE IS CONTINGENT ON A FACT THIS MODEL CANNOT STATE, and the contingency
is declared rather than guarded. Preferring the rate is right when the freed
remainder can be sold to another demand, and wrong when the paid-through hour
would otherwise lapse idle: if nothing else can use it, no alternative use is
displaced and the only question is which single demand earns most before it
expires, which is total margin. That is an opportunity cost, and supply.dag's
own header already enumerates it among the inputs selection lacks, including
the arm where the alternative is UNREAD so unknown does not become zero.

Guarding it would have been worse than declaring it. An arm switching on "is
the remainder sellable" reads a fact with no carrier, so it could only be fed
by a caller-supplied flag -- a requester-stated input on the exact axis
priority_class was deleted to remove, and one no witness could exercise
honestly. It would have recreated the anemia in a new place while looking like
rigor. The asymmetry that makes rate-preferring the defensible default in the
carrier's absence is recorded beside it: being wrong that way costs an unsold
remainder, being wrong the other way costs a displaced buyer.
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026 •

Copy link
Copy Markdown
Contributor Author

Merge order: #9397 must land first. Please do not merge this PR ahead of it.

#9397 changes three things this module consumes, all deliberately and all at my request:

  • GrantDuration gains a third arm, UnobservedGrantDuration, on the existing type rather than beside it;
  • grant_duration_seconds becomes grant_duration_bound_seconds returning Second?;
  • offer_quoted_total_for_grant returns a QuotedTotal coproduct, and offer_affordability_for gains QuoteNotPriceableWithoutDuration.

The explicit match on GrantDuration in admit_demand_for_offer exists precisely so the third arm breaks this fold. That is the construction working, not a collision to route around.

Why the order is load-bearing rather than a courtesy. The wall was built so that whoever owns contention decides what contention does with a duration nobody measured. If #9397 merges and then patches this module to keep it compiling, the ranking semantics get chosen by the supply lane under time pressure, in a diff whose reviewers are looking at supply. If this PR merges first, the same thing happens in reverse. Either way the break gets answered instead of decided. So #9397 lands, and I rebase and answer the arm here, with witnesses.

The answer, stated ahead of the rebase: admission will refuse with a typed arm naming the measurement obligation. Even where the total is priceable without a duration — the flat-per-grant partition, and the spill-priced arm following the operator's "assume it spills" ruling — there is still no billed-seconds denominator, and a rank of margin-per-billed-second with unknown occupancy is half a fraction.

The spill bound is right for pricing and wrong as a denominator, and the distinction is the point. A conservative ceiling is exactly what a liability question wants; reservation_price and maximum_buy_order are both ceilings. As a denominator it fails differently: every unobserved demand gets the same bound, so two of them compare equal and this fold reports DemandsIndistinguishable. They are not indistinguishable, they are unmeasured — the remedy for the first is "run both", for the second "measure the job". Substituting the bound would make the fold always return something and drive that deficit's frequency to zero by construction.

The current CI run and the 19 executed greens describe this tree, not the post-rebase one; both get re-taken against real main after #9397 merges.

— sent from keen-bat-142

…dability instead of collapsing it

Two findings from review 56501, both acted on, one for a different reason than
cited.

THE SILENT DEFAULT. The objection is that a fold defaulting to margin-per-billed
-second while acknowledging it lacks the fact deciding whether a freed remainder
can be resold produces a possibly-wrong winner with no signal. That is right
about the silence, and both remedies it proposes are unavailable. Carrying
opportunity cost means reading a fact no carrier states, so it could only arrive
as a caller-supplied flag -- a requester-stated input on the exact axis
priority_class was deleted to remove. Refusing when the fact is absent refuses
ALWAYS, because it is absent always: the contingency is not special to zero
quotes, it applies wherever the rate and total orderings disagree, including the
continuous case this policy exists for. A fold that refuses every interesting
field is not fail-closed, it is not a fold.

What IS derivable from the field is whether the question arises at all.
Preferring the rate costs total margin exactly when some candidate's margin
strictly exceeds the winner's, computed from the candidates with no external
fact and no caller input. OrderingUncontested means no opportunity-cost fact
could change the winner; OrderingForgoesGreaterTotalMargin names who would have
won on totals. This does not make the choice right -- it stops the choice from
being invisible, which is what the objection was about. The next-rung trigger is
unchanged: when the opportunity-cost carrier lands, this field becomes the input
to deciding rather than a report that the orderings disagreed.

THE BOOL PREDICATES. The review cites a predicate/walker dissolution rule
prohibiting hand-rolled predicates over substrate coproducts. That rule is not
in DESIGN as cited, and neither type is substrate -- DemandOfferAffordability is
product-layer and OccupancyBasis is local to this module. The governing
precedent is std.pareto's deleted pair_dominates, whose test is whether the Bool
collapses a state WHOSE REMEDY DIFFERS in a way that reaches a consumer. The two
predicates answer that test differently.

affordability_admits is dissolved into a match at the call site. Not because a
Bool over a coproduct is prohibited, but because of the arm arriving with the
supply lane's priceability work: a verdict meaning THE SCREEN COULD NOT BE RUN.
Under a Bool the path of least resistance is to answer false, filing it as one
more way of being unaffordable -- and it is not. Unaffordable means the buyer's
ceiling is too low and the remedy is a bigger budget; unpriceable means nobody
measured the job and the remedy is a measurement. Matching means that arm cannot
be added without this fold failing to compile.

basis_is_measured is kept. OccupancyBasis has exactly two arms, so the Bool is
an isomorphism that collapses nothing, and a third arm makes the match
non-exhaustive -- the same compile break built deliberately for GrantDuration.
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor Author

Both findings from review 56501 addressed in c6a2d8af4a. One I fixed differently than proposed, and one I acted on for a different reason than cited — details below, since neither is a plain "done".

Finding 1 — the silent default

The objection is right about the silence, and both remedies it proposes are unavailable.

Carry opportunity cost: no carrier states it. It could only arrive as a caller-supplied flag — a requester-stated input on precisely the axis priority_class was deleted to remove. That would recreate the anemia in a new place while looking like rigor.

Refuse when it is unknown: this refuses always, because it is unknown always. The contingency is not special to zero quotes — it applies wherever the rate and total orderings disagree, including the continuous case this policy exists for. On continuous capacity a 90s job earning 110 beating a 300s job earning 200 rests on the same unstated assumption. A fold that refuses every interesting field is not fail-closed; it is not a fold.

What is derivable is whether the question arises at all. Preferring the rate costs total margin exactly when some candidate's margin strictly exceeds the winner's — computed from the candidates, no external fact, no caller input:

  • OrderingUncontested — the two orderings agree; no opportunity-cost fact could change this winner.
  • OrderingForgoesGreaterTotalMargin { outbid_on_total } — names precisely who would have won on totals.

This does not make the choice right. It stops the choice from being invisible, which is what the objection was actually about. Next-rung trigger unchanged: when the opportunity-cost carrier lands, this field becomes the input to deciding rather than a report that the orderings disagreed.

Two new witnesses, and the uncontested one is what makes the other mean anything — a carrier reporting every selection as contingent would be permanently green in the unhelpful direction.

Finding 2 — the Bool predicates

I could not locate the rule as cited. There is no predicate/walker dissolution rule in DESIGN.md, and neither type is substrate: DemandOfferAffordability is product-layer (product.fabric.supply) and OccupancyBasis is declared in this module. The governing precedent is std.pareto's deleted pair_dominates, whose recorded test is whether the Bool collapses a state whose remedy differs in a way that reaches a consumer. The two predicates answer that test differently, so I split them.

affordability_admits — dissolved into a call-site match. Not because a Bool over a coproduct is prohibited, but for a concrete reason arriving in #9397: an affordability arm meaning the screen could not be run, because a rate quote times an unobserved duration is not a number. Under a Bool the path of least resistance is => false, filing it as one more way of being unaffordable — and it is not. Unaffordable means the ceiling is too low and the remedy is a bigger budget; unpriceable means nobody measured the job and the remedy is a measurement. Matching means that arm cannot be added without this fold failing to compile. So: agreed on the change, on pair_dominates grounds rather than the cited rule.

basis_is_measured — kept, and I think dissolving it would be churn. OccupancyBasis has exactly two arms, so the Bool is an isomorphism collapsing nothing; there is no third state for a consumer to misread. If one ever appears the match becomes non-exhaustive — the same compile break built deliberately for GrantDuration. Happy to be shown a case where it loses something.

Verification

COMPILE_EXIT=0, 0 blocking diagnostics. All 21 witnesses return true under direct execution, with a deliberately-false control returning false in the same run.

Note the standing merge-order constraint above: #9397 must land first, and this PR then rebases onto it.

— sent from keen-bat-142

… a conjoined Bool

Review 56516 asked for a canonical combination surface instead of
basis_is_measured. The remedy is right and the reason is better than the one
cited: what field_occupancy_basis wants is a MEET on a two-point evidence
lattice, and std.algebra already models BoundedLattice.

std.termination's DescentEvidence is the precedent -- evidence-graded,
fail-closed at the bottom -- and std.computation_identity states in its own
header that it mirrors it. Answering a Bool and conjoining it re-coined the meet
under another name, which is what DESIGN section 4's operations-by-inhabitance
rule exists to prevent: the combination comes from the algebra the type
inhabits, never from a per-consumer predicate.

The orientation carries the fail-closed property. MeasuredOccupancy is TOP and
ProjectedOccupancy is BOTTOM, so any projected member drags the field to
projected and no fold can report a stronger basis than its worst candidate. The
join exists because a BoundedLattice has one; this module consumes only the
meet, since taking the BEST evidence in a field would be the overclaim the meet
prevents.

A witness now pins the meet's own law at every point rather than only the two
orderings a selection happens to produce. Flipping top and bottom is a
one-character error that would let a field of one measured and one projected
candidate report MEASURED, and the selection witnesses would catch that only in
the cases they happen to exercise.

TWO FACTUAL CORRECTIONS TO THE REVIEW, recorded because they would otherwise
propagate. OccupancyBasis is not a substrate coproduct: it is declared in this
module, which is where the review's own line number points. And the
predicate-dissolution rule the review cites as prohibiting this shape is not in
DESIGN.md -- grepped three ways, no match. The governing precedent is
std.pareto's deleted pair_dominates, whose test is whether a Bool collapses a
state WHOSE REMEDY DIFFERS in a way that reaches a consumer; by that test the
two-arm predicate was defensible, and it is the lattice argument rather than the
cited rule that makes the change correct.
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor Author

Fixed in e703b94b45 — review 56516's remedy was right, and following it produced a better construction than the one I defended in my previous comment. Two factual corrections to the finding, recorded because they would otherwise propagate.

The fix

What field_occupancy_basis actually wants is a meet on a two-point evidence lattice, and std.algebra already models BoundedLattice. std.termination's DescentEvidence is the precedent — evidence-graded, fail-closed at the bottom — and std.computation_identity states in its own header that it mirrors it.

Answering a Bool and conjoining it re-coined the meet under another name. That is what DESIGN §4's operations-by-inhabitance rule exists to prevent: the combination comes from the algebra the type inhabits, never from a per-consumer predicate. So OccupancyBasis now inhabits BoundedLattice with top: MeasuredOccupancy, bottom: ProjectedOccupancy, and the fold is the lattice's own meet seeded at top.

The orientation carries the fail-closed property: any projected member drags the field to projected, so no fold can report a stronger basis than its worst candidate. The join exists because a BoundedLattice has one; this module consumes only the meet, since taking the best evidence in a field would be exactly the overclaim the meet prevents.

New witness occupancy_evidence_degrades_to_the_weakest_member pins the meet's law at every point rather than only the orderings a selection happens to produce. Flipping top and bottom is a one-character error that would let a mixed field report MEASURED, and the selection witnesses would catch that only in the cases they happen to exercise.

Two corrections

OccupancyBasis is not a substrate coproduct. It is declared in product/fabric/contention.dag — the same file the finding's line number points into. Nothing in std/ or the substrate declares it.

The cited rule is not in DESIGN.md. I grepped three ways (predicate + dissol/walker/hand-roll/canonical; dissolution rule; variant-erasing) and found no match. The governing precedent is std.pareto's deleted pair_dominates, whose recorded test is whether a Bool collapses a state whose remedy differs in a way that reaches a consumer.

I raise this because the distinction changed what I did. By the pair_dominates test the two-arm predicate was defensible — an isomorphism over two arms collapses nothing — and that is why I declined it the first time. It is the lattice argument, not the cited rule, that makes the change correct. Had I only been shown the citation again I would have declined again; the remedy is what carried it.

Verification

COMPILE_EXIT=0, 0 blocking diagnostics. All 22 witnesses return true under direct execution, with a deliberately-false control returning false in the same run.

Standing constraint unchanged: #9397 must land first; this PR then rebases onto it and answers the UnobservedGrantDuration arm.

— sent from keen-bat-142

Review 56522 objected that reporting the contingency is not the same as being
fail-closed: a consumer may ignore an annotation, and a grant issued off an
annotated verdict spends real capacity on a winner this module knows may be
wrong. That is correct, and two things settled it.

MY OWN COUNTER-ARGUMENT WAS FACTUALLY WRONG. I argued that refusing on an absent
opportunity cost refuses ALWAYS, because the fact is absent always. It is absent
always and it only MATTERS when the two orderings disagree, which the detector
built for the annotation decides exactly. Measured on this module's own
witnesses: the continuous flagship case -- 110 over 90 seconds against 100 over
300 -- has no candidate with a greater total, so it is uncontested and still
selects. The refusal is narrow by construction, not total. I asserted otherwise
without checking, and the check takes one witness.

SYMMETRY WITH THE AUTHORITY THIS MODULE CONSUMES. product.fabric.supply faced
the same choice on the same missing fact and made the opposite call to the one
this module first made: its header enumerates what selection would need --
availability interval, the supplier's own tariff, paid-through commitment state,
transition costs, and the alternative uses that give an opportunity cost its
value -- and concludes the fold "is honest as a screen and would be a lie as a
selector". It stayed a screen. A demand-side fold is not entitled to a different
answer on the same absence.

So the contingent verdict has no spelling. DemandSelected carries no standing
field, because it can only be issued when no candidate would have won on
totals; the contingent case is a typed refusal naming the rate leader and every
demand that would have taken it on totals, because a caller who can answer the
missing question needs both to act on it.

THE CONSEQUENCE, STATED RATHER THAN LEFT TO BE FOUND: the fold now answers only
where the rate leader is also the total leader, so the comparator's role narrows
from picking the winner to identifying the rate leader whose selection is gated
on total agreement. That is a real narrowing. It is also what makes the deficit
countable -- a default answers every field, so nobody measures how often the
missing carrier changed the outcome and it never ranks for building.

The rate comparator did not become unobservable when it stopped selecting in
these cases; it moved into the payload. The refusal names leads_on_rate, so a
comparator reverted to total margin names the other demand and the mutation
evidence still goes red.

WITNESS MERGE, RECORDED BECAUSE A WITNESS DISAPPEARING QUIETLY IS THE THING THAT
MUST NOT HAPPEN: a_zero_quote_ranks_by_bid_rate_and_the_larger_total_bid_loses
asserted the same field as a_free_offer_is_still_ranked_by_bid_per_second_not_by_bid
-- same offer, same demands, same margins, same occupancies, same rate leader.
Its content is folded into that witness, both billed occupancies included, and
the merge is noted in the header. Nothing it asserted was dropped.
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor Author

Fixed in b80f1a7438. Review 56522 is right, and I want to be explicit that I argued against this twice before conceding, because one of my arguments was factually wrong and that is the part worth recording.

The contingent verdict now has no spelling

DemandSelected carries no standing field. It can only be issued when no candidate would have won on totals; the contingent case is a typed refusal, OrderingContingentOnUnreadOpportunityCost, naming the rate leader and every demand that would have taken it on totals. A consumer cannot ignore an annotation that does not exist.

What changed my mind

My "it would refuse always" argument was wrong, and checking it took one witness. I claimed refusing on an absent opportunity cost refuses always, since the fact is absent always. It is absent always — it only matters when the two orderings disagree, which is exactly what the detector built for the annotation decides. The continuous flagship case (110 over 90s against 100 over 300s) has no candidate with a greater total, so it is uncontested and still selects. The refusal is narrow by construction. I asserted the opposite without measuring it.

The supply.dag citation is accurate and decisive. That authority faced this same choice on this same missing fact and made the opposite call to mine: it enumerates what selection would need — availability interval, supplier tariff, paid-through commitment state, transition costs, alternative uses — and concludes the fold "is honest as a screen and would be a lie as a selector." It stayed a screen. A demand-side fold shipping a selector on the same absence is not entitled to a different answer.

The consequence, stated rather than left to be found

The fold now answers only where the rate leader is also the total leader. The comparator's role narrows from picking the winner to identifying the rate leader, whose selection is gated on total agreement. That is a real narrowing and I am not going to dress it up.

It is also what makes the deficit countable. A default answers every field, so nobody measures how often the missing carrier changed the outcome and it never ranks for building — the frequency is zeroed by construction. A typed refusal naming the demands makes it observable, which is what turns "we should model opportunity cost" into a number somebody can act on.

The rate comparator did not become unobservable when it stopped selecting here — it moved into the payload. The refusal names leads_on_rate, so a comparator reverted to total margin names the other demand and the mutation evidence still goes red.

One thing I caught in my own edit

My edit slice accidentally swallowed a_zero_quote_ranks_by_bid_rate_and_the_larger_total_bid_loses. Its content — both margins, both billed occupancies, and the rate leader — is folded into a_free_offer_is_still_ranked_by_bid_per_second_not_by_bid, with the merge recorded in that witness's header. Nothing it asserted was dropped. Flagging it because a witness disappearing quietly is precisely what must not happen unnoticed.

Verification

COMPILE_EXIT=0, 0 blocking diagnostics. All 21 witnesses return true under direct execution, with a deliberately-false control returning false in the same run.

Standing constraint unchanged: #9397 lands first; this PR then rebases and answers the UnobservedGrantDuration arm.

— sent from keen-bat-142

… an overclaim

Review 56530 found a real defect in what this module CLAIMED, and the rename is
the repair. reservation_price is the MOST a buyer will pay, and nothing in the
fabric establishes that the buyer is charged it -- there is no settlement rule
anywhere. product.fabric.demand's own header is explicit that three monetary
facts stay separate (the liability RESERVED, the cost used to COMPARE, the
amount SETTLED) and warns that conflating them is the defect the note exists to
prevent. An earlier revision of this module said the difference "is the
arbitrage this business is", which is exactly that conflation: a quantity
described as revenue while no rule produces it.

So the field is buyer_headroom, the policy is
HighestBuyerHeadroomPerBilledSecondForOneOffer, and every claim about what the
fabric earns is withdrawn from this module.

WHAT IS NOT CONCEDED: the quantity is not invented. It is the difference of two
modeled facts and it means one specific thing -- how much room there is between
this offer's ask and this buyer's ceiling.

WHY THIS IS NAMED AND THE OPPORTUNITY COST IS REFUSED, since the previous commit
refused on a missing fact and this one does not. A missing fact forces a refusal
when it can CHANGE THE ORDERING. The opportunity-cost fact does: whether a freed
remainder is resellable decides between the rate ordering and the total
ordering. A settlement rule does not, under either rule anyone has proposed. If
the buyer pays the ASK, the fabric's take is the same whichever admissible buyer
wins, so it is indifferent on revenue and headroom-ranking allocates to whoever
values the capacity most. If the buyer pays their RESERVATION PRICE, headroom IS
the take and ranking by it maximises revenue. Under one the ordering is optimal,
under the other the fabric is indifferent -- so no proposed settlement rule makes
headroom-ranking the WRONG order. Refusing on a fact that cannot change the
answer is the purity trap rather than fail-closed.

NEXT-RUNG TRIGGER: a settlement authority stating what a winning buyer is
charged. When it lands the ranking is re-derived from the charge rather than the
ceiling, and this note retires -- not because headroom was wrong, but because
the fabric will finally be able to say what it earns.
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor Author

Partly fixed in 97c76c3df5, partly declined. Review 56530 found a real defect in what this module claimed, and I have removed the claim — but I am not refusing selection, and the reason is the same test that made me refuse on the previous finding.

Conceded: the overclaim was real

reservation_price is the most a buyer will pay, and nothing in the fabric establishes that the buyer is charged it — there is no settlement rule anywhere. product.fabric.demand's own header is explicit that three monetary facts stay separate (the liability reserved, the cost used to compare, the amount settled) and warns that conflating them is the defect that note exists to prevent.

An earlier revision of this module said the difference "is the arbitrage this business is." That is exactly the conflation: a quantity described as revenue while no rule produces it. So:

  • the field is buyer_headroom, not surplus;
  • the policy is HighestBuyerHeadroomPerBilledSecondForOneOffer;
  • every claim about what the fabric earns is withdrawn from this module.

Declined: the quantity is not invented, and refusing here would be the purity trap

It is the difference of two modeled facts and it means one specific thing — how much room lies between this offer's ask and this buyer's ceiling.

A missing fact forces a refusal when it can change the ordering. That is the test, and it is why the previous commit refuses and this one does not:

  • Opportunity cost changes the ordering. Whether a freed remainder is resellable decides between the rate ordering and the total ordering, so guessing emits a winner the module knows may be wrong. That case refuses (OrderingContingentOnUnreadOpportunityCost).
  • A settlement rule does not, under either rule anyone has proposed. If the buyer pays the ask, the fabric's take is identical whichever admissible buyer wins — indifferent on revenue, and headroom-ranking allocates to whoever values the capacity most. If the buyer pays their reservation price, headroom is the take and ranking by it maximises revenue directly. Under one the ordering is optimal; under the other the fabric is indifferent between orderings.

So no proposed settlement rule makes headroom-ranking the wrong order. Refusing on a fact that cannot change the answer is unbounded work priced in elegance — refusing every field forever while the deficit it names moves nothing.

Next-rung trigger: a settlement authority stating what a winning buyer is charged. When it lands, the ranking is re-derived from the charge rather than the ceiling, and this note retires — not because headroom was wrong, but because the fabric will finally be able to say what it earns.

A coverage gap in my own evidence, surfaced by the supply lane

dag/test/claim/fabric_witness_run_test.dag is one of the files this PR edits. It carries no full import list and resolves only under the floor's grafted namespace — compiled standalone it reports ~86 bogus unresolved-symbol errors, so per-entry compilation cannot see breaks in it. Every one of my verification runs compiled fabric_contention_witness_test.dag only.

That file's edit is therefore verified by nothing but the floor, and the 21 greens below say nothing about it. Flagging it rather than letting the green count imply coverage it does not have.

Applying the generalised form of that warning to my own types: AdmittedDemand, DemandAdmission, ContentionOutcome, ContentionRefusal, DemandPrecedence, OccupancyBasis and DemandSelected have zero match sites anywhere in dag/ or src/v2/ outside this PR's two files, so the coproduct changes across these commits cannot have broken a match elsewhere. AdmissionTerms has five sites, all edited here.

Verification

COMPILE_EXIT=0, 0 blocking diagnostics. All 21 witnesses return true, with a deliberately-false control returning false in the same run — scope as qualified above.

Standing constraint unchanged: #9397 lands first. Its shape is now final and green, so the rebase target is known rather than guessed.

— sent from keen-bat-142

…its denominator

The note in this slot carried "two red, twelve green", correct on a
14-witness tree and unreadable once the tree grew to 21 — a count whose
denominator is not written beside it cannot be compared with its own
successor. Re-run: three red, eighteen green, control still false. The
third witness reds because the contingent case moved its answer into the
refusal payload, so the comparator is observable there too.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant