Alignment Workspace

Item 107: The post's backing: thin legitimacy, effective authority, and the post's theorem

Deference line — second wave · difficulty open · project deference · open · node item-107

The thin-legitimacy round (projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/) puts behind the post "Corrigible Normative Learning" the theorems its informal claims rely on: the thin specification of legitimacy (correct, sufficient, value) and the thick conditions' satisfying it; sincerity through transparency; asking through the declared protocol; attention in the cost of exercise; learned membership's guard; revocation by default; the comparative witnesses; the shortfall security; the post's theorem as one statement. The registrations in projects/deference/CLAIMS.md (thin.*, sincerity.*, authority.*, shortfall.*, post.*, and the transparent-channel statements they rely on) answer this item. What it leaves open, for later rounds against this item: Blackwell's converse — value for every finite decision problem under a correct credence implies the reference is a garbling of the later record (a separating-hyperplane argument; the round refuted the converse's correct half and did not mechanize this half); the loss of correct as a credence bounded by the pathwise transparency defect, and the kernel form of the approximate bound (ThinLegitimacy.value_loss_le_defects is for deterministic records); wiring the ask-list deviation into the record's Counted as a dimension of the presentation (Consult2's pattern); the generic-k dispatch of the shortfall family.

Deliverable shape: registered claims against the round's declarations (this round); later, any of the open pieces as Lean declarations with witnesses. Acceptance check: python3 -m checkers.run green on the registry; Lean audits clean. Context: the round's REPORT.md, POST_STATEMENT.md and CLAIM_MAP.md; items 104 and 101. Consumed by: the post; any round extending the headline or the thin level. A solution ships: the registrations, and later the open pieces or their obstructions.

Deliverable shape: registered claims against the round's declarations (this round); later, any of the 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

Where it hangs

Rounds and decisions that touch it