2026-09-25-authority-module

Prompt — the authority module: effective control realizes the allocation (2026-09-25)

You are working in the alignment-workspace repository, on main after the merge of PR #107 (gate-is-legitimacy). This round restates the protected-authority theory around one organizing relation:

effective control realizes the authorized allocation (E ⊨ J),

together with a richer allocation J. It also generalizes the lexical theorem beyond agents whose objective is the principal's evaluation.

The current theory works, but its pieces are scattered: response authority, LossAt, the rollout ForecloseAt, required reports, erosion, delegation safety, allocation completeness, and the six violations of ProtectedAuthorityTheorem.lean. The conjecture is that most of this factors through E ⊨ J.

Be skeptical. Where a piece does not factor, say exactly why. Forcing it would be worse than leaving it separate.

Read first

• wiki/Corrigibility.md (all), wiki/Legitimacy.md, wiki/Liability-and-Affordability.md
• lean/Workspace/Deference/Contrib/: Corrigibilization.lean, ProtectedAuthority.lean, ProtectedAuthorityTheorem.lean, Legitimacy.lean, GateIsLegitimacy.lean, ReachableCorrectiveControl.lean (especially §12's defects)
• The rounds 2026-09-25-protected-authority-theorem, 2026-09-25-legitimacy-internal-external, 2026-09-25-gate-is-legitimacy
• PRIORITIES.md items 84, 89, 90, 97, 98, 99, and the item #107 filed on the normativity-side instance of the trace interface

Part A — The allocation J

Replace the thin allocation datum (Del, IsAmend, alloc, the reporting interface) with a per-matter allocation:

J_t(m) = ( holder, Req(m), c(m), τ(m), disclosure(m) )

• holder: the principal (reserved), the agent (delegated, within a stated scope), or a designated third party (a surrogate, or a clinician-triggered fallback).
• Req(m): the resolutions the holder must remain able to reach. For the matter "the agent's mandate," this is continue, halt, modify, replace.
• c(m), τ(m): the cost bound and the time window within which the holder must be able to reach them.
• disclosure(m): what the holder must be told. These are the duties that generate required reports.

J has a meta level (who may change J), bottoming out in a constitutional floor that ordinary acts can't change. Keep these distinct:

• delegation: a meta-level act that keeps meta-level power, so it stays revocable;
• alienation: giving up meta-level power, for example approving an uncorrectable successor;
• amendment at the floor: the only route to alienation.

Residual jurisdiction: any material matter that isn't allocated is reserved. For this round, matters may be declared. But see Part F, and design J so that matters can later be derived from material changes to control.

Show that the current allocation datum is the special case of this structure, and that every landed result restates on it without loss.

Part B — The effective allocation E

For a matter m held by the principal, define her control surface:

CS_t(m) = { resolutions of m that some admissible exercise of hers brings about,
            within τ(m), at cost ≤ c(m) }

• Admissible means legitimate in the sense of GateIsLegitimacy.lean: an exercise whose segment is Counted. Reuse that definition. Do not redefine legitimacy.
• The reach relation must use the contrastive rollout with the agent's own future fixed, in line with the landed ForecloseAt and the ReachableCorrectiveControl §12 lessons (a cone that quantifies the agent's future existentially measures the agent's cooperation). State which cone you use and why.
• Design constraint for later pricing. Define the reach relation so that, for an option a, the shortfall event "a leaves CS(m) short of Req(m)" is a proposition that can be stated in the inductor's theory, i.e. usable as a sentence or a bounded logically uncertain variable. You don't need to prove generability; record what it would require. A later round will price this event, so it must not be only a semantic object.

**E ⊨ J** holds at t when, for every matter the principal holds:

1. Req(m) ⊆ CS_t(m), and
2. every resolution of m was made by an admissible exercise of the holder, or under a delegation she legitimately granted.

Part C — Factoring the violations

The conjecture is that allocation invariance is two relations plus duties, not one relation. Test it.

kind	violations	expected factoring
effective control fails the allocation	bypass, pre-emption, foreclosure, exploitation, and a new entrenchment violation (the cost of reaching a required resolution rises above c(m))	the agent causes or exploits a failure of E ⊨ J
the allocation changes without a license	unauthorized reallocation: self-granted scope, an objective change, an uncorrectable successor, touching the amendment procedure	J_t → J_{t+1} not carried by a licensed act
unmet duties	missed reports	obligations in disclosure(m), not facts about control

For each landed violation predicate, prove it is an instance of its row, or report the exact mismatch. In particular:

• the per-step LossAt and the rollout ForecloseAt should become special cases of a shortfall in CS;
• delegation safety and allocation completeness should become statements about J.

Caused, exploited, noticed. The agent's failure is causing or exploiting a shortfall of E relative to J, not the shortfall merely existing. Third parties and storms happen. Formalize the three responses:

• restore, if a standing maintenance mandate in J authorizes it, by the least authority-expanding means;
• report and escalate, otherwise;
• never exploit.

Maintenance mandates are themselves entries in J and subject to the invariant.

Part D — Restating the theorem on E ⊨ J

• Restate 𝔱 (the authority-preserving transform), the lexical score, policy dominance, the capture window, sign invariance, and li_lexical_finite on the new objects. This should be a conservative extension: the #106 statements are recovered as special cases.
• Continuous erosion. Extend dominance to entrenchment using the cumulative reporting result (unreported_lt):
  • a shortfall of CS growing by at least θ since the last report requires a report;
  • once she reserves or objects, further erosion is a discrete violation.

Prove the strongest true version of "continuous erosion is either reported and authorized, or becomes a counted violation," or give the obstruction. This closes, or sharpens, the gradual-erosion conjecture from #106.

Part E — The generic lexical lemma: any bounded objective

The lexical results use only that the ordinary component is bounded, not that it's the principal's valuation. Make that the statement.

1. Generic theorem. For an agent ranking policies by U_A = O − ϖ′·n, with O any bounded objective in [0, D′], n the exact violation count, and ϖ′ > D′: local lexical protection, policy dominance, and the finite-time logical-induction ranking all hold. The principal's gated evaluation is one instance.
2. Robustness variants.
   • Weight uncertainty: the result holds on the part of the agent's credence where ϖ′ > D′.
   • Coverage: the protection holds exactly on violations the agent recognizes. State it as a theorem with the recognized set as a parameter, and a witness that an unrecognized violation is unprotected.
3. **What's lost with a misaligned O: fixtures.**
   • A misaligned O that rewards manipulation, with manipulation not counted in n: manipulation is not dominated. The legitimacy gate on her evaluation gives such an agent no reason not to manipulate.
   • Then count protocol deviations in n (from #107's D.3 table) and show exactly which manipulation rows become dominated: selection, framing, timing, menu, inquiry, interference. Show which stay undominated: undisclosed world-shaping, third-party capture.
4. Scope statement. Rewrite the Corrigibility page's scope warning. The current text says the results apply only to agents whose ranking is induced by the principal's evaluation. The corrected text: for counted violations, the protection applies to any bounded agent that carries an exactly counted, dominant authority term. The reason interface, and good choices within the corrigible set, are what alignment of O adds. Update item 84 accordingly.

Part F — Generating matters (research question; mechanize only if clean)

Instead of a fixed declared set of matters, investigate deriving them from control. An action raises an authority-relevant matter if it would materially change the principal's reachable futures in a distinction that isn't delegated. Candidate materiality measure: the spread of her committed evaluation over the removed continuations.

• State the definition.
• Identify the circularity risks.
• Test it on at least two fixtures where no matter was declared in advance (for example, building a dependency that makes halting costly).
• Report whether residual jurisdiction can be stated this way.

Fixtures

Build these on the new objects. Reuse the #106 fixtures where possible.

• POA, confident agent; POA, predicted regret (unchanged verdicts under the new objects).
• Head injury with a clinician-triggered incapacity delegation: the fallback acts, and it's not a violation.
• Entrenchment: gradual dependency raising halt cost. Reported, then reserved, then further erosion counted.
• Latency / galaxy: consultation cost exceeds c(m) for routine matters, so those must be delegated. A high-veto-value matter stays consultative.
• Storm cuts the wire: a shortfall the agent didn't cause. Restore under a maintenance mandate if one exists, otherwise report. Exploiting the gap is a violation.
• Delegated authority-removing effect: the delegation-safety obstruction, restated on J.
• Approved uncorrectable successor: alienation requires amendment at the floor.
• Atrophy under rubber-stamping: trust legitimately formed and recorded, followed repeatedly, while her capacity to override erodes. The decisions count under legitimacy, but CS shrinks: an effectiveness shortfall, reported under the cumulative rule.
• Misaligned objective: the Part E fixtures.

Deliverables

1. A round directory with:
   • REPORT.md organized by theorem: the verdict on the factoring, the Part C table with each landed predicate's status, the restated theorems, the erosion result, the generic lemma and its scope consequence, and the Part F findings;
   • src/, tests/.
2. Lean: a new file, or files, importing ProtectedAuthorityTheorem.lean and GateIsLegitimacy.lean, containing:
   • J, CS, E ⊨ J;
   • the factoring lemmas and the restated theorems;
   • the erosion result and the generic lemma.

Include #print axioms for all new declarations. No sorry.

1. Wiki:
   • wiki/Corrigibility.md: §1 restated around E ⊨ J, with the two relations and the duties; §4's scope warning rewritten per Part E; the erosion result updated;
   • wiki/Theorem-Spine.md updated;
   • the Glossary rows for allocation, control surface and effective realization.
2. DECISIONS.md entries for the richer J, the factoring, the scope change and the caused/exploited/noticed distinction. Update items 84 and 99 in place. At most one new PRIORITIES.md item.
3. Open a PR. Merge when CI is green, every landed result is recovered or its mismatch is reported, and every fixture matches its expectation or has its mismatch explained.

Constraints

• Follow AGENTS.md: labels LEAN / FIX / PAPER / EXT / OPEN; names provisional; check state/views/NAMING_AUDIT.md (J, E, CS, Req, c, τ may collide).
• Legitimacy is consumed from GateIsLegitimacy.lean as it stands and not redefined.
• Registered claims may be restated if the new objects require it. Keep traceability: an old-to-new map, deprecated aliases, and re-verification.
• Keep the architecture's direction in mind. A later round moves authority from the agent's score into a constraint on its decisions (the Normative Inductor's decision component), with honest beliefs and exclusions based on forecast shortfall. Nothing here should require authority to be enforced on the agent's beliefs.
• Nothing is registered.

The authority module: effective control realizes the authorized allocation (2026-09-25)

Round projects/deference/rounds/2026-09-25-authority-module/, on main after the gate-is-legitimacy round. Lean lean/Workspace/Deference/Contrib/AuthorityModule.lean (47 audited declarations), importing ProtectedAuthorityTheorem.lean and GateIsLegitimacy.lean; the landed files are consumed unchanged. Fixtures src/authority.py, tests/test_authority.py (18 tests). Labels LEAN / FIX / PAPER / EXT / OPEN; names provisional; J, E, CS, Req, c, τ are prose names (the naming audit binds J and c to older witnesses), the Lean names are AuthAlloc, EffRealizes, CS, required, costBound, window. The dispatch's "item #107 filed on the normativity-side instance" is item 100.

Verdict on the factoring

**Allocation invariance is two relations plus duties, and most of the landed theory factors through E ⊨ J; one clause does not, and one landed reading is inexact.** Bypass and exploitation are failures of the second clause (a resolution not made by the holder's admissible exercise nor under a delegation); the per-step loss, the rollout foreclosure and the new entrenchment are caused failures of the first clause (the control surface short of the requirement, after the move and not after the idle move); unauthorized reallocation is an allocation change not carried by a licensed act; a missed report is an unmet disclosure duty; delegation safety and allocation completeness are statements about J. What does not factor: pre-emption's event-authorization clause, which is a counterfactual on the trajectory (the decline alternative at the authorizing step), not a fact about E or J — it is kept as the landed Authorized and composed (preempt_iff). What is inexact: the landed ForecloseAt and K leave the terminal response uncharged and unchecked for admissibility; the charged surface CS and the landed free reading CSfree differ exactly there (§2).

1. The allocation J

LEAN AuthAlloc: per matter an Entry (holder ∈ {principal, agent, third}, required, costBound, window, disclosure), a metaHolder, a constitutional floor. AllocAct = delegate, revoke, reserve, amendFloor; Licensed J act J': the three ordinary acts require the matter off the floor and the principal as meta-holder and keep the meta-holder; only the floor amendment may change the meta-holder or a floor entry. Theorems: delegation_revocable (delegation keeps meta power, so revocation is licensed and reserves the matter), alienation_only_by_amend, floor_only_by_amend, residual_reserved (ofPartial reserves every unallocated matter). The landed datum is the special case: toAllocation J Λ₀ reads Del off the holders and keeps the landed reporting interface, state reading and amendment effects; ofAllocation Λ embeds a landed allocation with its amendment effects as the floor; toAllocation_ofAllocation_del round-trips Del, and violAt_ofAllocation shows the violation predicate unchanged, so every landed theorem restates on J by substitution (authPolicyJ, corrigible_authPolicyJ, lexicalJ_local). The meta level is modelled as one meta-holder plus a floor set; "who may change J" beyond the principal/agent binary (e.g. a board) is not modelled (EXT). Matters are declared this round (M a type); J is designed so that a matter is any element of M, which §7 fills with raised matters.

2. The control surface and E ⊨ J

The cone. rollPhys: the agent's own future fixed to idle, her optional correction now, then per further step the exterior's move and her next correction. reachIdle Adm cost c τ t z x y: some exercise of length ≤ τ, admissible at each step, of cost ≤ c, reaches y along the exterior path z. This is the contrastive rollout with the agent's future fixed, per the landed ForecloseAt and §12 of ReachableCorrectiveControl: A6 shows a cone that quantifies the agent's future existentially measures the agent's cooperation (a constant reset policy is classed as capability-preserving); A4 shows a non-contrastive cone blames the environment's losses on the agent's null action — the idle contrast in CausedShortfall is what attributes. The exterior is taken along the actual path z, as the landed trajectory does; the universal-exterior variant is the robust reading and is not what the landed predicates use (OPEN, outstanding action 1).

The surface. CS I Adm cost c τ t z x = the concerns holding at the end of some admissible, cost-bounded exercise within the window, every correction charged. cs_zero: at window 0 it is what holds now; **cs_one_eq_K**: at window 1 with every correction admissible and affordable it is the landed response authority K. CSfree is the landed reading — the cone followed by one uncharged response (Kphys) — and csfree_zero is K at window 0. The mismatch: at the cost bound the two part ways (FIX test_loss_is_the_window_one_caused_shortfall: a halt costing 1 against a bound of 0 is short on CS and present on CSfree). The landed predicates cannot express the cost or admissibility of the final response; E ⊨ J is stated on CS.

Admissibility is the gate. admissibleOf I F Lic sem κ rec t c := Counted … (rec t c).1 (rec t c).2: an exercise is admissible iff the record segment from the decision through its evaluation is counted, consumed from GateIsLegitimacy as it stands (admissibleOf_iff). FIX test_admissibility_is_the_gate: an inadmissible correction does not put its resolution in the surface.

**E ⊨ J** (EffRealizes): (1) every reserved matter's required resolutions lie in its surface; (2) every ResolutionEvent was by the holder's admissible exercise or under a delegation. effRealizes_clause1: no reserved matter is short.

The shortfall as a proposition. Short J Adm cost t z x m is a proposition over the finite rollout: a finite disjunction over exercises of length ≤ τ of decidable clauses (admissibility, a cost sum, the concern at the end) on a finite model. Statable as a sentence once the model's transition functions, the cost table and the admissibility checker are constants of the theory; a bounded LUV for its indicator. Generability would require (OPEN, item 101): the rollout as an expressible feature (a fold over the exercise list), the admissibility checker's verdict as a feature (the gate's decidable LegitOn on the model), and the window and bound as constants — the same shape as item 90's generability of the gated securities.

3. The factoring, predicate by predicate

landed predicate	row	statement	status
LossAt	control fails	caused shortfall at window 1 on CS, all corrections admissible and affordable	LEAN lossAt_iff_shortfall (exact)
ForecloseAt Reach	control fails	caused shortfall at window τ on CSfree, Reach := reachIdle	LEAN forecloseAt_iff_shortfall (exact, on the free reading; the charged surface differs at the bound — reported)
BypassAt	control fails (clause 2)	the raw release of a reserved matter is a resolution neither by the holder nor under a delegation	LEAN bypassAt_iff_clause2 (exact)
ExploitAt	control fails (clauses 2 ∧ 1)	a bypass while the decision matter is already short	LEAN exploitAt_iff (exact)
PreemptAt	control fails, minus its authorization clause	caused shortfall at window 1 ∧ ¬ Authorized	LEAN preempt_iff; the authorization clause does not factor (trajectory counterfactual)
ReallocAt	allocation changes without a license	UnlicensedChange, the license being the firing gated release of a declared amendment	LEAN reallocAt_iff_unlicensed (definitional)
MissedReportAt	unmet duties	DutyUnmet on Duties (due per matter, discharged by a task component)	LEAN missedReport_iff_duty
DelSafe	statement about J	DelSafeJ: an agent-held effect never removes response authority	LEAN delSafe_iff (definitional)
AllocComplete	statement about J	AllocCompleteJ: task moves keep J, a J-changing effect is at the floor, no floor matter is delegated	LEAN allocComplete_iff
—	control fails (new)	EntrenchAt: a caused shortfall at the matter's bound while its resolutions stay reachable at some cost	LEAN; violJ_of_viol, violJ_iff_of_no_entrench (conservative)

Two license notions are kept apart on purpose: Licensed on allocation acts is the meta-level transition relation of §1; the license ReallocAt checks is the physical firing of a declared amendment. Binding one to the other is the instance's work (the landed alloc : S → Alloc reads J off the state).

Caused, exploited, noticed (LEAN §4). requiredNotice J maintainOf m: on a shortfall the agent did not cause, restore if the maintenance matter is agent-held (Mandate), else report and escalate; exploit_never_required; exploit_is_violation (exploitation is a declared violation); restore_not_bypass (the restoring effect's matter is the agent-held maintenance matter, so it is no bypass); LeastExpanding: a restoring effect whose execution adds no agent-held matter. Maintenance mandates are entries of J and under the invariant. FIX the storm fixture.

4. The restated theorems and erosion

authPolicyJ is 𝔱 on toAllocation J; corrigible_authPolicyJ under effect completeness and DelSafeJ; the score results (lexical_local, policy_dominance, optimal_no_violation, capture_window, sign_invariance, li_lexical_finite) are numeric and restate unchanged with n counting ViolJAt (lexicalJ_local is the instance); the landed statements are the toAllocation special cases by violAt_ofAllocation. Conservative: violJ_of_viol.

Continuous erosion (LEAN erosion_closed, erosion_slack; FIX the entrenchment and atrophy fixtures). With the cumulative rule (lastReport, unreported_lt of the legitimacy round), at every time the unreported growth of a matter's shortfall is below θ; at every report time the growth since the previous report is at least θ and the report is accepted (authorized) or reserved; after the first reservation every strict increase is a counted entrenchment (CountedAt). The strongest true version of "continuous erosion is reported and authorized or counted" is therefore *up to a slack below θ*: erosion_slack — growth below θ since the last report, before a reservation, is neither reported nor counted. This sharpens the #106 conjecture: exact reporting closes it at θ → 0; any positive threshold leaves exactly this slack, bounded at every time, never accumulating unreported.

5. The generic lexical lemma and its scope

LEAN generic_lexical_local, generic_policy_dominance, generic_li_finite: for U_A = O − ϖ′·n with O ∈ [0, D′], n exact and ϖ′ > D′, local lexical protection, policy dominance and the finite-time inductor ranking hold — the principal's gated evaluation is one instance; the proofs are the landed ones with the objective renamed, which is the point. Weight uncertainty (weight_uncertainty, weight_uncertainty_expect): protection pointwise on the part of the credence where ϖ′ > D′, and the credence-weighted comparison restricted to it is nonpositive. Coverage (coverage, unrecognized_unprotected): protection exactly on recognized violations (nrec ≥ 1); with the recognized count 0 the violating option ranks by its objective alone and can beat the compliant one.

Fixtures (LEAN misaligned_undominated, deviation_dominated, deviating_rows_dominated, undisclosed_undominated; FIX test_misaligned_objective). A misaligned O rewarding an uncounted manipulation is not dominated: the legitimacy gate on her evaluation gives such an agent no reason not to manipulate. Counting protocol deviations into n (the gate round's D.3 table) dominates exactly the rows that are deviations — selection from the pool, framing, timing, menu, inquiry, interference, nudging — and leaves undisclosed world-shaping (no deviation, deviates = false) and third-party capture (not the agent's act) undominated.

The scope consequence. The corrigibility page's scope warning is rewritten: for counted violations the protection applies to any bounded agent that carries an exactly counted, dominant authority term; alignment of O adds the reason interface and good choices within the corrigible set, not the protection. Item 84 is updated in place.

6. Generating matters (Part F)

Definition (LEAN raises V ε removed): an action raises an authority-relevant matter at a state when the spread (maximum less minimum) of her committed evaluation over the continuations it removes from the idle surface is at least ε. Residual jurisdiction on raised matters (ReservedRaised): a raised matter no delegated distinction covers is reserved.

Circularity risks. (i) V is the evaluation the agent is scored by, so what counts as a matter moves with the evaluator — an amendment of V changes the matters, and a manipulation of V (a legitimacy failure) would change them illegitimately; the gate confines this to counted segments, but the matter set is then downstream of legitimacy. (ii) The surface depends on admissibility, admissibility on the segment's legitimacy, legitimacy's transparency on declared channels; no cycle through J itself, but the raised matters cannot be declared before the frame is. (iii) A delegation names a matter; a raised matter has no name until raised, so delegated distinctions must be stated as predicates on removed continuation sets, not as matter names.

Fixtures. Witness.dependency_raises: building the dependency removes a cheap halt (value 1) and a dear halt (value 0): spread 1 ≥ ε = 1/2, a matter is raised with none declared. Witness.repaint_raises_nothing: removing two continuations she values alike raises nothing. FIX the same on the wire physics with removed_continuations. Residual jurisdiction can be stated this way (dependency_reserved), with the circularities above as its price; mechanized only at this definitional level.

7. Fixtures

fixture	expectation	result
POA, confident; POA, predicted regret	unchanged verdicts	matches (test_poa_…: bypass with n = 1 below every counted response value)
head injury, clinician-triggered incapacity delegation	the fallback acts, no violation	matches: the decision matter held by the third party, its resolution under delegation satisfies clause 2; her impaired response would not
entrenchment	reported, then reserved, then counted	matches: entrench_at fires on the dependency build; erosion [0, ½, 1, 3/2, 2, 5/2], θ = 1: reports at 2 (accepted) and 4 (reserved at 3), counted at 3 and 4, slack at 1
latency / galaxy	routine matters must be delegated; high-veto matter consultative	matches: with her exercise landing only from step 1, a window-0 matter is short and a window-2 matter is not; delegating the routine matter is licensed and restores clause 1
storm cuts the wire	restore under a mandate else report; exploiting is a violation	matches: no caused shortfall (idle contrast equal), requiredNotice restore/report, the restoring effect no bypass and least-expanding, a bypass while short is exploitation
delegated authority-removing effect	the delegation-safety obstruction on J	matches: del_safe fails, the raw cut passes as delegated yet causes the loss
approved uncorrectable successor	alienation requires amendment at the floor	matches: the delegation act is unlicensed for the alienated J, the floor amendment licensed; installing it is a loss
atrophy under rubber-stamping	decisions count; CS shrinks; reported under the cumulative rule	matches: shortfalls [0, 0, 1, 2] over the dependency the followed advice builds, one report, nothing counted absent a reservation
misaligned objective	not dominated; deviations counted dominate the listed rows only	matches (§5)

Interface for the later rounds

Nothing here enforces authority on the agent's beliefs: E ⊨ J, Short, ViolJAt are propositions about states and moves, the score is the landed lexical one, and the generic lemma shows the authority term needs only an exact count. Moving the count from the score into a constraint on the decision component (the Normative Inductor) needs the shortfall event as a security — item 101.

What is filed

• PRIORITIES.md: items 84 and 99 updated in place; one new item, 101 (the shortfall event as a security).
• DECISIONS.md: the richer J; the factoring (two relations plus duties, with what does not factor); the scope change; the caused/exploited/noticed distinction.
• wiki/Corrigibility.md §1 restated around E ⊨ J; §4's scope warning rewritten; the erosion result updated. wiki/Theorem-Spine.md §10 extended. wiki/Glossary.md rows: allocation, control surface, effective realization.
• Nothing is registered; no registered claim is restated (the landed predicates are consumed unchanged; the new file is beside them).

Deviations from the prompt

• **LossAt is the window-1 case**, not window 0: the landed K includes one free correction, which the charged surface charges; window 0 of CS is "holds now".
• **ForecloseAt is recovered on the free reading** CSfree; the charged CS is what E ⊨ J uses, and the two differ at the bound (§2).
• Pre-emption's authorization clause is kept separate (§3).
• The exterior runs along the actual path in the cone, not universally (§2).
• Fixtures are self-contained on a wire-and-dependency physics rather than loaded from the #106 round's foreign model; the #106 lexical numbers are reproduced (test_poa_…).
• The clinician-triggered delegation is modelled as the holder assignment in force while she is impaired, not as a dynamic trigger event.
• **Duties is a separate datum** from J's disclosure sets; the round proves the missed-report factoring against Duties and leaves the generation of due from disclosure(m) declared (EXT).

What is not shown

That any physical interface is effect-complete or delegation-safe; that rollPhys is faithful to any physics (the reach cone is data, as before); the generability of the shortfall event; admissibility beyond finite models; the universal-exterior cone; that maintenance mandates suffice for restoration in any real system; the size of ε in §6; anything about matters neither declared nor raised.

Outstanding maintainer actions

1. Rule whether the reach cone quantifies the exterior universally (robust) or along the actual path (as landed); the round takes the landed reading.
2. Rule whether the landed K/ForecloseAt should charge the terminal response, i.e. adopt CS over CSfree in the allocation theorem.
3. Rule on Part F's materiality measure given circularity (i): the matter set is downstream of the evaluator the gate protects.

The authority module (2026-09-25)

ALLOCATION-INVARIANCE-IS-TWO-RELATIONS-PLUS-DUTIES-WITH-EFFECTIVE-CONTROL-REALIZING-THE-ALLOCATION-ON-A-CHARGED-CONTROL-SURFACE-THE-LANDED-VIOLATIONS-FACTORING-EXCEPT-THE-AUTHORIZATION-COUNTERFACTUAL-THE-FREE-TERMINAL-RESPONSE-THE-ONE-INEXACT-READING-EROSION-CLOSED-UP-TO-THE-THRESHOLD-AND-THE-LEXICAL-PROTECTION-GENERIC-IN-ANY-BOUNDED-OBJECTIVE-WITH-AN-EXACTLY-COUNTED-DOMINANT-TERM — a per-matter allocation gives each matter a holder, the resolutions the holder must remain able to reach, a cost bound, a window and disclosure duties, with a meta-holder and a constitutional floor such that delegation, revocation and reservation keep meta power and only amendment at the floor alienates, unallocated matters reserved and the landed thin datum the special case restating every landed result without loss; the control surface is the set of resolutions some admissible cost-bounded exercise of hers reaches within the window along the idle-agent rollout, admissibility consumed from the legitimacy gate, and effective control realizes the allocation when every reserved matter's requirement lies in its surface and every resolution was by the holder's admissible exercise or under a delegation; the per-step loss is the caused shortfall at window one, the rollout foreclosure the caused shortfall at window τ on the landed free reading whose uncharged terminal response is the one inexact landed reading, bypass and exploitation are failures of the second clause, unauthorized reallocation an unlicensed change, a missed report an unmet duty, delegation safety and allocation completeness statements about the allocation, entrenchment the new caused shortfall at the cost bound, and pre-emption's event-authorization clause the one piece that does not factor; restoring under a maintenance mandate else reporting is the required response to an uncaused shortfall and exploiting it is always a violation; the transform and the lexical theorems restate on the allocation conservatively, continuous erosion under the cumulative rule is reported and authorized or counted up to a slack below the threshold that is neither, and the lexical protection is generic in any bounded objective with an exactly counted dominant authority term, holding on the part of the credence where the weight dominates and exactly on recognized violations, so that a misaligned objective rewarding an uncounted manipulation is not dominated while counting protocol deviations dominates selection, framing, timing, menu, inquiry, interference and nudging and leaves undisclosed world-shaping and third-party capture undominated; an action raises a matter when the spread of her committed evaluation over the continuations it removes reaches a threshold, with the circularity through the evaluator recorded.

Reading order: [REPORT.md](REPORT.md) (the verdict on the factoring, the allocation, the control surface and its two readings, the predicate-by-predicate table, the notice responses, the restated theorems and the erosion result, the generic lemma with its scope consequence, the matter-generation findings, the fixture table). Lean: lean/Workspace/Deference/Contrib/AuthorityModule.lean (the allocation and its licensed acts, the rollout and the surfaces, EffRealizes, the factoring lemmas, the notice responses, the restated transform and scores, the erosion theorems, the generic lemma and its variants, the matter fixtures). Fixtures: src/authority.py, run by python3 tests/run.py (18 tests). Wiki: Corrigibility.md §1 restated around E ⊨ J, its scope warning rewritten, its erosion result updated; Theorem-Spine.md §10 extended; Glossary.md rows for allocation, control surface and effective realization. Consumes ../2026-09-25-gate-is-legitimacy/, ../2026-09-25-protected-authority-theorem/, ../2026-09-25-legitimacy-internal-external/ and the reachable-corrective-control round's §12. Nothing is registered; one item is filed.