Item 23: Lean promotion of the finite wave-1 results
Deference line — second wave · difficulty entry · project deference · open · node item-23
Answered, and registered: sixteen entries in projects/deference/CLAIMS.md — the delegation bridge and its two corollaries, the margin, override, defect and advantage lemmas with the strict grade-register theorem, the piercing duality and the exposure–harvest identity with its attainment, and the four propositions establishing that valuation data cannot separate delegation from an accurate simulator. The two deliberately excluded results stay excluded: the certificate's comparator clause and the uniform delegation bridge both rest on the grade-to-quantity link the programme decided to derive rather than assume. Record: prompts/2026-08-11-phase-ii-promotion/REPORT.md §5.
Registered results bearing on this item
- certificate.advantage-estimate: Wave-1 L7.
- certificate.defect-bound: Wave-1 L3.
- certificate.grade-register-strict: Wave-1 Theorem C'. Theorem C's V-register comparator clause is deliberately absent, resting on the movement hypothesis the phase exists to replace.
- certificate.margin-forces-agreement: Wave-1 L1. Finite, order- and arithmetic-only, with a constructed inhabitation witness.
- certificate.override-bound: Wave-1 L2.
- certificate.selection-eq-of-margin: Wave-1 L1, the equality form.
- delegation.bridge: The local form under a named GradeTrust hypothesis. The uniform `2M` form was deliberately not ported: it rests on the grade-to-quantity link the programme decided to derive rather than assume.
- delegation.bridge-unconditional: The corollary that drops the hypothesis where the refinement supplies it.
- delegation.gradetrust-refinement: The second corollary of the bridge.
- exposure.greedy-duality: Wave-1 Lemma 1.
- exposure.harvest-attained: Sharpness: the bound is not merely an upper bound.
- exposure.harvest-bound: Wave-1 Theorem 2.
- substitution.extensional-admits-both: Wave-1 Proposition 1. One of the four establishing that valuation data cannot separate delegation from an accurate simulator.
- substitution.separation-requires-disagreement: Wave-1 Proposition 6.
- substitution.sim-depends-on-induced-choice: Wave-1 Proposition 2.
- substitution.unpredictability-separates: Wave-1 Proposition 7. The separation is not inferable from a run; this states the condition under which it exists at all.
Where it hangs
- held by deference-and-trust
Rounds and decisions that touch it
None recorded.