Alignment Workspace

Item 85: Margin realization and end-to-end rate compatibility

Deference line — second wave · difficulty open · project normativity · open · node item-85

GatedChoice.softGate_practicalCert pays the Normative Inductor's practical certificate with M = D·κ, κ = (Σ_{q∉A} pref q)/(W·δ), under region exclusion at the projection u (Region: inadequate responses score at most τ) and a positive margin, which has two types. Route A (MarginMass, on u): the compiler positively marks adequate responses of preference mass W at τ + 2δ — a completeness condition, not soundness. Route B (MarginDisplayed, on the displayed scores b, softGate_massOff_le_displayed): the region only excludes and the market independently displays a marked adequate response; lic_provind_true of the pinned Logical Induction dependency (prices of an efficiently codeable sequence of adequacy theorems ≈_n 1) is evidence of this route's shape, asymptotic and without rate, and it does not establish route A. Both routes are pointwise at the occasion and apply to deductively or externally certified adequacy. M = D κ is charged through PracticalUptake.amplification, so the end-to-end condition is the existing amplification/modulus condition with Γ uniformly bounded; the local reading is that market error must shrink relative to the certified margin with the inadequate/adequate preference-mass ratio controlled.

State, for route A, the compiler completeness condition and its cost; for route B, the displayed-margin theorem composed with softGate_massOff_le_displayed and the amplification hypothesis at the service occasions the evaluation transports mass to; or the negative that no finite-time form exists on either route and the margin at service times is an external certificate. Separately: adequacy known only through later settlement may not supply pointwise Region; the bridge "average score error ⇒ average inadequate-action mass or practical loss" is not a theorem and is filed here as open.

Deliverable shape: the composed theorem for each route, or the negative with a witness; and the empirical averaged bridge or its negative. Acceptance check: the module audits clean and python3 tests/run.py is green.

Context: NORMATIVE_CHOICE_THEOREM.md §6 and DECISION_THEORY_BILL.md §4–§5 of projects/deference/rounds/2026-09-06-decision-theory-bill/. Consumed by: the gated decision adapter as the realization of Evaluation.Pi. A solution ships: the composed theorems, or the negatives.

Deliverable shape: the composed theorem for each route, or the negative with a witness; and the empirical averaged bridge or its negative.

Acceptance check: the module audits clean and python3 tests/run.py is green.

Context: projects/deference/rounds/2026-09-06-decision-theory-bill/

Registered results bearing on this item

None registered.

Where it hangs

Rounds and decisions that touch it

None recorded.