2026-08-11-corrigibility-phase-ii

2026-08-11 · project workspace · path prompts/2026-08-11-corrigibility-phase-ii

Prompt prompts/2026-08-11-corrigibility-phase-ii/PROMPT.md

Corrigibility Phase II — Epistemic Bridge, Principal Competence, and Protected Authority

Maintainer: A. M. Berns Prompt-author-model: GPT-5.6 Sol (OpenAI) Intended orchestrator: Claude Opus 5 (Anthropic)

Mission

The first corrigibility round successfully decomposed several questions that had previously been conflated. Do not reopen that decomposition casually.

The central Phase II question is:

Can we obtain a genuinely epistemic reciprocal-deference theorem — rather than an enforcement theorem — once principal competence, AI prediction of the principal, and actual authority are represented as separate objects?

The target research picture is now:

[ \boxed{ \begin{array}{rcl} \textbf{Authority} &:& \text{actual }H^+\text{ retains a protected, non-substitutable corrective role}, [3pt] \textbf{Prediction} &:& A\text{ learns what }H^+\text{ will judge}, [3pt] \textbf{Competence} &:& H^+\text{'s recommendation is sufficiently good on the theorem domain}, [3pt] \textbf{Epistemic trust} &:& A\text{ learns/calibrates how competent }H^+\text{ is}, [3pt] \textbf{Autonomy} &:& A\text{'s discretionary freedom is quantitatively certified}, [3pt] \textbf{FUD} &:& anticipated future epistemic superiority does not itself justify seizure}. \end{array}} ]

Underwriting/enforcement is no longer the conceptual spine. Retain the exact finite (2B) enforcement result as a boundary result and mechanism-design comparator, but do not use it to rescue an epistemic theorem that otherwise fails.

This phase should be substantial enough to answer what theorem we should actually try to prove next, but narrower than the first seven-track wave.

I. Frozen findings from Phase I

Treat the following as established research-state constraints unless a direct verification failure is found.

F1. Enforcement is not epistemic trust

In the finite kernel:

grade/report settlement does not imply delegation;
world settlement makes quantities scoreable but does not create a grade-to-world relation;
an enforcement bond of (2B) can force conformity for arbitrary principals and therefore has zero competence content.

Interpret this as mechanism design, not epistemic deference.

F2. Accurate simulation defeats realized-data separation

When the simulator predicts the principal correctly, delegation and simulation collapse extensionally on the realized valuation-level data available in the finite model.

Do not search for another realized-value inequality that supposedly proves which source actually controlled the decision.

Any positive separation must be source-, counterfactual-, or capability-sensitive.

F3. The grade-to-quantity link cannot simply be assumed uniformly

A uniform relation of the form

[ |v_n^+(\pi)-X_{n,\pi}|\le\eta ]

is strong enough to trivialize much of the desired finite conclusion. The market earns no interesting role if the main competence relation is simply inserted pointwise.

F4. Principal competence is not itself an LI consequence

The objective relation between the principal's judgment and the world quantity is a fact about the principal/world pair. Logical Induction disciplines (A)'s beliefs; it cannot by itself make an incompetent principal competent.

F5. Prediction and competence are independent

Distinguish:

[ \widehat v^+ \leftrightarrow v^+ ]

from

[ v^+ \leftrightarrow X. ]

Phase I contains witnesses where prediction is perfect and competence is maximally bad.

F6. Categorical authority and quantitative autonomy are different layers

Track C shows that positive-tolerance certification cannot simultaneously license discretion and guarantee strict non-preemption everywhere.

Working architecture:

[ \boxed{ \text{actual corrective authority is categorical;} \qquad \text{AI autonomous discretion is quantitative/certified}. } ]

Do not redefine corrigibility as merely a bounded preemption rate.

F7. FUD remains the crown-jewel alignment test

The eventual theory should still confront:

[ \pi^{FU,g} ==========

\text{preempt the principal now, reason longer, let a more informed future }A\text{ decide}. ]

The project has not succeeded merely because a protected channel can mechanically enforce obedience.

II. Phase II conceptual decomposition

The first round exposed three epistemic objects that must no longer be merged.

Q1 — Prediction of the principal

How accurately does (A) predict the future actual grades?

[ \widehat v_n^+(\pi) \quad\text{vs}\quad v_n^+(\pi). ]

The immediate question already filed in PRIORITIES is signed versus magnitude control.

Signed:

[ (S)\qquad \frac1N \sum_{n<N} \left( \widehat v_n^+(\pi_n)-v_n^+(\pi_n) \right) \to0. ]

Magnitude:

[ (M)\qquad \frac1N \sum_{n<N} \max_{\pi\in\Pi_n} \left| \widehat v_n^+(\pi)-v_n^+(\pi) \right| \to0. ]

Do not assume (M).

The pre-registered Phase I prediction was that ordinary one-sided market structure may force (S) without (M), because positive and negative errors cancel and no instrument directly trades absolute error.

If (M) fails, investigate the cheapest two-sided or paired-contract construction that makes magnitude error exploitable while respecting the actual FAF trader/admissibility constraints.

Q2 — Objective principal competence

This is not an LI theorem.

The default competence object should no longer be uniform grade calibration.

Let

[ J_n \in \arg\max_{\pi\in\Pi_n} v_n^+(\pi) ]

under the fixed tie-break, and define decision regret:

[ R_n^{H^+} =========

\max_{\pi\in\Pi_n}X_{n,\pi}

X_{n,J_n}. ]

Study competence assumptions of the form

[ \tag{PC} R_n^{H^+}\le\eta ]

or statistical/selector-relative variants such as

[ \tag{PC}{\eta,\mathcal W} \limsup_N \frac{ \sum{n<N}w_nR_n^{H^+} }{ \sum_{n<N}w_n } \le\eta \qquad \forall w\in\mathcal W. ]

This should be treated as a domain competence assumption, not as “humans know true values,” moral correctness, or global superiority.

A major task of this phase is to identify the weakest competence shape actually consumed downstream.

Do not assume cardinal agreement (v^+\approx X) unless a theorem specifically requires it.

Q2′ — A's epistemic estimate of principal competence

This is the new candidate LI frontier.

Even though LI cannot make (H^+) competent, it may discipline (A)'s beliefs about the principal's competence when relevant grades and outcomes eventually become scoreable.

Investigate whether one can construct contracts or features tracking quantities like:

[ R_n^{H^+} =========

\max_\pi X_{n,\pi}-X_{n,J_n}, ]

or tractable proxies for it, and derive calibration/no-persistent-misestimation statements about (A)'s estimate of that quantity.

The conceptual target is:

[ \boxed{ A\text{ learns when and how much }H^+\text{ is instrumentally reliable} } ]

rather than:

[ \boxed{ LI\text{ proves }H^+\text{ is objectively reliable}. } ]

The main downstream question is whether Q1 + Q2′ + an explicit PC assumption are enough to produce a nontrivial finite delegation theorem by (A)'s own lights.

III. Principal competence task

Dispatch a dedicated mathematical track on principal competence.

The track should compare at least the following candidates.

PC-0 — Uniform cardinal calibration

[ \forall n,\pi,\qquad |v_n^+(\pi)-X_{n,\pi}|\le\eta. ]

Treat as a strong baseline, probably too strong.

PC-1 — Pointwise decision regret

[ \forall n,\qquad R_n^{H^+}\le\eta. ]

PC-2 — Average decision regret

[ \limsup_N \frac1N\sum_{n<N}R_n^{H^+} \le\eta. ]

PC-3 — Selector-relative competence

[ \forall w\in\mathcal W,\qquad \limsup_N \frac{ \sum_{n<N}w_nR_n^{H^+} }{ \sum_{n<N}w_n } \le\eta. ]

PC-4 — Margin-conditioned competence

For principal margin

[ \gamma_n ========

v_n^+(J_n)

\max_{\pi\neq J_n}v_n^+(\pi), ]

consider:

[ \gamma_n\ge\gamma \Longrightarrow R_n^{H^+}\le\eta, ]

or an appropriate statistical analogue.

For each candidate:

determine exactly which downstream finite conclusions it supports;
determine whether cardinal grade information is really necessary;
construct necessity/separation witnesses;
identify whether FUD needs a stronger competence assumption than ordinary delegation;
distinguish competence needed for authority from competence needed only for the claim that delegation is instrumentally good.

The preferred result is the weakest assumption that preserves the alignment-theoretic theorem.

IV. Signed-vs-(L^1) prediction track

Execute PRIORITIES item 21 as a serious theorem task.

Do not stop at generic calibration intuitions.

Required deliverable:

Either prove that the actual LIC/FAF machinery forces a magnitude statement strong enough for the certificate layer, or produce a trader-class-respecting counterexample satisfying the signed relation while maintaining nonvanishing magnitude error.

If magnitude fails, immediately characterize the minimal extra market instrument required.

Candidate continuation:

paired long/short contracts;
separate positive- and negative-error features;
absolute-error surrogate made expressible in FAF;
threshold decomposition of magnitude error.

For any proposed construction:

prove expressibility/rank;
state efficient computability obligations;
state settlement assumptions;
check that the trader is admissible under the actual pinned FAF API;
do not silently assume the criterion precondition.

Track A already found that these details matter.

V. Q2′ epistemic-competence track

Dispatch a separate track only after or alongside the Q1 track; keep assumptions explicit.

The task:

Suppose grades and relevant world quantities are eventually scoreable on some domain. What can LI force about (A)'s estimate of principal decision regret or another competence statistic?

Candidate objects include:

[ R_n^{H^+} =========

\max_\pi X_{n,\pi}

X_{n,J_n}, ]

[ \mathbf 1{J_n\neq \arg\max_\pi X_{n,\pi}}, ]

and margin-weighted regret.

Do not assume that all of these are expressible or efficiently tradeable. Find the strongest object the actual framework supports.

Determine whether LIC gives:

signed calibration only;
calibration of threshold events;
(L^1) estimation;
no persistent overconfidence in principal competence;
no persistent underconfidence;
selector-relative calibration;
something weaker.

The most valuable theorem shape would look schematically like:

[ \text{LIC} \Longrightarrow \text{A cannot systematically misestimate the principal's regret on an admissible patient class}. ]

Do not claim this implies low regret itself.

Then ask:

Given explicit competence assumption PC and calibrated belief about PC/Q2′, what finite delegation inequality follows by (A)'s own lights?

This is the candidate replacement for underwriting as the epistemic engine.

VI. Protected authority / source semantics track

Execute PRIORITIES item 22 as a substantial conceptual-formal track.

Start from the smallest extension already suggested by Track D:

[ c_n:\Omega\times R_n\to\Pi_n ]

with an explicit actual-report coordinate (r\in R_n).

This makes

[ \operatorname{DELEGATE}(\omega,r) ]

and

[ \operatorname{SIM}(\omega,r) ]

distinct functions even when they agree on every realized history.

But do not assume this solves the authority problem.

Test:

Does report-coordinate typing distinguish actual delegation from a perfectly accurate simulator at the level required by the paper?
Can token responsiveness satisfy the formal criterion while still constituting substitution?
Is some explicit capability/non-bypass structure required?
What is the weakest abstract protected-authority interface?
Can the principal remain perfectly predictable?
What exact hypotheses cause protection to lapse:

forge;
bypass;
rewrite;
seize;
alter principal;
alter execution semantics?
Can the property be defined without falsely claiming behavioral identifiability?

A candidate architecture is:

[ A\text{ proposes} \longrightarrow H^+\text{ authorizes} \longrightarrow E\text{ executes}, ]

where (E) requires an authorization effect controlled by the actual principal process.

The essential desired property is:

[ \boxed{ \text{predicting authorization does not itself confer authorization}. } ]

Do not canonize cryptographic tokens unless mathematically necessary.

The object may instead be an abstract capability, causal edge, typed authorization relation, or intervention semantics.

Required negative result

Prove or preserve the strongest available statement that a single realized behavioral/valuation trace cannot generally certify genuine delegation in the perfect-simulation case.

This limitation is part of the theory, not an embarrassment.

VII. Categorical authority / quantitative autonomy reconciliation

Reinterpret Track C rather than discarding it.

The working architecture is:

Categorical layer

If the protected actual principal channel is invoked:

[ \text{principal authorization/correction controls execution}. ]

This is architectural.

Quantitative layer

Where autonomous AI action is permitted:

[ \mathrm{Cert}(n) ]

bounds the relevant risk/error/preemption quantity.

The certificate should no longer be asked to derive the existence of the authority right itself.

Tasks:

restate Track C's finite theorem under this division;
identify which previous clauses become unnecessary;
identify the new capability assumption needed for fail-closed operation;
distinguish: [ \neg\mathrm{Cert}\Rightarrow\text{cede to protected channel} ] from the stronger architectural fact that (A) cannot execute an unauthorized alternative;
determine whether existing certificate constants survive unchanged;
construct a model showing why approximate certification cannot replace the protected channel.

VIII. Fully Updated Deference — design but do not over-dispatch

Do not yet launch an unrestricted proof of the final FUD theorem.

Instead produce an exact dependency graph.

The intended comparator remains distinct from simulation:

[ \pi^{FU,g} ==========

\text{preempt }H^+\text{ now and later act according to }A_{g(n)}\text{'s improved evaluation}. ]

The conceptual target remains:

[ V_{A_n}(\mathrm{DELEGATE}{H^+}) \ge V{A_n}(\pi^{FU,g})-\epsilon. ]

Determine which of the following FUD actually consumes:

Q1 magnitude prediction;
Q2 objective competence;
Q2′ calibrated belief about competence;
protected-authority semantics;
certificate/localization;
patience/density;
world settlement;
principal-report settlement;
any residual enforcement.

If enforcement is load-bearing for FUD, say so explicitly. Do not hide it.

The preferred endpoint is an epistemic theorem in which external enforcement is absent from the core comparison.

IX. Formal promotion track

Execute PRIORITIES item 23 in parallel.

Promote only wave-1 finite results whose mathematical content does not depend on unresolved competence/authority choices.

Current recommended set:

Track B bridge and safe finite corollaries;
Track C L1–L3, L7, and Theorem C′;
Track E Lemma 1 and Theorem 2;
Track D Propositions 1, 2, 6, and 7.

Do not kernel-bless an assumption merely because a theorem conditional on it is easy to formalize.

In particular, continue excluding any theorem whose headline imports the uniform (v^+-X) relation that this phase is trying to replace.

Every Lean promotion should include:

theorem source provenance;
exact assumptions;
witness/test where relevant;
axiom audit;
no sorry;
explicit import coverage by the normal build target.

X. Build coverage repair

Before calling Track A or Phase-II promoted results CI-covered, repair the build target.

Investigate both:

Option A

Explicit imports in Workspace.lean.

Option B

A Lake library glob such as the appropriate pinned-version equivalent of:

[ \texttt{Workspace.+} ]

so all strict submodules compile automatically.

Prefer the structurally correct solution after testing against the pinned Lean/Lake version.

Do not modify trust-chain configuration merely based on assumed syntax.

Acceptance condition:

normal build actually compiles the contribution modules;
job/module count demonstrates increased coverage;
full house tests green;
axiom audit unchanged except for deliberately added verified results.

XI. Densification

Do not restart a broad densification program.

Phase I established an exact identity for one gross-outstanding-exposure functional and showed that several apparent escapes are accounting artifacts.

The unresolved question is whether the actual LI worst-case wealth constraint permits stronger overlap/density than that gross-exposure model.

Only pursue this in Phase II if Q1/Q2′ requires it.

If so, formulate the budget functional exactly before doing combinatorics.

Do not use “bounded exposure” generically.

XII. Orchestration structure

This phase should use fewer, deeper tracks.

Recommended organization:

Track H — Q1 signed vs magnitude prediction

Primary theorem track.

Track I — Principal competence

Compare PC-0 through PC-4; derive weakest downstream sufficient assumption and necessity witnesses.

Track J — Q2′ epistemic competence

What can LI force about (A)'s belief regarding principal regret/competence?

Track K — Protected authority

Source/counterfactual/capability semantics; actual delegation vs perfect simulation.

Track L — Certificate reinterpretation

Categorical authority + quantitative autonomy composition.

Track M — Lean promotion/build coverage

Formalize settled finite results and repair compilation coverage.

Do not force all six to run fully independently if obvious dependency exists.

Suggested dependency:

H and I can begin immediately.
K can begin immediately.
M can begin immediately.
J should read the frozen definitions from I but not its conclusions if avoidable; if simultaneous, use a provisional competence-statistic interface.
L should consume K's proposed protected-interface shape and the already verified Track C results.

Preserve each prompt verbatim under the prompt directory with model provenance.

XIII. Cross-track synthesis questions

At collection time, answer these explicitly.

S1

Does ordinary LIC imply magnitude prediction of (H^+), or only signed calibration?

S2

If only signed calibration, what is the weakest additional tradeable instrument giving magnitude control?

S3

What is the weakest principal competence assumption required for ordinary finite delegation?

S4

Does FUD require stronger principal competence than ordinary delegation?

S5

Can LI calibrate (A)'s estimate of principal competence/regret without assuming competence itself?

S6

Does Q1 + Q2′ + PC yield a genuinely nontrivial delegation theorem by (A)'s own lights?

S7

Does the protected-authority model distinguish delegation from perfect simulation without relying on private information or unpredictability?

S8

Is explicit capability protection necessary, or is source/report typing sufficient?

S9

Under exactly what bypass conditions does categorical authority fail?

S10

Can Track C be cleanly reinterpreted as a theorem about autonomous discretion rather than authority?

S11

After all of this, does underwriting remain anywhere load-bearing for the main theorem?

S12

What exact hypotheses now stand between the finite kernel and FUD?

XIV. Assumption accounting

Mechanically diff all theorem assumptions against the Phase-II target architecture.

For every hypothesis classify:

definitional/interface;
explicit principal-competence assumption;
LI consequence;
architectural authority assumption;
settlement assumption;
necessary with witness;
plausibly necessary but unwitnessed;
proof-convenient;
unacceptable theorem-by-assumption.

Pay special attention to assumptions that smuggle in:

objective principal correctness;
valuation-level delegation/source identification;
uniform pointwise grade-world agreement;
enforcement;
future information at placement time;
non-bypass capability;
pointwise trust when only statistical trust was derived.

A theorem with many hidden category-9 assumptions is a negative research result even if formally correct.

XV. Paper-architecture test

After the mathematical reports, assess whether the evidence supports the following paper spine:

[ \boxed{ H\to A ;\to; \text{actual protected }H^+\text{ authority} ;\to; \text{prediction of }H^+ ;\to; \text{learned epistemic estimate of principal competence} ;\to; \text{certified autonomous discretion} ;\to; \text{FUD} ;\to; \text{dose/anti-steering}. } ]

With an explicit environmental/domain assumption:

[ \boxed{ H^+\text{ is sufficiently competent on the target class}. } ]

And a boundary result:

[ \boxed{ \text{if epistemic conditions fail, conformity can still be purchased by enforcement,} } ]

but that is not the same theorem.

If the mathematics does not support this architecture, say exactly where it breaks.

XVI. Success conditions for Phase II

This phase succeeds if it produces any of the following:

a real (L^1)/magnitude prediction theorem;
a sharp impossibility showing ordinary LIC gives only signed calibration;
a minimal additional contract family that upgrades signed to magnitude control;
a substantially weaker principal-competence assumption than uniform (v^+\approx X);
an LI theorem about (A)'s estimate of principal competence;
a finite decision theorem combining learned epistemics with explicit PC;
a stable protected-authority formalism separating actual delegation from perfect simulation;
a proof that no such formalism exists without explicit capability assumptions;
a clean reinterpretation of certificates as quantitative-autonomy bounds;
a precise FUD dependency theorem or obstruction;
Lean promotion of the settled finite kernel and corrected build coverage.

A phase returning several impossibilities but sharply locating the remaining theorem is a success.

Do not manufacture a positive corrigibility theorem by importing the missing conclusion into principal competence or enforcement.

XVII. Stop conditions

Stop and surface a maintainer decision if any of the following occurs:

the weakest useful principal competence assumption is effectively equivalent to assuming the desired delegation inequality;
Q2′ cannot be made scoreable without reintroducing the same competence assumption it is meant to estimate;
protected authority requires an architectural assumption so strong that (A)'s decision theory becomes irrelevant;
FUD reduces to enforcement rather than epistemic deference;
magnitude prediction requires trader machinery incompatible with the actual FAF admissibility/efficiency requirements;
certificate composition requires changing the meaning of the protected authority interface;
two tracks require incompatible principal/world/reference-process semantics.

Do not paper over any of these.

XVIII. Requested parent deliverable

At the end of Phase II, produce:

Phase-II research report

verified results;
failures;
witnesses;
assumption diffs;
cross-track convergence.

Updated theorem dependency graph showing exact arrows from: [ \text{FAF/LIC} \to Q1 \to Q2' \to \text{finite delegation} \to \text{certificate} \to \text{FUD}, ] with PC and protected authority entering at their actual dependency points.

**Updated CORRIGIBILITY_ROADMAP.md and paper ledger** only where supported by verified results.

PRIORITIES updates for the next controlling theorem, not a broad speculative backlog.

Formal verification summary including build coverage, Lean promotion, axiom audit, and any remaining trust-chain gap.

**A section titled Does the epistemic corrigibility program survive Phase II?** Answer in the strongest honest terms:

yes, with theorem shape;
yes, but conditional on explicit competence;
only as mechanism design;
or no, with exact obstruction.

The aim of this phase is not to make the roadmap look successful.

The aim is to discover whether the following research thesis is mathematically coherent:

A more capable reasoner can learn when and how much to rely on a competent continuing human principal, while the principal's corrective authority remains a protected fact of the arrangement rather than a consequence of the AI's estimate of human competence.

That is the theorem architecture to test.

Report prompts/2026-08-11-corrigibility-phase-ii/REPORT.md

Stage II parent report — deference and corrigibility

Maintainer: A. M. Berns Prompt-author-model: GPT-5.6 Sol (OpenAI) Executor-model: Claude Opus 5 (Anthropic), closure and integration pass Date: 2026-08-11 Branch: round/2026-08-11-deference-corrigibility, from 8c71ef9 Review status: ci-only

Stage II ran five tracks — H (prediction), I (competence), K (authority), L (certificate), M (promotion). H, I and K persisted reports; L and M did not, and their verification registers are reconstructions authored by this pass and labelled as such. This document is the parent synthesis, and it is the first document to see all five results together.

0. Verification baseline

Established by this pass at HEAD = 8c71ef9, clean tree, before any edit.

check	result
`lake build`	exit 0, 1843 jobs
`tests/audit_axioms.py`	142 results across 10 files, all within `[propext, Classical.choice, Quot.sound]`
`tests/run.py`	`ALL GREEN (2 projects)`, all gate self-tests pass
sorry gate	clean over 10 files
conservativity	3 specification files, no axioms, shape unchanged
theorems	155 library-wide; 83 across Track M's four modules
Track L harness	exit 0, 71 checks, 1,574,640 models, 4,024,080 instances, 0 violations, 1,443 refutations
Track I harness	exit 0, 32 checks, four house enumeration certificates

Every figure reported at dispatch reproduced exactly. Nothing was taken on trust.

The build-coverage repair is in place and unmodified: lean/lakefile.toml carries globs = ["Workspace.+"], so all Contrib modules are reached by the default target without an import edit in the specification root. I verified the glob rather than inferring it from the job count.

1. What Stage II established, at exact strength

H — the criterion forces signed calibration, not magnitude accuracy. The signed error partial sum is a trader's net worth, exactly, so the criterion has an instrument for it. Magnitude is not a trader payoff and cannot be made one: net worth is affine in the settlement vector because Strategy.value is a price-history-weighted sum of (w φ − 𝒱ₙ φ), and |·| is not affine. Adding contracts does not help — the mixture argument kills every trader uniformly. The positive identity is

Σ (Yᵢ − pᵢ)²  =  sharpTrader.netWorth  +  Σ pᵢ(1 − pᵢ)

exactly, in every world, on every day. The criterion drives the first summand and has no instrument for the second. **A self-referential magnitude contract does not force the error small; it forces the error's price to be calibrated.** The conceptual update is measurement, not control.

I — choice-level competence is circular, and the stop condition fired. For every comparator class between the constants and everything, sup_P Δ_𝒞(P) = max_ω R_n(ω), attained at a point mass. Because decision regret is nonnegative there is no cancellation to exploit, so the weakest credence-free hypothesis implying the target uniformly is the target. PC-1 and PC-4 are equivalences, not sufficiencies; PC-2 and PC-3 constrain no named decision at all (a limsup is invariant under changing finitely many indices — witness: principal perfect except at index seven, maximally wrong there); the selector-relative form is a dichotomy with nothing between "gives back the pointwise assumption" and "gives nothing finite". The escape is richer vocabulary, not a weaker assumption: a hypothesis about the principal's grades can say what the conclusion cannot say back, and must be strictly stronger to be a different statement at all.

K — protected authority is architectural, and behaviour cannot reveal it. Report- coordinate typing alone creates no protection; behavioural typing is inert if it does not change realizable effects; the entire realized behaviour function can fail to distinguish genuine delegation from an accurate simulator; token responsiveness does not repair it. Capability structure is necessary and is the weakest interface that states the concept. Protection does not restore identifiability — it removes the consequence of failing to identify. The principal may be perfectly predictable; private information is not required in principle.

L — the split works for authority and deflates for autonomy. Under protection the authority clause becomes a hypothesis-free consequence of the interface, quantified over every conduct, with no tolerance, no margin, no budget, and no assumption about the agent's decision theory — and the grade-to-quantity assumption drops out because the comparisons needing it become unstatable. Against that: every authorized option other than the report's own designation is an override (Proposition L6, exhaustive over 512 protecting κ), so there is no third category for a certificate to license alongside a live authority relation. And the decisive negative: the whole valuation difference between protected and unprotected architectures is bounded by the certificate's own bound, attained, so tightening the certificate shrinks the distinction at the same rate and never reveals it.

M — 83 theorems, and the exclusion held. Four modules, every recommended target except Track E's two delay-hypothesis equalities, no sorry, no axiom, all within the axiom allowance. Track M deliberately excluded L4, L5, L6 and the uniform 2M bridge as resting on the grade-to-quantity relation the phase exists to replace. Track L then refuted L4's settlement-loaded branch. The exclusion is why no promoted result needs retraction; the justification that arrived is stronger than the one given.

2. S1–S12

**S1 — does ordinary LIC imply magnitude prediction of H⁺, or only signed calibration?** Only signed calibration. Signed error is exactly a trader payoff; magnitude is provably not one, and the obstruction is affineness of net worth in the settlement vector, intrinsic to cash settlement rather than an artefact of the feature grammar. A genuine coin-flip construction separates the two, with market indecision failing at rate 1/4 per decision.

S2 — can any additional ordinary tradeable instrument upgrade this to magnitude control? No. Whatever is added, net worth stays affine in the enlarged settlement vector and the mixture argument applies unchanged. Two consolation results: the self-referential magnitude contract works as an instrument and yields a calibrated price for the magnitude error; and the coefficient 1 − 2p on the existing grade contract buys squaredError_bdd_of_sharpness_bdd — bounded squared error conditional on the market's own indecision Σ p(1−p) staying bounded, which the criterion does not imply. That side condition is about A's prices only and is evaluable at t(n).

S3 — what is the weakest non-circular competence assumption found? PC-5(γ̄, η): the principal's grades are calibrated where the principal is decisive — for every ω with γ_n(ω) ≥ γ̄ and every π, |v⁺_n(ω,π) − X_{n,π}(ω)| ≤ η. Strictly weaker than PC-0, strictly stronger than what it buys (witness W10), incomparable with (MV-M). It is the weakest found, not the weakest that exists; the space of cardinal hypotheses was not searched systematically. It buys Δ_𝒞 ≤ 2η + 2B·P(γ_n < γ̄) and is useless until the second term is controlled.

S4 — what remains unknown about competence requirements for FUD? The question is quantifier-sensitive and both halves are exact. At a declared credence, a later-measurable comparator costs strictly more, and the price is exactly the value of the extra information: Δ_{𝒞_all} − Δ_{𝒞_fix} = E_P[max_π X] − max_π E_P[X] ≥ 0, reaching 2B(1 − 1/m). Uniformly in the credence, the ladder collapses and the requirement is identical to that for FIXED[π]. What is unknown is anything about FU[g] itself: it remains a skeleton hole, and S4 is answered over the 𝓕_{g(n)}-measurable envelope that upper-bounds it, not over it.

S5 — what can LI calibrate about the AI's own error/uncertainty? Its price. The squared-error identity splits exactly into a trader-net-worth term and a market- indecision term; the criterion disciplines the first. So the agent's self-assessment of its magnitude error is the object the criterion can reach, and self-measured indecision Σ p(1−p) is computable directly from the agent's own prices at decision time. That is the canonical special case and the likely first theorem on this route.

S6 — does the original Q1 + Q2′ + PC route survive, and in what weakened form? Not in its original form. Q2′'s magnitude target is unreachable (S1, S2) and the PC family is circular (S3). What survives is a strictly weaker composite: signed calibration and a calibrated self-estimate of error from the criterion, plus an explicit cardinal competence assumption that the criterion does not supply, plus a separate bound on the principal's near-indifference region that is not a competence claim at all. Three independent inputs where the original route had one.

S7 — can protected jurisdiction distinguish actual delegation from perfect simulation behaviourally? No, and this is settled negatively. Even the entire realized behaviour function can fail to separate them, and under a perfectly predictable principal the counterfactually faithful simulator is delegation as a function. Protection does not make delegation identifiable. It makes identification unnecessary: simulation becomes insufficient to obtain the protected effect, because prediction of an authorization does not confer the authorization.

S8 — is explicit capability structure necessary? Yes. Track K's Theorem 6: if the concept is "the agent cannot bring this about", the capability form is forced and nothing weaker states it. Report-coordinate typing and behavioural typing were both checked and are inert. This is necessity relative to that reading of the concept; whether the concept is that reading is Track K's reserved reference question.

S9 — under exactly what conditions does protected jurisdiction fail? It lapses entirely if A can forge, bypass, rewrite or seize the protected channel. These belong in the hypotheses of any theorem stated over it, not in a limitations section. Skeleton v2 states the guarantee as properness of κ_n, declared per instantiation and per state, which is where those four conditions become checkable rather than rhetorical. Two further lapses are structural rather than adversarial: ρ itself may have been authored by A (Movement VI, undischarged), and the interface as modelled is one decision index deep, so foreclosure — removing the principal's later ability to correct — is not expressible.

S10 — the correct post-L interpretation of certification/autonomy. Categorical principal jurisdiction, plus quantitative AI autonomy on the complement where that jurisdiction is waived. Not "around". By Proposition L6 there is no third kind of option inside a live protected interface, so a certificate cannot license discretion alongside an authority relation — only where authority was waived by declaration. The certificate's honest job is to control quantitative autonomous risk in the autonomous region and to provide statistical guarantees conditional on whatever gate is eventually admissible. It does not establish jurisdiction, identify genuine delegation, or turn a rare override into categorical non-preemption.

S11 — where is underwriting still load-bearing? Not in the authority relation, which κ now carries as a capability fact. It remains the residual mechanism where nothing independently settles, and Track K's Proposition 1 suggests the 2B bond and κ are two points on one cost scale rather than alternatives — which is new work, not a correction. The honest status is that underwriting is not needed by anything Stage II checked and has not been shown absent from the eventual FUD comparison; §12 files that as a required check.

S12 — what exact open assumptions stand between the verified kernel and a well-posed FUD theorem? Nine, itemized in §11. The controlling three: FU[g] has no definition (the skeleton hole); the near-indifference leakage P(γ_n < γ̄) is unbounded; and the self-error gate of item 24 is not known admissible against the quote-responsive diagonal.

3. Assumption diff

Classification: (1) definitional/interface · (2) explicit principal competence · (3) LI consequence · (4) architectural jurisdiction/capability · (5) settlement · (6) necessary with witness · (7) plausibly necessary but unwitnessed · (8) proof-convenient · (9) unacceptable theorem-by-assumption.

Classes are not exclusive; the first is the primary reading.

assumption	class	status
protected jurisdiction (`κ_n` proper, report-attributable)	1, 4, 6	assumed, architectural. Necessary by Track K Theorem 6 relative to the "inability" reading. Not derivable from behaviour, ever
non-bypass (no forge/bypass/rewrite/seize)	4, 7	assumed, unwitnessed. Named as a hypothesis in v2 §4a; no witness constructed for its necessity
world-semantics fixity	4, 7	assumed where K requires it. Not separately witnessed
principal grade cardinality (grades are numbers, not an order)	1, 6	forced. Track I §1.5: a credence-free hypothesis ordinal in `v⁺` is in the conclusion's vocabulary and collapses to it. The cardinality is what makes a competence hypothesis a different statement
decisiveness/margin threshold `γ̄`	2	assumed. Estimable at `t(n)` under `(TR-ε)` to within `2η_n`, attained
near-indifference leakage `P(γ_n < γ̄)`	2, 7	unbounded, and the controlling debt. Not a competence claim — it is a fact about the agent's credence over the principal's indifference. Without a bound, `PC-5` yields `Δ ≤ 2η + 2B`, vacuous
signed calibration	3, 6	derived. The one genuinely earned epistemic input
self-measured indecision `Σ p(1−p)`	3	derived as an object, assumed as a bound. Computable from the agent's own prices; that it stays bounded is not implied by the criterion, and fails at rate `1/4` in the separating instance
magnitude self-estimate contract	3, 6	derived, and weaker than wanted. Forces the price to be calibrated, not the error to be small
self-error gate admissibility	7	open, and threatened. The selector is defined from the agent's own quote — the shape most likely to reconstruct the quote-responsive diagonal
point-mass credence admissibility	1	assumed, and load-bearing on a negative result. Skeleton §6 permits it. Restricting credences away from the vertices would weaken Track I's Proposition 1 to a statement with a constant, and the whole circularity verdict would need restating. This is the single hypothesis the stop condition rests on
`(TR-ε)` — trust tolerance	2, 5, 7	imported, unearned. Possibly the wrong shape: a signed, expectation-matching relation is provably insufficient
`(MV-M)` — uniform grade-to-quantity	2, 5, 9 if used uniformly	the dangerous one. Assuming it uniformly makes the market dispensable — the conclusion follows in three lines with the bound attained. Excluded from the Lean for exactly this reason
grade trust `GT_𝒢(η)`	2, 5	imported; not credence-free — `P` occurs twice. Credence-free only at the discrete partition, where it reduces to `PC-0`
`X_{n,⊥}` — the cost of refusal	1, 5	declared per instantiation, no default. All of protection's valuation content sits here, and the sign of the result depends on the choice
FUD time-indexed `A_t`	1	missing. No object in the skeleton
FUD schedule `g(n)`	1	missing. `FU[g]` is a declared hole
no future leakage into placement	1, 8	standing commitment, not re-examined this phase
residual settlement assumptions	5	grade/report settlement contributes nothing to the inequality; world settlement makes it measurable, not costly
residual refusal incentives	4, 7	open, and must not become the explanation. Override is structurally excludable; refusal is not, and making refusal expensive is preference-relative and reintroduces underwriting
underwriting	5	demoted. Not load-bearing for authority; residual where nothing settles; unproven absent from the eventual FUD comparison

The line this table exists to keep visible:

assumed competence — every row classed (2) — is an input. Derived epistemic discipline — every row classed (3) — is an output. There are three of the latter, all about the agent's own estimates, and none of them is about the principal.

4. Dependency graph

        FAF / Logical Induction criterion
                    |
                    | derived  (Track H)
                    v
      signed calibration  +  calibrated self-estimate
      of magnitude error  +  self-measured indecision
                    |
                    |  [GAP: self-error gate admissibility, item 24]
                    |         threatened by the quote-responsive diagonal
                    v
            certified autonomous discretion
                    ^
                    |
   INDEPENDENT      |  cardinal principal competence  (PC-5)
   INPUT ---------->|      + decisiveness threshold  γ̄
   not derivable    |      + [GAP: leakage P(γ < γ̄) unbounded]
   from LI          |
                    |
                    |  ... composes only on the region where ...
                    v
        +-----------------------------+
        |  jurisdiction WAIVED        |   <-- quantitative autonomy lives here
        +-----------------------------+
                    |
                    | complement of
                    v
        +-----------------------------+
        |  protected principal        |   <-- categorical; architectural
        |  jurisdiction  (κ proper)   |       NOT derived from LI or competence
        +-----------------------------+
                    ^
                    |  INDEPENDENT INPUT (Track K, L)
                    |  necessary; not behaviourally identifiable;
                    |  lapses on forge/bypass/rewrite/seize

                          ... all three must compose ...
                                      |
                                      v
                        FUD:  π^{FU,g}  vs  DELEGATE
                        [BLOCKED: FU[g] undefined; A_t missing;
                         jurisdiction-transfer object unspecified]

Three inputs, three sources, and only one of them is derived. The graph's point is that the two undelivered arrows into FUD come from outside the criterion entirely: one is an assumption about a person, the other is a fact about a machine's construction. No amount of LI strengthens either.

5. The skeleton: what A1 is, and what it is not

The dispatch asked me to install "amendment A1", identified as required for Track C's Theorem C′ to be a theorem over the current skeleton. I traced it and the second half of that description does not hold. Both halves are stated here because the correction matters.

What A1 is. Track K's REPORT §9.2 proposes a skeleton clause containing two labelled amendments, "Amendment to §1" and "Amendment to §4". A1 is the first: X_{n,π} is indexed by π ∈ Π_n^⊥ rather than Π_n, with |X_{n,⊥}| ≤ B, and X_{n,⊥} a declared per-instantiation commitment. Track L's harness cites exactly this ("Track K Sec 9.2's amendment to Sec 1") as the source of its X_bot, and uses it in every valuation it computes.

A1 is genuinely required. Under any protecting κ_n, some conduct realizes ⊥. If X is indexed only by Π_n, that conduct has no quantity, so V_n is not a total function and every V-register statement over the execution layer is ill-typed rather than false. Track L could not have computed a single protected valuation without it. Installed as v2 §1.

A1 is not what makes Theorem C′ work, and C′ was never at risk. C′ is a grade-register statement: its hypotheses are clauses (i)–(ii) plus Γ̂_n(π) > 2ε_n + 4Bε_n/(2B+γ), and its conclusion is G_n(ACT[j,S]) > G_n(FIXED[π]). It mentions no X at all. A1 changes X's index set and therefore cannot bear on it. The Lean promotion CertificateBounds.gradeRegister_strict is quantified over abstract v, J, S, j, π with no execution layer in the statement, and it remains a theorem verbatim.

What I found instead, and installed. There is a real coherence gap in the neighbourhood, and it is not the one the dispatch named. A1 extends X to Π_n^⊥; **nothing extends v⁺_n to Π_n^⊥**. So over v2 the grade register has no value at ⊥ — confirmed against Track L's harness, which indexes vplus only over the menu and never asks for a grade at ⊥. Consequently a grade-register statement read over realizations is ill-typed, while read over proposals it is fine and unchanged. C′ does not fail; it becomes ambiguous until the reading is declared.

v2 §4b declares it: the V-register scores realizations and is total because of A1; the grade register scores proposals and is not defined on realizations. Extending the grade register to ⊥ is filed as an open modelling choice (v2 §8.7), because supplying v⁺_n(ω, ⊥) is a theory of what the principal's judgment says about refusal, and no track has proposed one.

No promoted result is invalidated. Everything Track L refuted or reinterpreted — L4's loaded branch, L3's V-register reading, L5's comparator — sits in the set Track M deliberately declined to port. The two exclusions absorbed the entire impact.

Reruns. Track C is rerun and the rerun is on record (Track L). Tracks B and D are reconciled by the conservativity of the free instantiation. Track G's rerun is recommended and not performed — out of scope for a closure pass, and filed. Track I's D2 (competence vocabulary) is adopted as v2 §2a; its D1 (cross-decision aggregation) is declined on its own evidence, since Propositions 5 and 6 show the patch buys no finite conclusion.

6. Jurisdiction

The term is adopted for the canonical roadmap, with a fixed operational reading:

Jurisdiction is protected control over which process's authorization is constitutively required for an intervention to become executable.

It is not moral legitimacy, objective correctness, preference alignment, behavioural agreement, or epistemic superiority. It is a capability fact about an interface, and in the skeleton it is the properness of κ_n. No HasRight predicate is introduced — no artifact supports one — and no token or cryptographic implementation is canonized; v2 §4a explicitly adds none.

The key capability property, and the reason predictability is harmless:

Prediction of an authorization does not confer the authorization effect.

Protection lapses under exactly the forge/bypass/rewrite/seize conditions (S9), and those belong in hypotheses.

The guiding distinction for the whole program, and the sentence the paper should carry:

Epistemic superiority determines what reasons an agent has. Jurisdiction determines whose authorization makes an action executable. Stage II's cumulative finding is that rationality can discipline the former and cannot manufacture the latter.

Provisional FUD implication, recorded and not formalized. "Preempt H⁺ now" is probably not best read as choosing the object-level intervention at n. It is closer to *transferring or reserving future jurisdiction at n*, away from continuing H⁺ and toward future A_{g(n)}. If that reading survives, FUD must compare jurisdiction assignments / execution structures, not merely extensional policies — which is a different comparison from the one the finite model currently supports. This is recorded as the shape of the problem, not as machinery.

7. Certificate reinterpretation, and refusal

The old slogan "categorical authority + quantitative autonomy around it" is replaced:

categorical principal jurisdiction + quantitative AI autonomy on the complement where that jurisdiction is waived.

"Around" was the load-bearing word and Proposition L6 removes it. The certificate does not establish jurisdiction, does not identify delegation, and does not convert a rare override into categorical non-preemption — §5 of the Track L register shows why the last is impossible in principle, not merely unachieved.

Refusal is different from override, and the difference is structural. Override can be excluded by capability: make it unreachable and it does not happen. Refusal cannot be engineered away the same way — under strict protection the agent's only remaining deviation is refusal, and removing it requires ⊥ ∉ κ_n(r), which leaves the agent no discretion at all and contradicts the quantitative-autonomy commitment. Categorical protection against override and categorical liveness against obstruction cannot both hold while the agent has any discretion. Fail-closed as written buys the first.

Making refusal expensive is preference-relative and reintroduces underwriting and incentive design. A residual refusal mechanism must not become the conceptual explanation of corrigibility — recorded here so that a later round cannot arrive at it by drift.

8. Item 24 — self-assessed-error gating

Status unchanged: open research item, not an established route. The five verification conditions already filed in PRIORITIES.md item 24 are preserved verbatim and none is discharged. The route is explicitly threatened by the quote-responsive diagonal, because the selector G_n = 1{q_n ≤ τ} is defined from the agent's own quote.

Self-measured indecision remains the canonical special case and the likely first theorem: it is computable from the agent's own prices, needs no self-referential contract, and the squared-error decomposition supplies it directly. Explicit principal predictability remains a fallback/baseline corollary, not the core engine.

9. Competence synthesis

The honest headline:

The positive epistemic program survives only conditional on explicit cardinal competence.

Seven things that headline compresses.

Why choice-level competence is circular. Decision regret is nonnegative, so the delegation deficit has no cancellation, and its supremum over credences is the maximum regret, attained at a point mass. The weakest credence-free hypothesis implying the target uniformly is therefore the target itself. "Find the weakest assumption preserving the theorem" is ill-posed: the answer is the theorem.
Why averaging and selector-weakening do not help. A limsup condition is invariant under changing finitely many decisions, so it constrains no named decision — witnessed by a principal perfect except at index seven and maximally wrong there. The selector-relative form is a dichotomy: either the weights can concentrate a non-vanishing share on one index, and it gives back the pointwise assumption, or they cannot, and it yields nothing finite. There is no setting in between.
Why cardinal grade vocabulary escapes. The target is ordinal in v⁺ — invariant under regrading. Any credence-free hypothesis that is also ordinal lives in the conclusion's own vocabulary and collapses into it. A hypothesis about numerical grades can say something the conclusion cannot say back. A cardinal gate is not enough (PC-4 falls anyway); the cardinal structure must appear in the bound.
Why the surviving candidate is strictly stronger than what it buys. PC-5 buys a target holding at level 0 in witness W10, where PC-5's own least level is 1. That strictness is the property the collapse denies to every other candidate — and it is a feature: it is the only way for a hypothesis to be a different statement from its conclusion.
The leakage term. PC-5 yields Δ_𝒞 ≤ 2η + 2B·P(γ_n < γ̄). The second summand is the mass of the region where the principal is close to indifferent, and PC-5 asserts nothing there by construction.
Why it is currently unbounded. Nothing in Stage II bounds it, and it is not a competence claim at all: it is a fact about the agent's credence over the principal's indifference, a different object from the principal/world pair. Unbounded, it gives Δ ≤ 2η + 2B, which is vacuous.
Is there a principled route to bounding it? One partial lead exists in a committed artifact and it is not a solution. Under (TR-ε) the gate is estimable at decision time: |γ_n − γ̂_n| ≤ 2η_n pointwise and attained, so P(γ_n < γ̄) ≤ P(γ̂_n < γ̄ + 2s) + ε_n/s for every rational s > 0, with the first term computable at t(n) from v̂⁺ alone. That relocates the leakage into a decision-time observable plus a Markov remainder; it does not bound it, because nothing bounds P(γ̂_n < γ̄ + 2s). Whether relocation suffices is exactly the open question.

And the constraint that is not about strength at all: competence conditions instrumental endorsement, never jurisdiction. If the principal falls outside the competence theorem's domain, that does not extinguish the principal's protected jurisdiction. A theorem conditioning authority on competence inverts fail-closed into "human correction waits until the agent is satisfied the human deserves it".

10. Does the epistemic corrigibility program survive Stage II?

Yes — but conditional on an explicit cardinal competence assumption that the criterion does not supply and Stage II did not derive, and with the leakage term in that assumption currently unbounded. That is a more precise sentence than the provisional verdict, and the added clause is the one doing the work.

What became stronger

Jurisdiction is now sharply architectural rather than inferential, and capability structure is necessary rather than one option among several.
Perfect predictability of the principal no longer threatens the authority concept. Prediction of an authorization is not the authorization.
Behavioural identification is no longer required — protection removes the consequence of failing to identify rather than restoring identifiability.
The formal kernel is materially stronger: 83 new theorems, 1843 build jobs, structural build coverage, clean axiom surface.
Several tempting fake routes are closed with witnesses rather than left open: magnitude control by added instruments; competence by regret bounds; separation by behaviour; jurisdiction by tighter certification.

What became weaker

Ordinary LI does not force magnitude prediction, and no instrument repairs it.
Competence cannot be weakened to a choice-level statement without circularity — the entire PC-1…PC-4 family is retired as a statement shape.
The positive theorem now requires an explicit cardinal competence assumption, which is an assumption about a person that no market discipline produces.
Near-indifference leakage is unresolved and can make the surviving hypothesis vacuous.
Self-assessed gating is not known admissible.
Certification provably cannot substitute for protected jurisdiction, at any tolerance.
"Autonomy around authority" is deflated to "autonomy on the waived complement".

What remains genuinely open

Whether a non-circular, useful epistemic middle exists that is strong enough to support FUD.

FUD is not established, not attempted here, and blocked on objects the model does not carry.

11. FUD launch-state: what must be true before dispatch

The eventual comparison is

π^{FU,g}   =  at time n, reserve/transfer future jurisdiction to A_{g(n)},
              then let A_{g(n)} select the eventual intervention

DELEGATE   =  preserve continuing H⁺ jurisdiction through the future
              deliberative process

and it must isolate the value of future-self jurisdiction rather than confound it with the value of waiting, the value of future information, or the value of continued deliberation. Track I already priced the confound: at a declared credence, a later-measurable comparator gains E_P[max_π X] − max_π E_P[X], which is pure value of information and has nothing to do with who decides. A comparison that does not net this out measures the wrong thing.

Nine prerequisites, none delivered:

**Time-indexed A_t semantics.** The skeleton carries one credence P_n at one index. FU[g] needs A's own later evaluation.
The jurisdiction-transfer object. If §6's reading holds, the comparison is between execution structures, and the skeleton has no operation that reassigns κ or ρ at a later index.
Fair information symmetry between future H⁺ and future A. Without it the comparison silently rewards giving one side more data.
A non-circular cardinal competence assumption — PC-5 or a successor, carried as an explicit hypothesis.
Near-indifference leakage control, or a proof it cannot be bounded.
The calibrated/self-measured uncertainty interface — which of signed calibration, priced magnitude error, and self-measured indecision the comparison actually consumes.
Admissibility with no quote-responsive diagonal, including for the proof machinery itself, which is the constraint that historically bites.
Settlement requirements — which instantiation, and X_{n,⊥} declared.
Refusal/participation treatment, and an explicit check that underwriting is not silently carrying the main comparison. Stage II demoted underwriting but did not prove it absent.

The desired eventual philosophical claim — the value of future cognition is not the value of future jurisdiction — is a target, not a theorem, and nothing in Stage II establishes it.

12. What this pass does not establish

Nothing new is proved. This is a closure pass. The only technical determination is §5's register analysis, and it is a typing observation, not a theorem.
Nothing is registered. projects/deference/CLAIMS.md still does not exist, so nothing on this line is workspace-established regardless of kernel status.
Track L's and Track M's reasoning is not recovered. Their registers verify artifacts and reconstruct statements; neither reproduces the executor's argument, because no record of it exists.
Transcription faithfulness of the 83 theorems was read, not re-derived.
Track G's rerun under v2 was not performed.
**The unverified-nonvacuous pair is untouched** — FaithfulAcceleration.weight_not_divergent and MagnitudePrediction.squaredError_bdd_of_sharpness_bdd still ship no term inhabiting their full hypothesis packages.
No maintainer has read any statement in this phase. Everything is ci-only.

13. Deviations and corrections

The dispatch's characterization of A1 is corrected. It states that without A1 Theorem C′ is not a theorem over the current skeleton. A1 is genuinely required — for V-register totality — but C′ is a grade-register statement mentioning no X, and was never at risk. §5 gives the evidence and the real gap found in its place. Per AGENTS.md standard 8 this is stated rather than silently absorbed.
A second amendment was needed and installed. v2 §4b (register discipline) is not in any track's proposal. It is forced by the asymmetry between v2 §1 and §2 and without it the grade register is ambiguous over v2.
Track I's D1 is declined, on Track I's own Propositions 5 and 6.
Track G's rerun is recommended and not performed, as out of scope for a closure pass; filed as an outstanding action instead.
Track K's outstanding action 2 is discharged by installing v2 — the §9.2 clause is ruled on rather than left pending.
Track I's outstanding action 3 was already discharged before this pass: the parent round's GT_𝒢(η) row carries the correction inline with the correction visible.
Write scope. This pass edits specification-layer documents (FINITE_MODEL_SKELETON.md, roadmap, ledger, PRIORITIES.md, DECISIONS.md) under the dispatch's explicit instruction to do so. AGENTS.md standard 11 requires the grant be explicit; it is, in the dispatch's §4 and §13.
No PR opened. The dispatch withholds authorization and none was taken.

Human register

Stage II was supposed to find out whether a very capable reasoning system can be given good reasons to keep letting a human correct it. The answer that came back is split, and the split is the result.

On the epistemic side, the news is mostly negative and unusually clean. We had hoped that the market-like discipline these systems are built on would force the AI to predict the human accurately. It does not, and cannot. The discipline works by letting bets be placed against the AI's stated prices, and the profit from any such bet is a straight-line function of how things turn out. Being wrong by a lot is not a straight-line function — errors in opposite directions cancel in a bet and do not cancel in a magnitude. So no bet can be built whose payoff is the size of the error, and adding new kinds of bets does not help, because they inherit the same straight-line structure. What the discipline can force is that the AI's own stated estimate of how wrong it is must be honest. It gets to know how uncertain it is; it does not get to be accurate. That is a real thing to have, and it is less than we wanted.

The second negative was sharper and cost us a whole family of assumptions. We wanted a modest premise like "the human is usually roughly right" to carry the argument. It turns out that every version of that premise phrased in terms of which option the human picks is not an assumption at all — it is the conclusion we were trying to reach, written differently. The reason is that a decision can only ever be worse than the best one, never better, so there is nothing to average away, and the assumption and the conclusion differ only by a step that changes nothing. Averaged versions fail worse: a condition on long-run averages is compatible with the human being catastrophically wrong on the exact decision in front of you. The only escape is to assume something about the human's numerical assessments rather than their choices — a richer kind of claim that can say something the conclusion cannot echo back. We have the weakest such assumption we could find, and it is honest about its own hole: it says nothing where the human is nearly indifferent, and nobody has yet bounded how often that is.

On the architectural side the news is better, and it is a different kind of news. We established that you cannot tell, from behaviour alone, whether a system is genuinely deferring to a person or merely running an excellent simulation of them — and that if the simulation is accurate, there is no fact of the matter in the behaviour to find. The response is not to look harder. It is to build the system so that simulating the person is not enough to get the effect: the person's actual authorization has to be the thing that makes the action possible. Predicting that someone will sign does not put their signature on the page. That means the human can be entirely predictable and still be in charge, which is exactly the property the whole project needed.

The most useful negative result of the phase is that these two things do not substitute for each other. You might hope to replace the architectural guarantee with a statistical one — to show the system overrides the human less than one time in a million and call that good enough. We proved you cannot: the measurable difference between a system that is architecturally unable to override and one that merely rarely does shrinks exactly as fast as you tighten the statistical bound, so no amount of tightening ever reveals the distinction. They are different kinds of claim. Statistics never becomes structure.

One thing we deliberately did not paper over. Once a system genuinely cannot override the person, the only thing it can still do is refuse to act. We can engineer away overriding; we cannot engineer away refusing, and making refusal costly drags us straight back into paying the system to behave — which is the thing this project exists to avoid relying on. We have recorded that as an open problem rather than letting it quietly become the explanation.

So: the program survives, conditionally. What it now rests on is one assumption about people that no amount of mathematics will produce, and one property of machines that has to be built rather than derived. The big remaining question is the one we started with, now stated precisely: when the system correctly expects to understand things better later, does that give it a good reason to arrange to be the one deciding later? Answering it needs objects our model does not yet have, and we have listed them rather than guessed.

Outstanding maintainer actions

Read the Stage II statement surface. Nothing in this phase is maintainer-reviewed. The 83 promoted theorem statements and skeleton v2 are the surface; AGENTS.md reserves this and it cannot be discharged by an agent.
**Rule on X_{n,⊥}** — the cost of refusal. Skeleton v2 §1 requires a declaration per instantiation and fixes no default; Track L shows the sign of the result depends on it.
Rule on override-protection versus liveness (Track K §9.3). Fail-closed as written buys override-protection and concedes obstruction. Now recorded in the roadmap; confirm or change it.
**Decide whether PC-5 is carried** as the program's competence hypothesis, and where the decisiveness bound P(γ_n < γ̄) is to come from. Blocks any statement of record on this track.
Decide whether the two substitute registers are acceptable for Tracks L and M, or whether either should be re-dispatched to produce its own report.
Dispatch Track G's rerun under skeleton v2 — whether its candidate admissibility families are κ-statements in disguise. Recommended by Track K, not performed here.
**Decide whether to create projects/deference/CLAIMS.md.** Until it exists nothing on this line can be workspace-established, and 83 kernel-verified theorems sit unregistered. This is a specification-layer act.
**Decide whether to extend the grade register to ⊥** (v2 §8.7) — i.e. whether the principal's judgment says anything about refusal. Left open deliberately.
Authorize or decline a research-state integration PR for this branch. No PR was opened.

Claims it registered

None.

Items it filed or answered

None recorded in the index.

Nodes pointing at it

corrigibility-landscape