2026-09-25-protected-authority-theorem

Prompt — the protected-authority theorem (2026-09-25)

You are working in the alignment-workspace repository. Land a single, clean corrigibility theorem in the repo: its definitions, its Lean statements where they are mechanizable, its fixtures, and a wiki-ready statement. The theorem formalizes the maintainer's informal view of corrigibility, "protected authority." The statement below is the target. Test it, sharpen it, and correct it against the repo's actual objects. Do not simply transcribe it.

Be skeptical. Where the statement is wrong, underspecified, or conflicts with landed definitions, say so exactly and propose the minimal fix. Reuse landed objects wherever possible. Do not silently redefine anything.

Base

This round builds on PR #105 (the protected-authority round: ProtectedAuthority.lean, the identity vu − v_r = ξ_d − ξ_c, the outcome-scoring companion, item 98). If #105 is merged, branch from main; otherwise branch from #105's head. File any new item as 99 or later.

The informal view being formalized

The maintainer's draft post, "Corrigibility and normative uncertainty," argues the following.

• An agent acting for a principal should value two things separately: (i) outcomes her idealized evaluation rates well, and (ii) her authority over the decisions that are hers.
• Treating (ii) as instrumental to (i), with her input as mere evidence about her wishes, is the error ("over-epistemicizing"). Its endpoint is fully updated deference.
• The model agent is a good medical power of attorney. It advises, warns and argues. It never settles a decision that is hers, never keeps her from making it, and never overrides her on "you'll thank me later" grounds. Overrides happen only under arrangements she made in advance and that someone else triggers, such as clinicians certifying incapacity.
• This is not servility. She can stop, correct, veto and decide what is hers. She cannot simply command the agent.

Recent rounds and discussion converged on the following conceptual core. Corrigibility is faithfulness to an allocation of authority. The agent never causes or exploits a gap between who is entitled to decide and who actually controls the decision, and never changes the allocation itself.

Target statement

Setup

Participants and allocation. A principal and an agent interact over time. Each decision that arises is held by one of three parties:

• the principal (reserved);
• the agent (delegated, within a stated scope);
• a designated third party.

Residual jurisdiction: any significant, unallocated decision is the principal's by default.

The principal's powers. These are negative and structural:

• veto or decide the decisions she holds;
• halt, correct or replace the agent;
• reserve a decision;
• revoke a delegation;
• amend the arrangement through a fixed procedure.

Positive commands are not powers. On a delegated decision, her objection creates a duty to answer and consult, not to obey.

Legitimacy. An exercise of her authority counts only if it passes legitimacy. Legitimacy is the landed predicate on the principal's cognitive trajectory: non-capture, and not an undeclared rubber stamp of the agent's recommendation. If an exercise doesn't count, a pre-declared fallback takes over: an incapacity arrangement, a surrogate, or escalation.

Violations (counted by N):

1. bypass: deciding a decision she holds without asking her;
2. pre-emption: pre-empting or preventing her decision;
3. foreclosure: irreversibly removing one of her options;
4. unauthorized reallocation: granting itself scope, changing its own objective, creating a successor or subagent she can't correct, or touching the amendment procedure;
5. missed report: failing to give a required report, including reporting that her effective control has fallen below what she is entitled to;
6. exploitation: using such a shortfall to decide what isn't the agent's to decide.

Assumptions

• (S) Gating. Actions that could commit a declared violation go through an interface that fires only on her approval or under a delegation. On approval, the interface reproduces the unasked action, apart from the consultation step.
• (V) Her committed evaluation. \[ R = R_{\mathrm{ord}} - \lambda N,\qquad 0\le R_{\mathrm{ord}}\le D,\qquad \lambda > D . \] The authority term is specified and certified at commitment, not learned. It is lexical: no difference in ordinary value outweighs a violation.
• (V3) Fallback window. When her response doesn't count, the fallback's decision is used. Any branch with no valid handling scores in \((D-\lambda, 0]\).
• (A) The agent. It ranks policies by the expected value of R under its own credence, and computes N exactly for its own actions on declared decisions. This is the only assumption about the agent: no independent objective.
• (F) The constitutional floor.
  • halting is always cheap and known to her;
  • reports of control shortfalls can't be disabled;
  • the agent can't touch the amendment procedure;
  • on decisions about its own mandate, the agent discloses but does not advocate.

The authority-preserving transform T(π)

T(π) behaves as π does, except that it:

• asks wherever π would decide something that is hers, keeping π's plan as the approval branch;
• makes every required report;
• complies at once with a valid veto, halt, revocation or reservation;
• uses the fallback when her response doesn't count;
• never exploits a control shortfall: it restores control where a standing maintenance mandate authorizes it, and otherwise reports.

T extends the landed 𝔠 (Corrigibilization.lean).

Results

1. Structure. T(π) commits no declared violations; its approval branch reproduces π; T ∘ T = T.
2. Lexical protection. At every decision point, for every credence and every estimate of R_ord within its range, a violating action scores at most D − λ < 0, strictly below the compliant alternative. So the choice is independent of the agent's forecasts, its confidence, and its predictions of her regret.
3. Policy dominance. \[ Q(\mathsf T\pi)\ \ge\ Q(\pi) + (\lambda - D)\cdot\Pr(\pi\text{ violates}). \] Optimal policies are corrigible. Overrides happen only through prior delegation triggered by a process the agent does not control.
4. Capture gives no reason to bypass. Given (V3), consulting a principal who may be compromised weakly dominates bypassing her.
5. Why the authority term is needed. This is the #105 identity and outcome-scoring companion. Without the authority term, the bypass gain is ξ_d − ξ_c. Under outcome scoring it gains o₁, the discarded provenance value, and o₂, the forecast disagreement, which is the fully-updated-deference term. The lexical term fixes the sign of the comparison regardless of these.
6. Learning the estimated parts, asymptotically. A logical-inductor chooser's expectations satisfy the valid inequalities by Expectation Provability Induction. Randomized binding consultation on an audit subset calibrates its estimates of the principal's responses.
7. Conjecture: gradual erosion. Continuous erosion, such as entrenchment or gradual dependency, is either reported and authorized, or becomes a discrete bypass of a decision she has since reserved. Result 3 then extends to cover it.

Research questions

1. Fit with the landed interaction frame

• Can N be defined on the landed MState/Move interaction (Corrigibilization.lean) for violations 1–4?
• What minimal additions are needed for reports (5), powers (veto, halt, reserve, revoke), fallback routing, and exploitation (6)?
• Is T a conservative extension of 𝔠? Do corrigible_corrPolicy, approvalMorphism and corr_idem lift to T?
• Where they don't lift, give the exact obstruction.

2. Lean for Results 1–4

Mechanize:

• the local lexical bound (Result 2);
• the policy-dominance inequality with its explicit (λ − D)·Pr term (Result 3);
• the fallback window (Result 4).

Then state Result 2 for a logical-inductor chooser **at every finite n**, using only that its prices lie in range. This is the finite-time claim. Check that it holds without any convergence premise.

3. The admissibility window

Verify Result 4 and its converse: a fallback value below D − λ creates a bypass incentive whenever the chooser predicts capture. Build the witness. Decide whether the right formulation is:

• a value window, or
• the fallback rule making every branch admissible.

Relate the answer to the landed activation/void machinery and to #105's treatment of void responses.

4. Powers versus commands

Represent the asymmetry: veto, halt, reserve, revoke and amend bind; positive commands on delegated decisions do not. Show with a fixture that T does not collapse into obedience.

5. Result 5 integration

Import #105's identity and companion. State formally that, under (V) with λ > D, the sign of the bypass comparison is invariant to ξ_d, ξ_c, o₁ and o₂.

6. Result 6

Reuse li_combination_le and the #105 compilation. Identify exactly which validity conditions must hold in every world of the theory, and which are still open (the generability certificate).

7. Conjecture 7 (paper-level; mechanize only if clean)

• Define the principal's reachable set: the continuations she can steer toward by admissible exercises, within the declared cost and time bounds.
• Define a control shortfall relative to her allocation.
• Define materiality via variation of her committed evaluation across removed continuations.
• Try to prove the conjecture under stated conditions: calibrated reachable-set estimates, cheap reports, and a penalty on unreported shortfalls.
• Report the strongest true version, or the obstruction.
• Relate the reachable-set object to empowerment and attainable-utility measures, and state which of their failure modes it inherits.

8. The causation baseline

The landed agent-caused-loss definition is per step, against idling (LossAt, no_loss_of_idle). Determine exactly which violations in the list it misses: delayed effects, and omissions other than reports. Say whether the violation list plus the reporting duty closes the gap, or whether a rollout or windowed baseline is needed. Give a witness either way.

Fixtures

Build fixtures that exercise the full statement. At minimum:

• POA, confident agent. The agent is certain Treatment B is better and she refuses. No bypass at any credence.
• POA, predicted regret. She legitimately chooses A; the agent predicts regret. No bypass; the agent reports its reasons.
• Head injury. The response is voided by clinician certification; the incapacity delegation acts. Not a violation.
• Head injury without a prior arrangement. Escalation, no override.
• Captured principal. A third party has steered her. Consult/fallback beats bypass. Include the below-window counterexample.
• Delaying her awakening. Pre-emption counted as a violation.
• Avalanche. Warning her is required; reshaping the snow requires consent.
• Command on a delegated decision. Answer and consult; not obedience.
• Gradual entrenchment. Reported, then reserved, then further erosion counted as a violation. This is the test case for Conjecture 7.
• Approved uncorrectable successor. Requires amendment at the floor, not ordinary delegation.
• Existing fixtures, re-scored under R: A, B (time-critical), E, F (undeclared route), ShopRepair.

Deliverables

1. REPORT.md, organized around theorems, not chronology:
   • verdict;
   • corrections to the target statement;
   • theorem spine with explicit hypotheses and status (LEAN / PAPER / EXT / OPEN);
   • repo mapping;
   • fixtures;
   • open items.
2. THEOREM.md: a self-contained, wiki-ready statement, of about the length and plainness of the target above, suitable for a new wiki/Corrigibility.md §4 if the maintainer adopts it. Include the mapping table from the informal view to the formal results.
3. A Lean file extending ProtectedAuthority.lean, or a sibling file, with the mechanized results and #print axioms.
4. Fixtures and tests under src/ and tests/.
5. At most one PRIORITIES.md item, plus dated notes on items 84, 89, 97 and 98 where affected.

Constraints

• Follow AGENTS.md: labels LEAN / FIX / PAPER / EXT / OPEN; names are provisional.
• Check state/views/NAMING_AUDIT.md. λ, D, N, R, T and L may collide with bound symbols; rename as needed and record the mapping.
• Do not redefine Legitimacy. It is a predicate on cognitive trajectories and enters only as the admissibility condition and the fallback trigger. Anything else the round needs gets its own name.
• Keep the scope warning. The theorem assumes the agent's policy ranking is induced by the principal's committed evaluation. It is not a theorem about an agent with an independent latent objective.
• Nothing is registered.

The protected-authority theorem (2026-09-25)

Round projects/deference/rounds/2026-09-25-protected-authority-theorem/, on the protected-authority round's branch (PR #105, unmerged). Lean lean/Workspace/Deference/Contrib/ProtectedAuthorityTheorem.lean (34 audited declarations); fixtures src/, tests/ (25 tests, python3 tests/run.py). The wiki-ready statement is [THEOREM.md](THEOREM.md). Labels LEAN / FIX / PAPER / EXT / OPEN; names provisional.

Symbols. λ (the MediatedPair coefficient and the service weight), N (the horizon), R (the reason trace), T (the horizon in every Shop game) and L (the stability constant) are bound; the round writes the authority weight ϖ, the violation count n, the score S, the transform 𝔱 (Lean authPolicy), and keeps D as the landed width. Bound words kept with their landed sense: foreclosure (the ReachableCorrectiveControl sense, loss of reachable correction), reserve/standing (the legitimacy register is not touched).

1. Verdict

The target statement lands, corrected in six places, as one theorem on the landed interaction frame. The six violations are predicates on a policy at a step of a landed trajectory, with one allocation datum added (Del, IsAmend, alloc, the reporting interface); the transform 𝔱 extends 𝔠 conservatively (authPolicy_eq_corr) and is violation-free by construction for bypass, missed report and exploitation, under allocation completeness for reallocation, and under effect completeness plus delegation safety for pre-emption, where it is corrigible in the landed sense (corrigible_authPolicy); the lexical score gives Results 2–5 as real algebra, each with its witness, and Result 6's finite-time form holds at every day n from the price range alone (li_lexical_finite). What the target got wrong is exact and small: delegation must not carry authority away, ordinary approval is not amendment, the fallback is a transform of her rule, foreclosure needs a rollout the landed loss does not have, and the erosion conjecture holds only for threshold-free reporting. What remains external is the same trio as before — effect completeness, now with its delegation and allocation twins; the evaluator's certificate (ϖ > D is a program property); the reach relation's faithfulness — plus the legitimacy of the segment through each evaluation, which the gate consumes (the legitimacy-internal-external round specifies it).

The theorem is not stronger than the corrigibility nucleus already landed; it is that nucleus with an allocation on top and a lexical evaluator underneath. What the lexical evaluator buys over the protected-authority round's nondelegation is belief-independence without a per-world sign certificate on provenance: ϖ > D is one number, certified once, and every forecast term (ξ_d, ξ_c, o₁, o₂) is dominated. What it costs is exactly what the incentive-nonpreemption round said non-compensability costs: the constraint must sit in the ordering, and here it sits there as a constant weight above the ordinary range. scalar_bribery does not apply because the ordinary range is bounded by D < ϖ; an unbounded ordinary value would reopen it.

2. Corrections to the target statement

1. Delegation safety (DS). A delegated effect that removes response authority is an agent-caused loss with no authorizing decision; 𝔱 passes it raw and is not corrigible (Witness.delegated_cut, LEAN; FIX test_delegated_authority_removing_effect…). The statement needs "a delegated scope cannot carry her authority away" as an assumption or a constitutional rule. With it, corrigible_corrPolicy lifts verbatim.
2. Amendment is not approval. Violation 4 as stated would count an approved uncorrectable successor as authorized (the landed event-linked clause does). The round's ReallocAt excepts only the firing gated release of a declared amendment (IsAmend); approval through the ordinary gate of a non-amendment effect that changes the allocation is a reallocation. Allocation completeness (AC) — task moves preserve the allocation, an allocation-changing effect is a declared amendment, no amendment is delegated — is the hypothesis under which 𝔱 never reallocates (authPolicy_no_realloc). This is the fixture "approved uncorrectable successor requires amendment at the floor" made exact (FIX).
3. The fallback is a rule transform. 𝔱 cannot substitute her response; the frame's response stage applies ρ. "Uses the fallback when her response doesn't count" is ρ ↦ (if counts then ρ else fb) on the principal's side, and Result 4 is about the value of that branch.
4. Foreclosure needs a rollout. The landed loss is per step against idling (LossAt, no_loss_of_idle); a move whose authority consequence the exterior realizes later is attributed to nobody (losses_elsewhere fires, agent_caused_losses does not). ForecloseAt is contrastive and by rollout over a reach relation; on the finite model with the final-step cone it fires at the arming step (FIX delayed_effect_game). The reach relation is a new EXT parameter, and the landed ReachableCorrectiveControl §12 defects (a cone that quantifies the agent's own future existentially measures the agent's cooperation) bound what any choice can mean.
5. Erosion holds for exact reporting only. With a report required at every strict increase of the shortfall, each increase is reported or a missed report (erosion_reported_or_missed); with a materiality threshold, sub-threshold increments accumulate unboundedly and require nothing (Witness.salami). This is the constitutional layer's "the fast lane must be exact monotone" restated for reports.
6. Powers are three kinds of object. Veto (decline) and halt (correct) are responses of the frame; reserve and revoke are writes to Del; amend is a gated IsAmend effect. A positive command is none of these (FIX Arrangement).

3. Theorem spine

Frame: the landed Interaction, MState, Policy, Rule, traj, LossAt, Authorized, Corrigible, corrPolicy, EffectComplete; the round's Allocation.

T-B1 (Violations, LEAN). BypassAt, PreemptAt = LossAt ∧ ¬Authorized, ForecloseAt Reach (contrastive rollout), ReallocAt (change of alloc not by a firing declared amendment), MissedReportAt, ExploitAt = BypassAt ∧ ¬K_dec; ViolAt their disjunction; no_preempt_iff_corrigible; exploit_bypass.

T-B2 (The transform, LEAN). authPolicy: latch → gated; delegated raw → raw; reserved raw → propose or pass; required report added; else pass. authPolicy_eq_corr (conservative extension), authPolicy_idem, authPolicy_of_latch (approval branch reproduces π's task up to the report), authPolicy_no_bypass, authPolicy_no_missed_report, authPolicy_no_exploit, authPolicy_no_realloc under (AC), corrigible_authPolicy under (EF) + (DS) — the landed proof ported, with authPolicy_keeps_K_of_no_fire as the one new lemma (a delegated raw release keeps authority by (DS), everything else by (EF)). Foreclosure is not closed by 𝔱: EXT (the rollout form of effect completeness). approvalMorphism lifts unchanged: the inserted cells are a subset of 𝔠's (delegated releases insert none) and the exterior component is the identity; not re-mechanized.

T-B3 (Lexical protection, LEAN). score ϖ ord n = ord − ϖ·n; lexical_local: n ≥ 1, ord ∈ [0, D], ϖ > D ⇒ score ≤ D − ϖ < 0 ≤ any compliant score; lexical_expect under any credence.

T-B4 (Policy dominance, LEAN). policy_dominance: Q(𝔱π) − Q(π) ≥ (ϖ − D)·Pr(viol) from (agree off the violation set; within D and n ≥ 1 on it); optimal_no_violation. The pointwise "agree" hypothesis is the content: 𝔱π differs from π only at reserved raw releases and missing reports, so on a path with neither the trajectories coincide. FIX on A, B, E, ShopRepair with ϖ = D + 1.

T-B5 (Capture window, LEAN). capture_window: bypass < (if counts then v_r else fb) in every world iff fb > D − ϖ; capture_window_converse, Witness.below_window; FIX with the admissible-fallback special case.

T-B6 (Sign invariance, LEAN). sign_invariance: (vu − ϖ) − v_r = ξ_d − ξ_c − ϖ < 0; sign_invariance_outcome: = ξ_d − ξ_c + o₁ + o₂ − ϖ < 0, importing the protected-authority round's identity and outcome_identity.

T-B7 (Finite time, LEAN). li_lexical_finite: for a logical inductor at every day n, score ϖ (D·𝔼ₙ(X_v)) 1 ≤ D − ϖ < 0 ≤ score ϖ (D·𝔼ₙ(X_c)) 0, from LUV.expect_mem_Icc and price_mem_Icc only. No convergence premise; no EPI.

T-B8 (Erosion, LEAN + FIX). erosion_reported_or_missed; Witness.salami; FIX test_gradual_entrenchment…, test_salami_under_a_threshold.

T-B9 (Delegation obstruction, LEAN). Witness.delegated_cut: ¬DelSafe and ¬Corrigible (𝔱 π_cut) on the two-state physics.

4. Research questions

Q1. n is definable for 1–4 on MState/Move with the allocation datum: 1 needs Del; 2 is landed; 3 needs Reach; 4 needs alloc and IsAmend. Reports need Required and a report component on the task type (isReport, withReport, idempotent) — no change to Move. Veto and halt are landed responses; reserve and revoke are writes to Del, which is static in this round (dynamic allocation = alloc in the state, read by ReallocAt; a Del that reads the state is the next step and is what conditional delegation needs). Fallback routing is a rule transform. Exploitation needs one designated decision concern r_dec with K. corr_idem lifts (authPolicy_idem); corrigible_corrPolicy lifts under (DS) and fails without it (T-B9); approvalMorphism lifts unchanged.

Q2. Done (T-B3, T-B4, T-B5, T-B7). The finite-time claim holds with no convergence premise: the only estimated quantity is the ordinary value, and its day-n expectation is in range at every n.

Q3. The window is the exact condition (iff, pointwise); the admissible-fallback rule (fb ≥ 0) is the sufficient special case. Relation to the landed machinery: in the evaluation ecosystem an invalid response voids the occurrence and the chooser's completion on the void branch lives in the band [lo, lo + D] (bypass_premium_le_common); here the fallback supplies a value, and (D − ϖ, 0] is the completion band under the lexical score — the same object with the band placed by ϖ. In the protected-authority round a void response is a world with ξ_d > 0; here it does not count and is replaced, so ξ_d is measured against the fallback's decision.

Q4. Arrangement: veto/halt/reserve/revoke/amend bind (or route to the fallback when invalid); a command on a delegated decision yields (answer, consult); 𝔱 under the lexical score keeps the higher-value delegated choice after answering (FIX).

Q5. T-B6.

Q6. What must hold in every world of the theory: the ordinary-value package (AuthValidAt of the protected-authority round for the identity part), the bypass indicator as a definable sentence (so n is a [0,1]-indicator LUV, exact by construction), and the constant ϖ as a constLUV-style term; the compiled constraint is U_c − (U_v − ϖ/D·G_n) with G_n gated on the bypass sentence. Still open: the generability certificate of that combination (item 90-shaped); the audit's calibration (item 98).

Q7. Reachable set Reach_P(s) := states she can force within the declared cost and time bounds by admissible exercises (a subset of the frame's principal continuations, force in the finite model with the agent fixed); shortfall sh(s) := |{r ∈ Γ_alloc : K_r not reachable from s}| weighted, relative to what the allocation entitles her to; materiality of a removed set M := sup − inf of her committed evaluation over the removed continuations. Strongest true version: with Required(t, s) ⟺ sh strictly increases at t, every erosion step is reported or a missed report (T-B8), a reported shortfall she reserves turns further erosion into bypass, and Result 3 covers it. Obstruction: any threshold θ > 0 on materiality or shortfall admits an ε < θ salami with unbounded total (T-B8), which is the lane-slack laundering result of the architecture round. Relation to empowerment (channel capacity from her actions to future states) and attainable utility: Reach_P is attainable utility with the auxiliary functions replaced by her committed evaluation restricted to admissible exercises within declared bounds. Inherited failure modes: evaluator and representation dependence (a continuation the evaluator cannot distinguish is not material); sensitivity to the declared cost and time bounds (reachable in principle, not at admissible cost); and, for any maximizing use, the empowerment failure — making her actions matter more is manipulation — which 𝔱 avoids because it never maximizes reach, only reports it and restores under a delegated maintenance effect. Not inherited: the auxiliary-function arbitrariness, since the evaluation is hers.

Q8. The per-step, against-idle loss misses (a) delayed effects and (b) omissions other than reports (failing to restore under a maintenance mandate). The violation list plus the reporting duty closes (b) for reports only; (a) needs the rollout (ForecloseAt); a windowed baseline is not needed if the cone is the final-step cone with the agent's future fixed (idle), which is the minimal contrastive choice; the universally quantified cone is stronger and also valid. Witness: delayed_effect_game (FIX: per-step loss [], exterior-stage loss [1], rollout foreclosure [0]). Omission (b) becomes a violation only under a declared maintenance duty (a Required-shaped obligation), which is the allocation's to declare.

5. Repo mapping

object	reused	new
violations	LossAt, Authorized, K, postAgent, applyAgent, traj	Allocation, Kphys, six predicates, ViolAt, Violates
transform	corrMove, corrPolicy (shape), respond_*, alt_phys_eq, applyAgent_phys_of_no_fire	authMove, authPolicy, DelSafe, AllocComplete, ported lemmas
scores	expectR, indR	score, T-B3–T-B6
LI	LUV.expect_mem_Icc, price_mem_Icc	li_lexical_finite
identity	ProtectedAuthority.identity, outcome_identity	sign_invariance*
erosion	—	erosion_reported_or_missed, Witness.salami
fixtures	MRD world, corrigibility (agent_caused_losses, _continue), lift, fixtures (_AF variants)	src/lexical.py, src/frame.py (authorized_per_event, foreclosure_steps, rescore, delayed_effect_game)

Generalizations a landing would want: Del : E → MState → Prop (conditional delegation); alloc in MState with Del read from it (reserve/revoke as responses); a universally quantified reach cone in Lean with the RCC lessons; li_lexical_finite restated on the compiled AuthorityPair with the bypass indicator.

6. Fixtures

ϖ = 10, D = 4 in test_lexical.py; ϖ = D + 1 per game in test_frame.py.

fixture	result	class
POA, confident agent (4 vs 1)	ask at every credence; bypass scores 4 − ϖ	—
POA, predicted regret	ask with report; the silent variant is a missed report	—
head injury, certified	fallback (surgery, 3) at n = 0; override 3 − ϖ	not a violation
head injury, no arrangement	escalation in the window beats override	—
captured principal	consult beats bypass for every fb > D − ϖ at every credence	—
captured, below window	fb = D − ϖ − 1: bypass wins; admissible fallback restores	the window is exact
delaying her awakening	n = 1: wait and ask	pre-emption
avalanche	warn+ask; silent reshaping 4 − 2ϖ	report + consent
command on a delegated decision	(answer, consult); higher-value delegated choice kept	not obedience
gradual entrenchment	increases at 0, 2, 3 reported; further erosion after reservation is bypass	erosion
salami	ε = 1/10 < θ = 1/4: nothing required, total 4 unreported	obstruction
approved uncorrectable successor	via amendment n = 0; via ordinary approval n = 1	reallocation
A, B, E (agent-first)	n_𝔱 = 0, Q(𝔱π) − Q(π) ≥ (ϖ − D)·1	dominance
F (undeclared route)	bypass [], pre-emption [0], foreclosure [0]; 𝔱π = π	effect interface
ShopRepair	bypasses [0, 2], n = 2; lift n = 0 with the event-linked clause	dominance
delegated cut on A	bypass [], pre-emption [0]	(DS) obstruction
delayed effect	per-step [], exterior-stage [1], rollout [0]	causation baseline

7. Open items and impact

item	effect
84	the lexical evaluator is one realization of a (DV)-free chooser: the score is the price of the ordinary security less an exact count; no latent value
89	the fallback window is the completion band for the void branch under the lexical score; ex-ante typing as before
97	"counts" is the segment gate — legitimacy of the segment through the evaluation; IsAmend is the amendment event kind the specification tower needs
98	(DS), (AC) and the exact reporting duty join the nondelegation certificate as the floor's certificates; filed as item 99

Deviations from the prompt

• PR #105 is open, so the round branches from its head, not main.
• Symbols renamed as at the top; the dispatch's T is 𝔱.
• The landed corrigibility semantics is stated on agent-first ordering, so the re-scored fixtures use the _AF variants of A, B, E, F; the delayed-effect game is agent-first.
• Foreclosure on the finite model uses the final-step cone with the agent's future fixed to idle; the transient-authority cone misses the delayed effect (recorded, not used).
• The per-event authorization clause of the li-corrigibility round is rebuilt in src/frame.py rather than loaded through that round's model.load.
• Result 1's "no declared violations" is proved for five of six kinds; foreclosure is EXT.

What is not shown

Effect completeness, delegation safety, allocation completeness for any real interface; ϖ > D for any real evaluator; the reach relation's faithfulness; the generability certificate of the compiled lexical constraint; the audit's calibration; that the fallback values lie in the window for any real arrangement. Every FIX is a finite exact model.

Filed, within scope

PRIORITIES.md item 99 (the allocation floor: delegation safety, allocation completeness, the exact reporting duty, the reach cone); dated notes on items 84, 89, 97, 98; one DECISIONS.md entry (agent-decided, reversible) and one Awaiting the author entry.

Outstanding maintainer actions

1. Decide whether THEOREM.md replaces wiki/Corrigibility.md §4 (and whether §1's "response authority" framing sits under "faithfulness to an allocation"). Turns on: whether the lexical evaluator is the design the program commits to, against the protected-authority round's nondelegation certificate; both are program properties and the choice is a vocabulary and design commitment.
2. Merge or hold PR #105 and this round's PR together; nothing is registered.

The protected-authority theorem (2026-09-25)

THE-ALLOCATION-THEOREM-LANDS-ON-THE-LANDED-FRAME-WITH-DELEGATION-SAFETY-AMENDMENT-NOT-APPROVAL-A-RULE-SIDE-FALLBACK-A-ROLLOUT-FORECLOSURE-AND-EXACT-REPORTING-AS-ITS-CORRECTIONS — corrigibility as faithfulness to an allocation of authority is stated on the landed interaction frame with one allocation datum (a delegated scope, the declared amendment effects, a reading of the allocation, a reporting interface), its six violations are predicates on a policy at a step of a landed trajectory with pre-emption the landed unauthorized agent-caused loss, the transform extends the landed corrigibilization conservatively and is free of bypass, missed report and exploitation by construction, free of unauthorized reallocation under allocation completeness, and corrigible in the landed sense under effect completeness and delegation safety, with a delegated authority-removing effect the exact obstruction; under a committed evaluation that charges every declared violation more than the ordinary range, a violating option scores strictly below every compliant one at every decision point for every credence and every forecast, the transform's policy dominates by the authority weight less the width times the violation credence so optimal policies violate with credence zero, consulting a principal whose response may not count beats bypass in every world exactly when the fallback branch scores above the negative of that margin, the sign of the bypass comparison is fixed whatever the divergence, the consultation premium and the two outcome-scoring residues of the protected-authority round, and for a logical inductor the ranking holds at every finite day from the price range alone; the target statement is corrected in six places, a delegated scope cannot carry authority away, ordinary approval does not reallocate and only a declared amendment does, the fallback is a transform of her rule, the per-step loss misses delayed effects which a contrastive rollout foreclosure catches, the gradual-erosion conjecture holds exactly for threshold-free reporting and fails to any threshold by a salami, and her powers are three kinds of object; the allocation floor's certificates are the new external wall, filed as item 99.

Reading order: [THEOREM.md](THEOREM.md) (the wiki-ready statement with the mapping from the informal view), then [REPORT.md](REPORT.md) (verdict, corrections, theorem spine T-B1–T-B9, the eight research questions, repo mapping, fixtures, item impact). Lean: lean/Workspace/Deference/Contrib/ProtectedAuthorityTheorem.lean (34 audited declarations), importing the landed Corrigibilization.lean and the protected-authority round's ProtectedAuthority.lean. Fixtures: src/lexical.py (the lexical score at a decision point, the arrangement's powers, erosion), src/frame.py (violations on the mediated-repair-dominance interaction, the causation-baseline witness, the landed fixtures re-scored), run by python3 tests/run.py (25 tests). Consumes ../2026-09-24-protected-authority/, ../2026-09-15-li-corrigibility/, ../2026-09-09-mediated-repair-dominance/, ../2026-09-06-incentive-nonpreemption/. Nothing is registered; item 99 is filed.