PrimitiveCostFact carries the structured cost, and the duplicate carrier goes

[gunbai-bot]

PrimitiveCostFact.cost moves from the coarse CostShape to the structured CostBound that std.realization_cost_fidelity actually compares, closing the two-carrier fork that module's own frontier note named and scheduled. Follow-up to review 63996 finding 2 on #11026.

What the migration found before it changed anything

The note that scheduled this work said "the six populated rows record a shape and NO PARAMETER". Two corrections, both load-bearing:

• There are five rows, not six. The sixth was the type PrimitiveCostFact { declaration, counted by a grep. The count is corrected in that note by this PR, which also retires it.
• No row's parameter is recoverable from its signature. Three of the five (sorted_map_keys, fold_list, index_by) are SignatureUngrounded, and each states in its own reason that authoring a signature would fabricate it. The other two ground on FinitelySupportedFunctionProfile, which supplies type params K,V and a FiniteSupport classification but no cardinality variable. So the axis for the two grounded rows is derived from the carrier's declared support, not read off a signature.

The shape of the change

PrimitiveModeledCost has two arms: StructuredCost { bound } for a row whose axis is derivable, and CoarseCostOnly { shape, cause } for one whose is not.

The coarse shape survives on the refusal arm. Dropping it would have deleted ShapeSortBody and ShapeIterateBody — facts that were true and never in question. Only the structured form is unavailable for those rows, so the two-grain state survives exactly where it is declared with a typed cause, instead of silently across the population.

The axis has exactly one producer. finite_support_cardinality_param reads the carrier's own support axis; linear_support_scan_cost is the single constructor every structured row goes through. No row authors a parameter literal, so two rows about one carrier cannot spell the same axis differently — which nothing in the type system would otherwise prevent, since AtomicCost.param is a bare String.

Evidence

claim_batch over the new suite: 14 witnesses, 14 PASS, rc=0. The existing suites that touch this module are unaffected and re-run green: realization_cost_fidelity_witness 39, primitive_identity_join_witness 16, primitive_signature_grounding_witness 11. All eight modules importing std.primitive_identity compile with 0 blocking errors.

Green witnesses prove nothing on their own, so each discriminating arm was planted against, with the failures predicted in advance:

plant	predicted	observed
open-support carrier names an axis	the 2 refusal arms	exactly those 2
bound built quadratic, not linear	the 2 shape-agreement arms	4 — see below
map_values authors its own literal axis	the axis-identity arm	exactly that 1

The second plant failed two arms I had not predicted, and that exposed a defect in my own witness: both_grounded_rows_scale_in_the_same_derived_axis was comparing coarse shapes, so two rows with different parameter names would both have passed it. It now compares the actual parameter names via cost_bound_params, and the third plant confirms it fails on exactly that divergence.

The duplicate carrier goes with it, and the cut is at the root

ModeledCostBoundFact carried the same (PrimitiveIdentity, CostBound) pair as this carrier and had no production rows at all — its only constructions in the tree were fixtures. Leaving two carriers of one fact standing is the §3 fork that gets consolidated later at interest, so it is deleted here rather than after, and §3's replacement-migration rule says the cut goes at the root: the join's signature.

realization_cost_fidelity_rows now takes List<PrimitiveCostFact> directly. That collapses its two input lists into one, and the consequence is worth stating precisely because it is a ladder climb rather than a tidy-up:

• The join used to take modeled and unstructured separately, so a primitive appearing in both was a contradiction about one key that only a check could catch — PrimitiveIsBothStructuredAndUnstructured.
• With one list whose rows carry a coproduct, a row is structured or coarse-only and cannot be written as both. The state has no constructor.
• That is §4b's climb from mechanically preventable to structurally impossible, and §5's "prefer a single authority the realization is derived from over a check that flags the bad state after the fact".

No coverage was lost to that deletion. The old both-lists specimen becomes an ordinary duplicate — the same primitive on two rows, once structured and once coarse — which the surviving arm still refuses, and the witness still exercises it. The refusal type drops from three arms to the one that remains writable, and it is renamed: StructuredPrimitiveDuplicated said "structured" when there were two lists, and the single list holds both kinds, so keeping that spelling would have left one name covering two populations — the same §3 meaning fork this PR closes one layer up.

Declared frontiers

§3c consumption. The five rows had no roster and no consumers — dangling, while their sibling PrimitiveTraversalOrderFact has both. This PR adds primitive_d0_cost_facts, and the row says plainly that the roster is the identity join's subject universe, not the consumer.

• Consumer: std.realization_cost_fidelity realization_cost_fidelity_row, reached through realization_cost_fidelity_report.
• Route: the structured rows supply that join's modeled side. That side is typed ModeledCostBoundFact, whose only constructions in the tree are fixtures in test.claim.realization_cost_fidelity_witness — a shape with no production supplier, which is what these rows are shaped for.
• Trigger: the first construction of a RealizationCostFact outside dag/test/ — stated as that symbol rather than "when measurements exist", because the capability it stands for (the emitted compiler being measurable per primitive, so a realized cost is an observation rather than an assertion) is exactly what the first non-fixture producer demonstrates.
• Kill condition: if such a producer lands and these rows are still unread by that join, the frontier was wrong and the rows are dangling, not deferred.

§2 next rung. AtomicCost.param is a bare String — an anemic leaf carrying a modeled quantity as free text. The single-producer discipline above is a containment, not a fix: it makes this module's rows agree with each other and can do nothing about another module naming the same axis differently. Trigger: std.induction AtomicCost carrying a parameter identity rather than String, which dissolves the discipline into the type. Not attempted here — it rewrites every cost-bearing row in the tree.

What is still open

The realized side. No RealizationCostFact exists outside dag/test/, so no production caller passes the roster to the join yet — that is the §3c frontier above, and no amount of work on this carrier can supply it. The modeled side is now one carrier, read directly by the join, and executes in the witness suite.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f