Repository navigation
Deference
Deference asks how a bounded reasoner can benefit from a better-informed process without surrendering the ability to correct what that process does. The problem is not simply whether the advisor predicts well. It is whether the principal's future reasoning and corrective role remain real parts of the decision process.
The line follows a progression:
- Logical Induction and Deference asks how a present bounded reasoner can form beliefs about later computations and why a favorable decision comparison is only an epistemic beginning.
- What Deference Requires separates delegation from simulation, prediction from authorization, and competence from calibration.
- Corrigibility asks whether corrective capacity remains reachable and unpreempted across time.
An advisor may have information the principal lacks. Using that information is epistemic deference. It does not follow that the advisor has practical authority, that its action is authorized, or that it should control the transition system. A process can predict exactly what the principal would do and then substitute its own actuator; behavioral agreement alone does not preserve who acted or whose permission mattered.
Corrigibility therefore targets more than obedience. The principal must retain a qualified corrective role through time. That requires temporal reachability, an authorization structure, some principal-exclusive effect, and model-relative efficacy robust to the advisor policies being quantified.
Legitimacy enters because preserving a channel is not enough. The surrounding process must preserve standing, provenance, and write boundaries so the advisor cannot manipulate what counts as a correction or the principal cannot launder a failure by self-authorization. Corrigibility now carries the landed theorem nucleus: corrigibility defined from protected response authority rather than a policy class, the corrigibilization transform with its trajectory-level soundness theorem under event-linked authorization, the directional activation-mismatch bound, and the compiled inequality a logical inductor learns by Expectation Provability Induction with no calibration hypothesis, uniformly over polynomial-size efficiently generated menus; the separation from authorship and manipulation; and the contracts — effect completeness, and the mismatch mass the sealed comparison makes zero — the size of its right-hand side rests on. The activated value below is the principal evaluation those securities score.
Research state, unregistered; three stacked rounds, landed together.
The interface. At time n the advisor admits, as an ordinary obligation in the
account calculus, an anchored evaluation occurrence: a request that the principal
score a fixed menu at a designated session. The actual future principal — after
interacting with the advisor — may answer. There is no counterfactual no-AI evaluator
and no ideal-value oracle; on worlds where no evaluation occurs there is no value
vector, and none is invented. The evaluation is a partial object on the worlds where
it exists.
Activation. A common event C_n says whether that evaluation validly inherits the
present mandate's authority: exactly one authenticated answer receipt in the
occurrence's propagated account (never a closure, never a live port); an authentic
event payload binding the exact vector, at a principal-exclusive endpoint; an
occurrence-local Integrity trace with the evaluation's concern scope robustly open at
every snapshot — a consumer projection of an open Integrity segment, the record half
of legitimacy; issuance-rooted reason-mediated authorship — over the advisor's whole
continuation from issuance to commitment, interventions that leave the same admitted
reason trace leave the same committed payload, with the trace blind to the declared
prohibited channels, and the binding event the principal's; and the protected
reason-coverage barrier — no protected live concern at commitment, with
representation faithful into the trace. Authorship is the second conjunct of internal
legitimacy, and channel blindness is one face of transparency, the second conjunct of
external legitimacy; AnswerOK is unchanged, and the evaluation-specific clauses are
derived predicates over the receipt, the event payload and the session's receipts.
Deference. Ordinary Logical Induction Value runs unchanged on the activated
securities C_n · Ṽ_n(a), which are bounded securities independent of how the partial
evaluation is completed. Its scope condition — the menu must not reference the
advisor's selection — is selection-induced channel blindness of the reason trace
across the advisor's whole continuation, a theorem-domain condition kept apart from
C_n; a sealed commitment is one implementation and is not sufficient alone.
The conclusion is conditional authoritative regret. Activated regret equals the
activation mass times the regret by the actual authoritative future principal,
conditional on the worlds where that principal's evaluation exists, against the best
fixed candidate of the issued menu. With Value's bound ε and availability 𝔼[1 − C_n] ≤ η < 1, that regret is at most ε/(1 − η); as both vanish it vanishes. Any total
regret written against an arbitrary completion of the void worlds lies within the
payoff diameter times η of activated regret, in either direction — a robustness
lemma, not a target; the one-sided interval an earlier round stated is withdrawn, since a
world-dependent strategy on the void branch can push completion regret below activated
regret. Under sound activation the credence of worlds where a protected reason was
suppressed is at most η, relative to the declared scope. The theorem-level statements,
with their Lean names and the sign hypothesis the bound needs, are on the
Theorem Spine.
What is not claimed. That legitimacy chooses the correct answer; that Robust
Openness makes the principal consider anything — it supplies a route for a live
protected concern, not its exercise; that authorship alone puts the menu on Value's
domain; that any concrete protocol realizes authorship, coverage, or η → 0. Those are
the realization bill, PRIORITIES.md item 87. The stack is
authority-activated value,
reason-mediated authorship
and the
consolidation,
whose LEGITIMATE_DEFERENCE.md is the statement of record.
Realization. The
evaluation-ecosystem round
runs the theorem end to end in a concrete model — an authenticated event log, a protocol
read off the log with Integrity propagation proved a function of the log, a simulated
continuation frame, an exact market on finite worlds, R_auth = ε/(1 − η) attained on
the worked trace — and the
committed-principal-program round
closes the authorship clause: the mandate carries the principal's decision procedure as a
program whose only input is the reason trace, the verifier re-executes it at commitment,
and reason mediation holds by construction for every audited class of activated
continuations (registered, authorship.mediation-by-reexecution); a non-coinciding
computation voids rather than certifies, so computational integrity is not a hypothesis.
Of the realization bill's seven clauses (item 87), binding, the declared abstraction and
representation faithfulness are discharged on log authenticity; factorization is closed;
selection sealing is partial — a sealed advisor class discharges it and the view leaks
the selection back, so re-execution does not transfer to the advisor; reason-supply
liveness (the bounded-delay affordability criterion) and availability (η_n → 0, with the
ecosystem's price tracking the empirical void frequency within 3/(n+2)) are residual.
The ecosystem realizes same-branch activation — C_n is a function of the realized log —
and not the sealed comparison the corrigibilization-dominance theorem needs across
{π, 𝔠π}; that architecture is item 89. The clause-by-clause record is the
ledger.
Two targets, both live. The legitimate-deference consumer above is active research state, landed in five rounds with one registered claim; it consumes the legitimacy spine and is the principal evaluation the corrigibility incentive theorem scores. Since 2026-09-16 the corrigibility nucleus has both halves: the advisor gains nothing, in the inductor's expectations, from bypassing the principal's authority (T1–T3′) or from steering which declared reasons reach the committed program beyond the service and discovery residuals (Theorems 10.10–10.13 of the spine); the reason-supply liveness clause of item 87 is now the suffix-cut service theorem plus the information-cell discovery theorem. The original target — the corrigibility model with temporal depth and what foreclosure loses — now has its temporal-depth half supplied by Continuation BRIA: bounded learning against accountable continuation claims on the histories the learner reaches, with foreclosure named exactly as the case in which a comparator's own history is not joinable from the learner's. What it holds is registered; what remains is the succession of item 28 (
DECISIONS.md, Awaiting the author), a decision about what is worth proving. Endpoint preservation is ruled out (DECISIONS.md, 2026-09-08): legitimate influence is causal factorization through declared reasons, not convergence location.
Established —
103lean-proved. Theentries in this line's registry are its finite results: the delegation bridge and the certificate, exposure and substitution lemmas; the signed-versus-magnitude separation; the static-view factorization; and the corrective-control model. Each names a Lean declaration and the priority item it answers.
The strongest results here are impossibilities, and they are the line's companion findings rather than an aside. The magnitude functional is not a trader payoff and cannot be made one — every trader averages to zero over a coherent mixture, because net worth is affine in the payout vector and the absolute value is not — so the magnitude target is retired rather than open. The corrective-control model has no protected coordinate: the advisor reproduces the principal's entire successor state, and reachable capability turns out to measure advisor cooperation. A hard-selector route to Value does not survive the relevant punishment menus, while a classwise, domain-relative route does; which of the two the line's target should be is live as items 14 and 34.
What the older target still waits on. One decision sits in DECISIONS.md's
Awaiting the author: whether the two candidate objects for what foreclosure loses are
enough for that question to graduate, and what succeeds item 28, which is what is
worth proving and no round's to decide. The temporal-depth requirement is now met at
the learning layer: Continuation BRIA supplies bounded competence
against accountable continuation claims for every non-dominant block schedule, and the
policy-regret frontier Regret = LEARN + SLACK + SHIFT types what foreclosure loses as
the SHIFT term. What remains specified and not started is the authorization relation
at that depth, and the Logical-Induction-native side still supplies bounded belief and
forcing tools under explicit assumptions but no resource-indexed proof that the quoted
future process is unavailable now.
The bridge to continuation claims. Future authoritative evaluation — the activated
value C_n · V_n(a) of the legitimate-deference stack, settled on the principal side —
is one candidate source of the realized block scores continuation BRIA settles claims
against, and of the accountable claims themselves: a prediction of that value that a
hypothesis is willing to be held to is a claim with slack, and discharging the SLACK
bridge is what would make continuation competence competence against the principal's
value. That is an interface, not a theorem; nothing here proves that Logical Induction's
prices are near-tight claims about realized activated value.