Item 46: Should force cost depend on the row presentation?
Normativity line — traderized enforcement · difficulty open · project normativity · open · node item-46
— partially answered by the proof-closing pass
The traderized compiler consumes a row system, not an admissible set, and the two are not interchangeable. Under the installed ForceDeclaration at a fixed declared tolerance, k duplicate rows scale the emitted position and the safety charge by k; rescaling a row by λ scales them by λ²; and a redundant non-duplicate row — p_A ≥ ½ and p_B ≥ ½ already imply p_A + p_B ≥ 1 — changes the emitted force while leaving the admissible set exactly where it was.
Rescaling is the benign case: it is a genuine reparametrization, and at a matched actual conformance target the position, realized liability and charge all agree. Duplication and redundancy are not.
The round takes Option A — the presentation is part of the force request — and records it as a choice rather than a result. Three alternatives are open:
- canonical normalization, which must state exactly which equivalence class it normalizes; scalar rescaling and literal duplicates are tractable, general H-presentation redundancy is not obviously so;
- a weighted compiler, where redundant rows carry declared weights summing to one, which would need the conformance theorem re-derived at the wrapper level;
- minimization over equivalent presentations, which is theoretically the right answer for "the cost of enforcing
K" and is expensive.
Deliverable shape: derived for a normalization theorem with its equivalence class stated; witness-checked for a construction; or a reasoned decision to keep Option A. Acceptance check: the round's presentation fixtures run against the chosen architecture, and the interface note's table is either derived or deleted. Context: .../2026-08-16-traderized-enforcement/NORMATIVE_SAFETY.md §11; test_outflow.PresentationChangesTheInstalledCompiler.
Partially answered: the intrinsic target is presentation-independent and the compiled trader is not, and the proof-closing pass separated the two. The exact dual-distance family depends on K alone — a generator inside the hull of the others contributes an implied constraint, so redundant generators and generator order change nothing (test_coherence.TheExactFamilyIsCanonical) — while duplication and rescaling of an arbitrary presentation do change the emitted position and the charge (test_outflow.PresentationChangesTheInstalledCompiler). What is still open is whether the cost can be made canonical, which is a question about the charge and not about the metric.
Deliverable shape: derived for a normalization theorem with its equivalence class stated; witness-checked for a construction; or a reasoned decision to keep Option A.
Acceptance check: the round's presentation fixtures run against the chosen architecture, and the interface note's table is either derived or deleted.
Registered results bearing on this item
None registered.
Where it hangs
- held by normativity
Rounds and decisions that touch it
None recorded.