feat(represent): proxy evidence orders promotion without becoming price (R4-F1) - #379
Merged
Merged
Conversation
chrishayuk
force-pushed
the
fix/r4f1-ordinal-proxy-dominance
branch
from
September 1, 2026 20:48
683c56e to
7928615
Compare
R4-F1, found by Rung 4's first real search.
The driver printed `PROMOTE: e26`, matching the pre-registered
prediction. Reversing the input list printed `PROMOTE: e20`, from
identical reports. All four rank keys were byte-identical —
`tier=1 within=0.702202900 frugality=-0.0` — because `within` falls back
to `gpu_ms_saved` for any non-`Priced` class and every one-step move
removed the same bytes. `cmp_rank` returned Equal and a stable sort
handed back input order. At diagnostic scale nothing is priceable BY
DESIGN, so that tie is the normal state, not an edge case. Meanwhile
both calibrated proxies separated the four candidates monotonically and
unanimously: the evidence existed and the comparator could not see it.
The invariant this pins:
Determinism may order indistinguishable candidates for DISPLAY; it may
never convert indistinguishability into evidence for PROMOTION.
`display_order` may use identity as its final tie-break.
`decide_promotion` is not given identity at all, so it cannot.
ORDINAL, never scalar. An OrderingProxy licenses order and not
magnitude, so a numeric proxy term in RankingScore would smuggle
magnitude back through the comparator. Instead: A proxy-dominates B iff
no worse on every comparable proxy and strictly better on at least one.
Comparability requires BOTH candidates to have observed the statistic
and the registry to say it orders at this scale.
Conflicts are REFUSED, not traded off — there is no empirical basis for
how many places of kl are worth one place of routing, so a frontier
returns Ambiguous{ConflictingOrderingProxies}. Physical gain may
separate candidates the proxies call EQUAL, and that is recorded as
`decided_by_physical_gain` so a trace never has to guess which stage
decided.
Statistic moves to its own module with a canonical `better()`/`order()`:
one derivation of which end is good, because deriving it from a gate's
LimitKind would only work for statistics a contract bounds, and
RouteFlipRate is bounded by nothing. quality.rs also went to 888 lines
in #376 — over the 800 cap — and is back to 775.
Two things the tests caught. The decision was permutation-invariant
before the evidence RECORD was: `dominated` echoed input order, so the
same round produced different traces. And sorting the table on
`cmp_rank` alone put the WORST candidate first, because every key tied
and identity decided — `display_order` now reads best-first.
On the real four reports, both permutations: PROMOTE e26, dominating
e20/e23/e24, deciding proxies [KlP99, RouteFlipRate]. No new GPU work.
Selection is not prediction. The variant is `SelectForAuthority`, not
`Promote`, and its evidence names the authority dimensions the
diagnostic scale could not speak to. `Uninformed` is ELIGIBLE by design:
authority is the mechanism that resolves those dimensions, so gating it
out would silently rewrite the doctrine into "diagnostic must predict
every authority dimension before authority may run" — impossible at 256
positions for the mass tails.
Uninformed may be selected for authority IFF it is otherwise
promotable, the missing dimensions are EXPLICIT, and no
better-evidenced candidate outranks it.
Never `Uninformed => refuse`, never `Uninformed => assume free`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
R4-F1 — found by Rung 4's first real search against the Kimi bank.
The defect
The driver printed
PROMOTE: e26, matching the pre-registered prediction. Reversing the input list printedPROMOTE: e20, from identical reports.All four rank keys were byte-identical:
rank_key() = (class.tier(), within, frugality), andwithinfalls back togpu_ms_savedfor any non-Pricedclass. Every one-step move removed the same bytes ⇒ exact tie ⇒cmp_rankreturnsEqual⇒ a stable sort returns input order.At diagnostic scale nothing is priceable by design, so this tie is the normal state, not an edge case. Meanwhile both calibrated proxies separated the candidates monotonically and unanimously. The evidence existed and the comparator could not see it.
The invariant
display_ordermay use identity as its final tie-break.decide_promotionis not given identity at all, so it cannot — structural, not a discipline.Ordinal, never scalar
An
OrderingProxylicenses order and not magnitude, so a numeric proxy term inRankingScorewould smuggle magnitude back in through the comparator.A proxy-dominates B iff no worse on every comparable proxy and strictly better on at least one. Comparability requires both candidates to have observed the statistic and the registry to say it orders at this scale.
The staged comparator: class → proxy ordering → physical gain → frugality. Conflicts are refused, not traded off — no calibration says how many places of kl buy one place of routing, so the frontier returns
Ambiguous{ConflictingOrderingProxies}. Physical gain may separate candidates the proxies call equal, recorded asdecided_by_physical_gainso a trace never has to guess which stage decided.Selection is not prediction
The variant is
SelectForAuthority, notPromote, and its evidence names the authority dimensions the diagnostic scale could not speak to.Uninformedis eligible by design — authority is the mechanism that resolves those dimensions, so gating it out would silently rewrite the doctrine into "diagnostic must predict every authority dimension before authority may run", which at 256 positions is impossible for the mass tails.The policy, stated once: Uninformed may be selected for authority iff it is otherwise promotable, the missing dimensions are explicit, and no better-evidenced candidate outranks it. Never
Uninformed => refuse, and neverUninformed => assume the missing dimensions are free.Result on the real reports — no new GPU work
display_orderrecovers the pre-registerede26 < e24 < e23 < e20.Two things the tests caught
The decision was permutation-invariant before the evidence record was —
dominatedechoed input order, so the same round produced different traces. And sorting the table oncmp_rankalone put the worst candidate first, because every key tied and identity decided.Also
Statisticmoves to its own module with a canonicalbetter()/order()— one derivation of which end is good, since deriving it from a gate'sLimitKindonly works for statistics a contract bounds, andRouteFlipRateis bounded by nothing.quality.rsalso hit 888 lines in #376, over the 800 cap; it is back to 775.Verification
fmt,clippy -D warnings, E0 (10 passed), full suite (3648 passed, 0 failed),cargo check --workspace --all-targets. Coverage policy passed —statistic.rs100.00%,decision.rs96.40%; crate 93.49%.