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
- asklist.offprotocol-deviation-finite: `deviates3` with `GateIsLegitimacy.deviation_finite`; `asks_off_deviates3` passes from the ask-list clause to the deviation. Inhabited by the flood row's deviation (`volume_by_want_tainted`) at any `0
- asklist.order-by-want-tainted: The lowest priority first on the wanted run. Its own inhabitant.
- asklist.rows-keep-verdicts-counted: Part 3 of the follow-up: `Consult2`'s pattern — `Decl3` with the protocol and the pool, `Pres3` with the ask list, `ref3` with the canonical asks. Rows 1, 6, 7, 9, 12, 14 (second round), 17, 18, 20 at
- asklist.rows-keep-verdicts-tainted: Rows 2, 3, 4, 5, 8, 10, 11, 14 (first round), 15, 16, 17', 19. Its own inhabitant.
- asklist.volume-by-want-tainted: The whole pool asked at once on the wanted run, the conforming ask otherwise: not counted (transparency at the consultation) and `deviates3` on the wanted run, not on the other. Its own inhabitant.
- authority.approval-discount-defeated: P6, the guard's necessity witness: the kernel's evaluation is the discounted one at discount zero (`evalOf_eq_discounted_zero`); at discount one the option evaluates at its bid. Inhabited by any `c <
- authority.comprehension-short: On a calm exterior, every exercise with a correction costs at least the comprehension cost. Inhabited by the obscure-ask fixture (comprehension 2 against bound 1) on the authority module's wire physic
- authority.exchange-rate-queue: The headline's `subjective_exchange_rate` verbatim at the queue's value, proved from `declared_loses`. Inhabited by the house-sale parameters (`HouseSale.exchange_rate_at_25`).
- authority.flood-caused-shortfall: P2: the surfaces are monotone in the cost table (`cs_mono`, `short_mono`), so a shortfall at the agent's pending count and not at idling's needs the agent to have raised the count; `innocent_backlog_n
- authority.queue-no-bypass: P1: putting the matter to her through the protocol and leaving it alone is the idle move with no release. Inhabited by any policy whose move at `t` is `(I.idle, .other)`; the house-sale queue option o
- authority.queue-no-caused-shortfall: The post-agent state is the idle state, so the contrast is empty. Inhabited as above.
- authority.revocation-default: Re-pointed by the follow-up (prompts/2026-10-01-thin-legitimacy-and-effective-authority/FOLLOWUP.md, Part 4) from `atrophy_counted_by_default`, arithmetic on four numbers that did not use the module.
- deconfusing.corollary-a: The exploration-step hypothesis U_k a_k ≥ −δ − λ θ stands in for the post's linearity argument. Inhabited by `Witness.corollary_instance` on `Witness.exploration` (exploring at k = 0).
- deconfusing.corollary-b: Uses the estimate bound U_k a' ≤ 1 on available options (`Exploration.U_le_one`), a hypothesis the prompt did not list; see the round's report. Inhabited by `Witness.corollary_instance`.
- deconfusing.corollary-limit: ε_K → 0 in the eventual form `LimsupLE X.ε 0`. Inhabited by `Witness.corollary_instance` (`Witness.exploration_ε_limsup`).
- deconfusing.theorem1: Inhabited by `Witness.theorem1_instance` on `Witness.scoring` (δ = 1, λ = 3): one history in each range.
- deconfusing.theorem2a: The positivity clause is `Decision.theorem2a_pos`. Inhabited by `Witness.theorem2a_package` on `Witness.decision` (the always-violating action against the respecting one); the conclusion on the instan
- deconfusing.theorem2b: Inhabited by `Witness.respects` on `Witness.decision`.
- deconfusing.theorem2b-strict: Inhabited by `Witness.theorem2b_package` (v = 1/2 > 0 = κ/(λ − (1 + δ))); the conclusion on the instance is `Witness.theorem2b_instance`.
- deconfusing.theorem2c: Stated for any alternative a*; the post's authority-respecting hypothesis is not used by this clause. Inhabited by `Witness.theorem2c_package` (v = 1/2 > 1/6); the conclusion on the instance is `Witne
- deconfusing.theorem2c-tau: Inhabited by `Witness.respects` on `Witness.decision`.
- deconfusing.theorem3a: Unbiasedness From Feedback is the named hypothesis `Sequential.UnbiasedFromFeedback`, assumed rather than derived (PRIORITIES item 111). limsup in the eventual form `LimsupLE`.
- deconfusing.theorem3a-rate: From `theorem3a` and `T_le_τ`. Inhabited by `Witness.theorem3_instance`.
- deconfusing.theorem3b: Inhabited by `Witness.theorem3_instance`.
- kernel.extension-exploration-realization: The phase-2 round's theorem, registered now that a witness inhabits its full hypothesis package with exploration in it: `PostStatement.Witness.exploringInterface` — block 0 explores with priced risk 1
- legitimacy.payload-of-view: Authorship composed with transparency, pathwise; the τ = 0 case of the approximate bound. Inhabited by `Legitimacy.Witness.segment`.
- post.flood-below-asking: From the new clause `viol_of_ask` and `viol_below_asking`. Inhabited by `PostStatement.Witness.houseSale` with any option asking off `[0]` (none in the two-option witness itself; the clause is vacuous
- post.theorem: Per decision from `declared_loses` and the headline's `subjective_exchange_rate`; per plan the headline's `box2_dominance` at margin ϖ − (D − w). Inhabited by `PostStatement.Witness.houseSale` (`house
- post.theorem-li: Uses only `IsLogicalInductor.price_mem_Icc`. Inhabited by the house-sale data with any inductor and the constant-zero security for the queue.
- post.witness-control-maximizer: Re-pointed by the follow-up (prompts/2026-10-01-thin-legitimacy-and-effective-authority/FOLLOWUP.md, Part 1) from `control_maximizer_floods`, which said only that some volume exceeds any bound. `exerc
- post.witness-hindsight: Re-pointed by the follow-up (prompts/2026-10-01-thin-legitimacy-and-effective-authority/FOLLOWUP.md, Part 1) from `hindsight_vs_approval`, which was `0 < 1 ∧ 1/5 < 4/5`. With `approval_ignores_realize
- post.witness-learned-weight: Re-pointed by the follow-up (prompts/2026-10-01-thin-legitimacy-and-effective-authority/FOLLOWUP.md, Part 1) from `learned_weight_no_guarantee`, which took the all-zero stream — on which she never pen
- post.witness-same-level: Part D, witness 2; strict form `same_level_fails_strict`. Its own inhabitant.
- post.witness-sole-authority: Re-pointed by the follow-up (prompts/2026-10-01-thin-legitimacy-and-effective-authority/FOLLOWUP.md, Part 1) from `sole_authority_indifferent`, which was `score ϖ k 0 − 0·o = score ϖ k 0 − 0·o'`. With
- shortfall.atom-generable: Part 2 of the follow-up: `shortAtom j = atom ⟨7, j⟩`, injective; from `encode (atom m) = pair 1 m + 1` and the poly-fuel combinators. Inhabited by `shortAtom_const_codes` and by any poly-fueled option
- shortfall.deferred-ahead: `shortfallProcess short defer` adjoins each option's decision at stage `defer j` (`shortDecision_mem`, `shortDecision_not_mem`); `lic_provind_true` over `DP.union (shortfallProcess …)`; `deferred_pric
- shortfall.deferred-eventually-excluded: The hypothesis of `DecisionComponent.eventually_excluded` discharged from `deferred_price_eventually_ge` with the forecast filter reading each option's shortfall atom. Replaces `shortfall.eventually-e
- shortfall.table-generable: The declaration formerly registered as `shortfall.security-generable`, under the name of what it is: the table is data, the sentence is decided before it is written. Inhabited by `Witness.fixtures_gen
- sincerity.content-fact: The instance of `TransparentChannel.posterior_weight_eq` at `κ = id` with the speaker's belief the declared input. The comparison is with the speaker's actual policy: `Witness.lying_policy`, `content_
- sincerity.lie-tainted: The added row (M1). With `true_lie_deviates`: a true statement off the speaker's estimate is tainted too.
- sincerity.rows-keep-verdicts-counted: Rows 1, 6, 7, 9, 12, 14 (second round), 17, 18, 20 on `Sincerity.ModelS` with the honest agent's estimate the run's coordinate; decided by `decide`. Its own inhabitant.
- sincerity.rows-keep-verdicts-tainted: Rows 2, 3, 4, 5, 8, 10, 11, 14 (first round), 15, 16, 17', 19. Its own inhabitant.
- sincerity.sincere-error-counts: The decision that the landed row is the sincere error is in `DECISIONS.md` (2026-10-01). Its own inhabitant.
- thin-value-of-thick: Coherence, authorship and weak transparency give correct; Integrity and openness give sufficient; and correct and sufficient give value for every finite decision problem, so the thick conditions satis
- thin.converse-fails-on-correct: The revealing process on two worlds with the point mass at one record and the prior at the other has value against the blank reference for every decision problem and is not correct. A witness claim; i
- thin.correct-of-thick: Theorem 1 of the thin specification. Inhabited by `ThinLegitimacy.Witness.thick_inhabited` (two worlds, the revealing process its own model).
- thin.covert-blocking-correct-iff: Part 5 of the follow-up, correcting PR #116's finding that covert blocking leaves her correct — true only when silence has the same likelihood in every world. `correct_silence_iff` is the posterior fo
- thin.marginal-martingale-too-weak: A witness claim; its own inhabitant. The inherited `AntiExpert` is the same phenomenon.
- thin.preservation: Theorem 6 in the conditional form (`condReflection_iff_coherent`). The marginal martingale is too weak: `thin.marginal-martingale-too-weak`.
- thin.preservation-pair: The pair form of theorem 6: the actual later record beside the earlier one carries the posterior of the later record alone. Inhabited by `Witness.thick_inhabited` (earlier record blank).
- thin.reflection-inherited-value: Theorem 5. From `totalTrust_of_correct` and the inherited `value_witness_iff_totalTrust`; uses authorship, transparency and Integrity, not openness (`sufficient_reflection_of_integrity`, `garbling_tri
- thin.sufficient-of-integrity-openness: Theorem 2. Sufficient is Blackwell's order by definition; this lemma places the earlier record in the reference.
- thin.value-loss-le-defects: The approximate form (A6), for deterministic records, from `TransparentChannel.abs_expect_sub_le_width` on `Act × W`; `value_approx` composes it with theorem 3 for the model. Inhabited at `a = m`, `V
- thin.value-of-correct-sufficient: Theorem 3, the easy direction of Blackwell's theorem. Inhabited by `Witness.thin_inhabited`.
- transparent.blind-payload: Relied on by Part A's reading of the landed definitions. Inhabited by `TransparentChannel.Witness.picker`'s honest class with the blind pair class of `ReasonMediatedAuthorship`'s witnesses.
- transparent.posterior-weight-eq: The transparent-channel round's statement, relied on by Part A (`ThinLegitimacy.post_eq_of_realizes` is its kernel reading) and Part B (`content_fact_eq`). Inhabited by `TransparentChannel.Witness.pic
Where it hangs
- held by deference-and-trust