Item 104: The corrigibility kernel headline: the registered statements and what they leave open
Deference line — second wave · difficulty open · project deference · open · node item-104
The kernel's headline (lean/Workspace/Deference/Spec/Headline.lean, the phase-2 round's SPEC.md) states Boxes 1–3, the hierarchy per decision and per history, the subjective exchange rate, the legitimacy map and the promoted definitions, with the house-sale witness inhabiting the package; the registrations in projects/deference/CLAIMS.md answer this item. What the headline leaves open, for later rounds against this item: the general split gate proved on GateIsLegitimacy.Segment beyond the consultation model's rows (the map is general, the rows are the model's); a recognized count on one model carrying all four instances of the fidelity interface, if one is ever wanted; the evaluator-to-auction bridge stated on the band rather than through bandParams at the floor; and the mediation results restated on the allocation of authority directly rather than through the thin datum.
Deliverable shape: registered claims against the headline's declarations (this round); later, any of the four open pieces as Lean declarations with witnesses. Acceptance check: python3 -m checkers.run green on the registry; Lean audits clean. Context: the phase-2 round's SPEC.md §8 and REPORT.md; the phase-1 round's REPORT.md §6 (what did not compress). Consumed by: the post; any round extending the headline. A solution ships: the registrations, and later the open pieces or their obstructions.
Deliverable shape: registered claims against the headline's declarations (this round); later, any of the four open pieces as Lean declarations with witnesses.
Acceptance check: python3 -m checkers.run green on the registry; Lean audits clean.
Registered results bearing on this item
- kernel-box2-finite-time: In the corrigibility kernel's second box, for a logical inductor the ranking of the violating option below the compliant one holds at every day from the price range alone, while the expectation-provab
- kernel.box1-fidelity-versus-fully-updated-deference: One menu, two options; one estimate within `r` of the true value. Scoring outcomes only, on a world where the true values agree, the margin for asking is at most `2r`; scored on the fidelity score wit
- kernel.box2-dominance: Where `π` does not violate, `𝔱π` agrees with it; where it does, `𝔱π`'s evaluation is at least the band's floor and `π` carries a violation. The margin is restated from the landed `ϖ − D` because the m
- kernel.box2-mediation-faithful: Formerly `kernel.box2-mediation`, statement of record `box2_mediation_corrigible` (the landed policy notion `Corrigibilization.Corrigible`); renamed by the second follow-up (2026-09-27) because "corri
- kernel.box3-gap-exchange-rate: The gap sets the threshold; the small-gap witness `box3_small_gap` forces it.
- kernel.box3-no-incentive-to-compromise: The witnesses `box3_conditioning_fails` and `box3_sealed_no_incentive` show why the gate multiplies rather than conditions.
- kernel.box3-no-laundering: Lower by `ϖ` per counted deviation.
- kernel.box3-restoration: With `box3_band_order` and `box3_suppression_loses` (the band's width below `ϖ`, the disclosure deadline at or before the settlement window's close). Inhabited by `HouseSale.box3_capture_reported_and_
- kernel.corrigible-fidelity-score: `Headline.Corrigible U D′ lo ϖ′` is the preference property over recognized violations (window `D′ − ϖ′ < lo`; the known clause with the margin `ϖ′ − (D′ − lo)`; the risk clause at the exchange rate).
- kernel.corrigible-generic: From the authority-module round's generic lexical lemma (`generic_lexical_local`) with the risk term added. The class includes objectives whose ordinary term is not her evaluation: `corrigible_not_ali
- kernel.extension-bria-realization: From `overestimation_le_allowance_opening` under the landed hypotheses (feasibility, consistency, inquiry on the menu, the conditional-expectation bound, the noise over all blocks). Follow-up (2026-09
- kernel.extension-realized-rate: The registered claim kernel.extension-realized-rate (The extension's interface theorem: avg π ≤ avg (D − c_k)/ϖ + ε̄ ((D − w)/ϖ + θ_hi) + (B(K) + M(K))/(ϖ Σ w_k)) holds as its declaration states it; t
- kernel.hierarchy-history: With `summed_counterexample`: `K·D − ϖ` beats `K·w_lo` once `K (D − w_lo) > ϖ`. Inhabited by the house-sale fixture (`test_history_hierarchy_and_summed_counterexample`).
- kernel.hierarchy-per-decision: Over any evaluation schedule, with `D − ϖ < w_lo`. Inhabited by `CorrigibilityKernel.Witness.hierarchy_instance` at the worked parameters.
- kernel.subjective-exchange-rate: With `subjective_exchange_rate_li` at every finite day of a logical inductor. Restated by the follow-up (2026-09-27, Part 1): `subjective_exchange_rate_corrigible` (= `Corrigible.exchange`) proves it
Where it hangs
- held by deference-and-trust