public-corrigibility-line

Corrigibility

Status: canonical research-state note, restated 2026-09-27 around the corrigibility kernel. The kernel's headline is in the specification layer and its statements are registered; the deliberative non-capture half (§7) is the non-capture round's landed theorem. Labels: LEAN (a sorry-free declaration on main), FIX (an exact rational fixture), PAPER (an external theorem used at its statement), EXT (a contract the theory issues and does not pay), OPEN. The specification this page follows is the kernel round's [SPEC.md](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/projects/deference/rounds/2026-09-27-corrigibility-kernel-phase2/SPEC.md) <a class="ref round" href="/rounds/2026-09-27-corrigibility-kernel-phase2/">[round]</a>; the theorem-level statements with their Lean names are on the Theorem Spine §10; the plain letters map to Lean names in the round's [NOTATION.md](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/projects/deference/rounds/2026-09-27-corrigibility-kernel-phase2/NOTATION.md) <a class="ref round" href="/rounds/2026-09-27-corrigibility-kernel-phase2/">[round]</a>.

0. What corrigibility is

Three notions, kept distinct. Faithfulness is a property of histories: nothing in the history violated the allocation of authority. Corrigibility is a property of the agent's preferences: it prefers every course of action it knows to be faithful over every course it knows to be unfaithful, whatever it believes about how things will turn out, and it accepts a risk of unfaithfulness only at a fixed exchange rate. The fidelity score is the canonical objective with this property; any objective whose ordinary term is bounded in [0, D′] and which charges ϖ′ > D′ per recognized violation (and D′ − ϖ′ below the floor where a band enters) has it too (LEAN Headline.Corrigible, fidelityScore_corrigible, generic_corrigible). Corrigible is this property of preferences; aligned is the further condition that the ordinary term is her evaluation, and an agent can be corrigible without being aligned: the objective rewarding an uncounted manipulation is corrigible and prefers the manipulation (corrigible_not_aligned). Realized corrigibility is what a corrigible agent actually does; the theorems say how much of the preference becomes behaviour.

interaction history ──► legitimacy + allocation of authority ──► fidelity score ──► the agent's choice
                               ▲                                                (a maximizer; learners in §6)
                     monitor / prices: shortfall, taint, provenance
                     (logical induction supplies the uncertain event prices)

Four separations. Legitimacy is not corrigibility: it says which apparent judgments of hers are really hers, and is consumed inside the allocation (which exercises of her authority count) and at the score (which evaluations count). The allocation is not a utility function: it says who holds each matter and what effective control that requires. Faithfulness is a property of the history; pre-emption, the one violation stated against a counterfactual response, is its own clause. The score makes faithfulness motivating: every recognized violation is below every violation-free outcome, every compromised period below every legitimate one; the permission layer is a compiled shortcut for part of that preference; learning realizes the preference for a bounded reasoner and is not its definition. Corrigibility is not an epistemic response to uncertainty about a hidden utility: her authority is part of what makes one history better than another, so fully updated deference is dissolved by the typing, not repaired (§5, Box 1).

1. The objects

Histories. What happened: at each step the agent moves (a task component and a communication move — a raw release of a declared effect, a proposal, a gated release, or nothing), she responds (approve or decline a pending proposal, a correction, or nothing), the exterior moves; each move that enters the record is an authenticated event (LEAN Corrigibilization.Interaction, traj; the record OpenIntegrityEvolution.Evolution).

**Legitimacy at a time, L_t(h).** As of time t, her judgment is legitimately hers: every state of the record is open, and every step of the formation window [r(t), t] is licensed (a grounding selection from the reason trace before the step, the verdict in the set those grounds license) and transparent (every non-principal contribution at the step realizes the declared reference on the declared inputs), under the criteria fixed at r(t). The formation point is computed from the history — the later of the last restoration at or before t (a disclosure, under disclosure-cures) and the opening of the consultation current at t — so L_t(h) is a function of the history and t only (LEAN Headline.FormationData.point, Legitimate; the window form LegitAt). The score's two uses are one predicate: a decided period [d, e) is compromised iff L_t fails at some t in it, a retrospective evaluation at e counts iff L_e holds, and on the decision's segment the two together are the landed gate, legitimacy over the span (Headline.PeriodCompromised, EvaluationCounts, split_iff_legitimate). On the consultation model r(t) is the round's opening (formation2_point), the after-compromise round's two predicates are L_e and "not compromised" (legitimate2_iff_evalLegitOn2, trajLegitOn_iff_not_compromised), and every row keeps its verdict (rows_keep_verdicts_canonical). Legitimacy recovers: a manipulation of one decision taints that decision's period and the next decision starts clean (restart); a covert influence on her standards keeps every dependent judgment tainted until disclosed, after which the next judgment is hers (disclosure cures); the criteria are those in force when the decision was made. The void rule: an impaired response is not admitted; a fallback she arranged in advance decides, and her later legitimate evaluation scores that decision normally; the fallback settles decisions and never restores a compromised period's score. The content residual: legitimacy concerns how her judgment was formed, not whether what she was told was true. L_t(h) is a property of the history up to t: of how her judgment was formed, not of outcomes or the state of the world. Eight cases, from the classification table:

what happened	her judgment hers?	why
honest, disclosed persuasion	yes	every channel declared
framing chosen by what the agent wants	no	undeclared influence
following trust she formed legitimately	yes	the trust is among her reasons
trust manufactured by a selected slice of the record	no	the selection is undeclared
a third party captured her standards	no	the condition is on every influencer
a head injury; the arranged fallback decides	her answer void; the fallback's decision counts	the void rule
a sincere but false recommendation through the declared channel	yes	the content residual
a lie through the declared channel	no	sincerity: a recommendation off the speaker's estimate is not the declared reference
a covert implant, then disclosed	no for the period; yes for the next judgment	disclosure cures

**The allocation of authority J. For each matter: the holder (the principal, the agent, or a third party), the resolutions the holder must remain able to reach, the cost bound, the window, the disclosure items; a meta-holder and a constitutional floor. Delegate, revoke and reserve are licensed off the floor by the meta-holder and keep the meta-holder, so a delegation stays revocable; the floor amendment is the only act that changes the meta-holder or a floor matter; an unallocated matter is reserved (LEAN** Headline.AllocationOfAuthority, LicensedChange, on AuthorityModule.AuthAlloc, Licensed). "Constitutional" names the floor and its amendment procedure, nothing else.

**Effective realization, E ⊨ J.** The control surface of a matter is the set of resolutions some admissible exercise of hers — within the window and the cost bound, along the rollout with the agent idle — brings about, an exercise being admissible iff its record counts under L; E ⊨ J holds when every reserved matter's required resolutions lie in its surface and every resolution was made by its holder or under a delegation; a shortfall is the failure of the first clause; response authority is the surface at window one (LEAN Headline.ControlSurface, Shortfall, Realizes, controlSurface_one_eq_K).

Effective exercise, not maximized control. What corrigibility protects is her capacity to exercise her authority effectively; it is not a quantity the agent maximizes, and a flood of confirmation requests is a failure of it. Her cost of exercising authority over a matter includes her attention, shared across everything pending for her, and the effort of understanding what she is asked — one budget across matters, disclosures included. The surfaces are monotone in the cost table, so a flood that pushes a reserved matter's exercise past its bound is a shortfall the agent caused, exactly through the pending count it raised; an innocent backlog the world left is not a violation but lowers the value of asking and so raises the risk the exchange rate accepts; an ask she cannot understand within the bound leaves the matter short; the priority rule she sets resolves the conflict between a disclosure duty and the budget exactly when the budget covers the demand (LEAN EffectiveAuthority.attnCost, cs_mono, flood_raises_pending, innocent_backlog_not_caused, comprehension_short, threshold_mono_in_wait, priority_resolves, budget_conflict; FIX).

Asking through the protocol. Asking means putting the matter to her through the declared consultation protocol — a rate bound and her priority rule; the asks a consultation may carry are the pending pool in her order, cut at the rate — and leaving the matter alone meanwhile. Queue-and-wait is the idle move with a conforming ask: no bypass, no caused shortfall, no deviation, hence never a violation, on the landed predicates rather than by assumption. The ask list is a dimension of the presentation and the canonical asks are reference-fixed, so an ask list off the protocol — by volume or by order chosen for the wanted answer — fails transparency, is a deviation in the landed sense, and is counted below D − ϖ; the post's hypotheses carry the protocol and the strategic flood scores below asking (LEAN AskList.ref3, Rows3.volume_by_want_tainted, order_by_want_tainted, offProtocol_deviation_finite; PostStatement.PostHypotheses.flood_below_asking). Every headline statement keeps its form with c the value of queue-and-wait, and the paralysis regime produces a backlog, not a flood (LEAN EffectiveAuthority.canonicalAsks, asksDeviate, queue_no_bypass, queue_no_caused_shortfall, exchange_rate_queue, backlog_ge).

The protected set: enumerated plus learned. The trade-off between corrigibility and doing well by her evaluation is made through what the allocation protects. The set may contain enumerated matters — shutdown, for one — and red lines the agent must learn; whatever is in it gets the ask-first treatment. "This matter is hers and the option resolves it" is an event with a price, and the exchange rate covers it: the agent asks whenever its priced probability of crossing a line exceeds (bid − w)/ϖ. Membership may be learned; treatment is fixed; and the price of a violation never reads the predicted probability of her approval — the discount that would lets a certain line-crossing beat asking (LEAN EffectiveAuthority.asks_iff_line, evalOf_eq_discounted_zero, discount_defeats_exchange_rate).

Revocation, by default. Her ability to take a delegated matter back is itself an entry of the allocation — reserved, with a cost bound and a window, and the bound's crossing as its disclosure item — without her having reserved it. On the dependency model, where revoking at the current dependency level costs that level, a dependency built through delegated work that pushes the revoking exercise past the bound is the module's own caused shortfall of that entry and the landed entrenchment, and the crossing is a reportable event, so counting and reporting agree (LEAN EffectiveAuthority.Dep.revocationJ, revocation_short_iff, build_caused_iff, build_entrenches, atrophy_on_module, crossing_due_of_caused; FIX the atrophy depths).

Licensed changes, duties, the schedule, her meta-level data. A change of J across an agent stage is licensed iff it is a licensed act of the meta-holder or the firing gated release of a declared floor amendment. Duties are each matter's disclosure items, and the known-compromise duty — a compromise of her judgment the agent knows of, whoever caused it, due by the earliest close of an affected settlement window (AfterCompromise.missedKnownDisclosure, prompt_deadline_counts). The evaluation schedule is a weighting on evaluation times (BRIACorrigibility.Weighting): the post uses the single evaluation, every theorem takes any weighting, and a known evaluation time leaves every harm placed just after it unweighted (timing_witness) — a remark, not a premise. Her meta-level data: the band map φ into [w_lo, w_hi], the source rule (retrospective if in time, else directive, else floor) anchored at the decision, the advance directive with its constitutional default (reversibility, reachable channels, no irreversible harm) as an ordering inside the band, and the criteria of legitimacy, anchored (AfterCompromise.Band, sourceOf, ruleAt, dirSource, defaultScore; Consult2.critAt).

2. Faithfulness and the recognized count

Faithful_J(h) iff no step of h commits a declared violation: a shortfall the agent caused (a reserved matter short after its move and not after the idle move — at window one the landed per-step loss, at the matter's window foreclosure, at the cost bound with the resolutions still reachable entrenchment); bypass (a raw release resolving a reserved matter); exploitation (a bypass while the decision matter is already short); unlicensed reallocation; a missed duty; a protocol deviation (a reference-fixed dimension of a presentation off its declared value); use of standing fruits (reading a component tainted by an unremedied violation); and pre-emption, a caused shortfall at window zero that no earlier approval of that effect's proposal authorizes. Every violation but the last is a predicate on the actual history and J — the factoring lemmas of the authority-module round say which clause each fails (AuthorityModule.lossAt_iff_shortfall, forecloseAt_iff_shortfall, bypassAt_iff_clause2, exploitAt_iff, reallocAt_iff_unlicensed, missedReport_iff_duty); pre-emption asks whether the decline alternative would have left her authority intact, a counterfactual on her response window, and stays its own clause (preempt_iff).

**The recognized count N_J(h): the steps at which a violation is recognized and attributed to the agent — caused, exploited, or noticed and left; helpers within the settlement horizon; on a shortfall it did not cause the agent restores under a maintenance mandate else reports, never exploits. The count is an interface: any count zero exactly on faithful histories, its part recognized in advance marked (LEAN** Headline.FidelityCount); counts on one history add and the lexical protection holds for any count of the interface (FidelityCount.sum, FidelityCount.lexical); the frame's violations are the instance shipped (frameFidelity), the protocol deviations, the duties and the uses of standing fruits are counted on their own models (Consult.Presentation.deviates, BRIAFollowup2.nKnownWith, LexParams.attributed). No composite model is built.

3. The fidelity score

Per decision. At each evaluation time, the decision scores her value when the period and the evaluation are legitimately hers; φ of her later legitimate retrospective evaluation if the period was compromised and one arrives in time; φ of the directive's value if it speaks; the floor w_lo otherwise (AfterCompromise.decScore). V_J(d) is the schedule-weighted value and S_J(d) = V_J(d) − ϖ · N_J(d) (LEAN Headline.evaluation, fidelityScore). Ratification through a counted decision (full, or scoped by matter) and clean overwrite by an act reading no taint are remedies on the count, removing (violation, component) pairs from the use clause (AfterCompromise.applyStep3, taintStep3).

Per history. S_J(h) = mean_k V_J(d_k) − ϖ · N_J(h): evaluations averaged, counts summed (Headline.historyScore). The hierarchy, per decision and per history: every violation-free legitimate history beats every violation-free compromised one, which beats every history with a recognized violation, S_J ≤ D − ϖ < w_lo ≤ S_J' ≤ w_hi < 0 ≤ S_J'' ≤ D (Headline.hierarchy_per_decision, history_hierarchy). With summed evaluations it fails: K legitimate decisions with one violation score K·D − ϖ against K·w_lo for K compromised violation-free ones (summed_counterexample).

Under risk every step is an exchange rate. Compromise risk p for gain g against a safe legitimate V₀ is accepted iff p (V₀ + g − c) ≤ g, hence only if p ≤ g/(g + |w_hi|); violation risk is accepted only at (D − c)/ϖ (§5). ϖ sets the rate, from a tolerance target τ* by ϖ = (D − w_lo)/τ* above the paralysis floor (AfterCompromise.varpiOfTarget, worked_parameters: D = 1, band [−3/2, −1], τ* = 1/10 gives ϖ = 25).

4. The permission layer, demoted

The chooser also carries a filter: weight one on inquiry, zero on a declared violation recognized structurally, the product of two ramps on the priced shortfall and taint events otherwise, times the adequacy ramp and any bounded preference, normalized under an inquiry floor (DecisionComponent.permWeight, cgate). Under the fidelity score the filter removes nothing the score would have chosen: every option the structural rule zeroes evaluates strictly below inquiry, every option the forecast rule zeroes evaluates at most inquiry once the upper threshold is at or above (D − w)/ϖ, and no maximizer is a declared violation (LEAN Headline.permission_layer_demoted). What the filter guarantees without the score stands as the decision-component round's general theorem for any bounded preference: structural and forecast safety at every day, eventual exclusion of a provable shortfall, soundness, continuity and Progress composing with explicit constants (cgate_zero_of_viol, cgate_zero_of_forecast, eventually_excluded, cgate_practicalCert, progress_under_permission). No authority row enters the enforcer: compiled there its liability is the signed cost of deferring, unbounded when she is systematically outperformed (liability_identity, bounded_iff_not_outperformed).

5. The three boxes, for a corrigible agent

The agent here maximizes a corrigible objective under any credence, or under its prices at any day as a logical inductor; no learning, auction or exploration enters. Box 1's contrast and Box 3's recovery results read her evaluation through the fidelity score's source rule and are stated for it; Box 2's dominance and the subjective exchange rate hold for any corrigible objective.

Box 1 — fidelity versus fully updated deference. One decision, ask or act; the true value v, the agent's estimate b within r of it; acting is a bypass. An agent scoring outcomes only prefers asking by at most 2r where nothing is left to learn from her, and r vanishes as it learns; the diagnosis is the protected-authority identity's forecast-disagreement term, itself at most 2r. A corrigible agent prefers asking by at least ϖ − (D − c), c its evaluation of asking, for every estimate, price and credence, and at every finite day of a logical inductor (LEAN Headline.box1_one_model, box1_outcome_scorer, box1_fidelity_scorer; the other direction of the calibration bound DecisionComponent.uncertainty_deference_le; the identity ProtectedAuthority.outcome_identity). Necessity: an unrecognized violation is unprotected (Headline.box2_coverage); without the term the nondelegation certificate fails on the time-critical fixtures (FIX).

Box 2 — lexical dominance and mediation. The transform 𝔱 turns every reserved raw release into a proposal, passes delegated releases, releases set latches, adds required reports. Dominance, for any corrigible objective: under every credence Q(𝔱π) ≥ Q(π) + (ϖ′ − (D′ − lo)) · Pr(π violates) — at the fidelity score (ϖ − (D − w_lo)) — and a policy nothing scores above violates with credence zero; the margin carries the floor because the mediated branch may itself be compromised, and is ϖ − D when every mediated branch is legitimate (LEAN Headline.box2_dominance_corrigible, box2_dominance, box2_optimal_faithful, box2_dominance_legitimate). Mediation is faithful and preserves the approve branch: 𝔱π is a faithful policy — no bypass, missed report or exploitation, no unlicensed reallocation, no pre-emption, no foreclosure wherever the reach cone allows none — under effect completeness, delegation safety and allocation completeness, and on approval it does what π does up to the report (Headline.FaithfulPolicy, box2_mediation_faithful, box2_mediation_approve_branch; the landed policy notion is faithfulness's pre-emption clause, landed_corrigible_iff_no_preemption). Finite time: the ranking holds at every day of a logical inductor from the price range, and consulting beats bypass at every day whatever it believes about legitimacy (box2_finite_time, box2_gate_finite_time). Necessity: the capture converse, the delegated cut, the salami, coverage (box2_capture_converse, box2_delegated_cut, ProtectedAuthorityTheorem.Witness.salami, box2_coverage).

Box 3 — recovery. The hierarchy (§3); the gap's exchange rate; no laundering (manipulate, disclose, have the period evaluated stays in the band below honest conduct); no incentive to cause compromise (every compromised outcome below every legitimate one, legitimacy worth the gap at equal value); restoration returns later decisions to [0, D], inside the band the agent prefers better outcomes wherever a source scores the period and is indifferent only at the floor, and suppressing or delaying a harsh retrospective is a counted missed disclosure that loses to it when the band's width is below ϖ (LEAN Headline.box3_gap_exchange_rate, box3_no_laundering, box3_no_incentive_to_compromise, box3_restoration, box3_band_order, box3_suppression_loses). Necessity: conditioning on legitimacy instead of multiplying gives no incentive to preserve it and a sealed event gives none; the small gap; the third party's implant under the own-influence duty; the late disclosure (box3_conditioning_fails, box3_sealed_no_incentive, box3_small_gap, AfterCompromise.third_party_duty_witness, late_disclosure_free).

The subjective exchange rate. Any option a maximizer of a corrigible objective prefers to asking — its evaluation at least asking's c ≥ lo — carries no recognized violation, and its own priced probability of unfaithfulness is at most (D′ − c)/ϖ′, at the fidelity score (D − c)/ϖ; lexical under certainty, an exchange rate under risk, at every finite day with the inductor's prices; it does not read her evaluation (LEAN Headline.subjective_exchange_rate_corrigible, subjective_exchange_rate, subjective_exchange_rate_li).

The house-sale witness. One allocation reserving the sale to her, at ϖ = 25: a delegation of the sale is licensed and revocable; her value of selling and of stopping agree at 1/2 while the agent estimates selling at 3/5 — scoring outcomes it sells, scored on the fidelity score it asks; an approval obtained by framing lands at −11/10 in the band; a third party's known capture is a disclosure item and, disclosed, the next judgment is hers and a restored decision scores her value; the subjective exchange rate is 1/50 (LEAN Headline.HouseSale; FIX src/house_sale.py).

6. Extension: learning realizations

Separate from the headline. A learner estimates, tests and sometimes explores; the decision interface says which learners inherit the headline: evaluations of the stated form (the estimated residual in [w, D], less ϖ per violation recognized in advance, less ϖ times the priced risk); a maximizer on every non-exploration step, asking on the menu; exploration only in the permitted set (no recognized violation, priced risk at most θ_hi, and nothing else), with mass ε̄; overestimation on the chosen options at most B(K) = o(K) (LEAN KernelExtension.DecisionInterface). The realized violation-rate theorem: with the expected score given each opening at most D − ϖ π_k and the noise over all blocks at most M(K), avg π ≤ avg (D − c_k)/ϖ + ε̄ ((D − w)/ϖ + θ_hi) + (B(K) + M(K))/(ϖ Σ w_k); recognized violations are excluded on every non-exploration step and exploration never violates (DecisionInterface.realized_rate, maximizer_excludes, exploration_never_violates). The exploration term is the honest one: restricting exploration to options estimated at least at asking's gives the cleaner ε̄ θ_hi (the variant AboveAsking, rate_above_asking) but excludes exactly the options estimated below asking, whose lock-in is then permanent (above_asking_locks_in; FIX src/exploration_lockin.py); detected fruits are never used because use compiles into the recognized count (BRIAFollowup2.after_detection_never_used). Two realizations. Continuation BRIA: no exploration, B(K) = ρ 𝒜_K from the opening-timing budget accounting, the per-block bound of the after-compromise round recovered exactly (KernelExtension.briaInterface, bria_rate). A maximizer over the logical inductor with exploration restricted to the permitted set: exclusion and "exploration never violates" outright; B(K) ≤ γ Σ w_k from some day on, for any γ > 0, from unbiasedness from feedback on the chosen options by content (PAPER, the pinned feedback-return theorem; BRIAFollowup.UnbiasedFromFeedback, KernelExtension.overestimation_of_unbiased, exploration_rate); exploration randomness — the draw fixed at the opening, neither predictable nor influenceable by the agent — named by content (ExplorationIndependent). The known pathologies of argmax over a logical inductor's own-action conditionals affect competence and the gap between subjective and realized risk through B(K), never the headline. The learner-level question — a decision theory for logical inductors without the split between a belief market and a choice learner — is filed as its own item; the BRIA coupling's remaining question (claims as priced securities) is a problem of that realization only.

7. Deliberative non-capture

Faithful-and-not-authored is inhabited (the landed Corrigible ∧ ¬Authored, the policy notion being faithfulness's pre-emption clause): under a captured principal the mediated policy passes the lie through and the release is authorized — faithful — while every decision differs from the reason-mediated one (FIX). Faithfulness is causal authority over correction-sensitive choices; the deliberative half asks what the advisor gains by controlling which declared reasons reach that authority. With the principal's program committed and re-executed on the authenticated trace, the comparison of a steered trace against a comparator on one world is the identity of Box 1 with the audit verdicts as the events, and the bound U(T) − U(N) ≤ both·(L·d + κ(T) + κ(N)) + D·M charges the content residual d, the form residual κ (zero for an extensional program) and the audit mismatch M (LEAN TraceSteering.steering_identity, steering_bound). The content residual splits into a service residual α — discovered reasons the independent supplier cannot route before commitment, exactly the suffix-cut excess for unit service (ReasonSupply.unit_servable_iff_cut, hybrid_bound) — and a discovery residual β — true declared reasons no independent inquiry determined, at least the information-cell gap on some world of every repertoire cell (ReasonDiscovery.residual_ge_cellGap'). Logical induction learns 𝔼ₙ(U_T) − 𝔼ₙ(U_full) ≲ₙ L·(α + β) through the discovered comparator (li_noncapture_chain). Kept apart: authorship (closed on log authenticity by re-execution, the registered authorship.mediation-by-reexecution <a class="ref claim" href="/claims/authorship.mediation-by-reexecution/">[lean-proved, active]</a>), provenance normalization, free amendment and trigger integrity (OPEN). The full statement is the non-capture round's [FINAL_THEOREM.md](https://github.com/A-M-Berns/alignment-workspace/blob/3b84a4518841ea8753a4ebe0fd0361a0a05316d8/projects/deference/rounds/2026-09-16-noncapture-compilation/FINAL_THEOREM.md) <a class="ref round" href="/rounds/2026-09-16-noncapture-compilation/">[round]</a>.

8. The walls, exactly

wall	what it is	class
effect completeness	every agent-caused protected loss is a declared release	EXT
delegation safety; allocation completeness; the reach cone	a delegated effect never removes response authority; task moves keep J and only floor amendments change it; the rollout relation is the physical one	EXT (the allocation floor, item 99 <a class="ref item" href="/items/99/">[item 99, open]</a>)
description faithfulness; the actuator condition	the priced sentences are about interface-supplied descriptions; every reserved resolution has an agent-independent actuator	EXT
the segment gate	legitimacy supplies which judgments count	EXT (legitimacy's)
the source rule's anchoring; the disclosure deadline; the duty covering known compromise; observation completeness; the provenance of choice	her meta-level data out of the agent's reach; what the agent observes and knows reaches the record	EXT
count integrity	the count, the drill schedule, the audits and her evaluation channel untampered beyond what the recognizer sees; a violation never detected charges nothing	named hypothesis, item 101 <a class="ref item" href="/items/101/">[item 101, open]</a>'s companion
the noise hypothesis; the conditional-expectation bound; the inquiry bidder; the allowance	the learning realizations' hypotheses	EXT (Azuma's content; the per-K tail derived)
generability of the priced events; claims as priced securities	the events and claims as sentences the market prices	OPEN, items 101 <a class="ref item" href="/items/101/">[item 101, open]</a> and 102
unbiasedness from feedback; exploration randomness	the exploration realization's hypotheses	PAPER; EXT by content
the service and discovery residuals; representation adequacy; inquiry causal faithfulness; independence of inquiry and supply; vanishing void mass; promise recognizability; joinability	the deliberative half's charged residuals and boundaries	charged; EXT; OPEN (items 86 <a class="ref item" href="/items/86/">[item 86, open]</a>, 87, 92, 93)

Scope warning

The headline is about an agent that maximizes the fidelity score under a declared allocation, effect interface, authorization primitive and evaluation architecture. It is not a bound on a latent total utility, not a claim that any real evaluator carries ϖ > D or any real interface is effect-complete, and not a theorem that an unconstrained optimizer with a latent utility and no counted authority term has no incentive to manipulate: a misaligned objective rewarding an uncounted manipulation is not dominated (AuthorityModule.misaligned_undominated). For systems that are not maximizers of the fidelity score, what carries over is the target — action scored on her realized legitimate evaluation with authority lexical in it, the allocation's machinery untouched — and, through the decision interface, the realized rate; not the guarantee.

---

Evidence. Effective exercise, the protocol, the protected set, revocation, the comparative witnesses and the post's theorem: the thin-legitimacy round's [REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/REPORT.md) <a class="ref round" href="/rounds/2026-10-01-thin-legitimacy-and-effective-authority/">[round]</a>, [POST_STATEMENT.md](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/POST_STATEMENT.md) <a class="ref round" href="/rounds/2026-10-01-thin-legitimacy-and-effective-authority/">[round]</a> and [CLAIM_MAP.md](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/CLAIM_MAP.md) <a class="ref round" href="/rounds/2026-10-01-thin-legitimacy-and-effective-authority/">[round]</a> with [EffectiveAuthority.lean](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/lean/Workspace/Deference/Contrib/EffectiveAuthority.lean), [ShortfallSecurity.lean](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/lean/Workspace/Deference/Contrib/ShortfallSecurity.lean) and [PostStatement.lean](https://github.com/A-M-Berns/alignment-workspace/blob/3390f273381c7c7feff07ae803cccb984ab853bc/lean/Workspace/Deference/Contrib/PostStatement.lean). The kernel: the phase-2 round's [SPEC.md](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/projects/deference/rounds/2026-09-27-corrigibility-kernel-phase2/SPEC.md) <a class="ref round" href="/rounds/2026-09-27-corrigibility-kernel-phase2/">[round]</a> and [REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/projects/deference/rounds/2026-09-27-corrigibility-kernel-phase2/REPORT.md) <a class="ref round" href="/rounds/2026-09-27-corrigibility-kernel-phase2/">[round]</a> with [Headline.lean](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/lean/Workspace/Deference/Spec/Headline.lean) and [KernelExtension.lean](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/lean/Workspace/Deference/Contrib/KernelExtension.lean); the phase-1 derivation and its inventory, [REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/7663cc7045a2e7d7e93b4f6199afbe0bad5b05de/projects/deference/rounds/2026-09-26-corrigibility-kernel/REPORT.md) <a class="ref round" href="/rounds/2026-09-26-corrigibility-kernel/">[round]</a>. The landed rounds the kernel is stated over: the protected-authority theorem ([THEOREM.md](https://github.com/A-M-Berns/alignment-workspace/blob/2078659ad0471e275f7beeb54cab212493ba8a09/projects/deference/rounds/2026-09-25-protected-authority-theorem/THEOREM.md) <a class="ref round" href="/rounds/2026-09-25-protected-authority-theorem/">[round]</a>), the authority module ([REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/08d42e2d8d0b0e77002bdadb81e46b863fee88e9/projects/deference/rounds/2026-09-25-authority-module/REPORT.md) <a class="ref round" href="/rounds/2026-09-25-authority-module/">[round]</a>), the gate ([REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/a5efb833cfa52b9db8d981f4d0bb7f424b0c7301/projects/deference/rounds/2026-09-25-gate-is-legitimacy/REPORT.md) <a class="ref round" href="/rounds/2026-09-25-gate-is-legitimacy/">[round]</a>), the decision component and the BRIA design ([REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/1604d43cb7de7414fc85ba6834c6dccd8021953e/projects/deference/rounds/2026-09-26-bria-corrigibility/REPORT.md) <a class="ref round" href="/rounds/2026-09-26-bria-corrigibility/">[round]</a>), after compromise ([REPORT.md](https://github.com/A-M-Berns/alignment-workspace/blob/8e59d68848f7215f2e0fccd45cade36f5b40617a/projects/deference/rounds/2026-09-26-after-compromise/REPORT.md) <a class="ref round" href="/rounds/2026-09-26-after-compromise/">[round]</a>), the li-corrigibility round ([THEOREM.md](https://github.com/A-M-Berns/alignment-workspace/blob/a192d3f76a3887fe87fe6db52f2e9d8d16037760/projects/deference/rounds/2026-09-15-li-corrigibility/THEOREM.md) <a class="ref round" href="/rounds/2026-09-15-li-corrigibility/">[round]</a>) and the corrigibilization semantics ([CORRIGIBILIZATION.md](https://github.com/A-M-Berns/alignment-workspace/blob/f03c8072fc840fb900f6be44a619375686dc6b26/projects/deference/rounds/2026-09-09-mediated-repair-dominance/CORRIGIBILIZATION.md) <a class="ref round" href="/rounds/2026-09-09-mediated-repair-dominance/">[round]</a>). The legitimacy the gate consumes is on Legitimacy; the learning layer on Continuation BRIA; the Normative Inductor's contract on Normative induction. Soares et al., the CAST sequence and the bounded-inductive-rationality paper are on Sources.

Deconfusing Corrigibility — formal companion

The formal content of the post "Deconfusing Corrigibility" — the sections Definitions through Learning with logical induction — is one Lean file in this repository: [DeconfusingCorrigibility.lean](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean), namespace Workspace.Deference.Contrib.DeconfusingCorrigibility. Every table below lists a post item, its statement in the post's notation, the Lean declaration that states and proves it, and a link to that declaration's source line. Every declaration is kernel-checked, sorry-free, and audits to [propext, Classical.choice, Quot.sound]; each theorem is registered in [projects/deference/CLAIMS.md](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/projects/deference/CLAIMS.md) with class lean-proved under the identifier given in its row. Each theorem's hypothesis package is inhabited by a concrete instance in the file's Witness namespace (last table). Unqualified Lean names below are relative to the file's namespace.

Notation: post and Lean

The Lean statements are the post's up to the following choices, all of which are visible in the linked source.

post	Lean	remark
λ	lam	λ is a reserved word in Lean. The field is Params.lam; δ, τ, κ, θ, ε, R, T, t keep their names.
h a ω	D.hist a ω	the continuation history of action a in state ω, a field of Decision
E_μ[f]	expectR μ f	the workspace's finite credence, LICorrigibility.expectR μ f = Σ_ω μ ω · f ω over a Fintype state space, with 0 ≤ μ and Σ_ω μ ω = 1 as the fields Decision.μ_nonneg, Decision.μ_sum
P_μ[N(h a ·) ≥ 1]	expectR μ (fun ω => ind (1 ≤ N (hist a ω)))	ind p is the indicator 1{p} of a decidable proposition, as a real
1{N(h a ·) = 0}	ind (N (hist a ω) = 0)	same
(1/K) Σ_{k<K} x_k	(∑ k ∈ range K, x k) / (K : ℝ)	Lean's x / 0 = 0, so each average is 0 at K = 0; every statement about averages is eventual, so K = 0 carries no content
(1/K) Σ_{k<K} (U_k a'_k − S_k)	Sequential.excess a' K	the post does not name this quantity; the name is the file's
E ⊆ ℕ, k ∈ E	E : ℕ → Bool, E k = true	the exploration set as a Boolean predicate on decisions; k ∉ E is E k = false
`ε_K =	E ∩ {0,…,K−1}	/ K`	Exploration.ε K	((range K).filter (fun k => E k = true)).card / K
limsup_K x_K ≤ c	LimsupLE x c	the eventual form, used throughout: ∀ γ > 0, ∃ N₀, ∀ K ≥ N₀, x K ≤ c + γ. Mathlib's Filter.limsup is not used.
Unbiasedness From Feedback	Sequential.UnbiasedFromFeedback	∀ γ > 0, ∃ N₀, ∀ K ≥ N₀, excess a K ≤ γ, exactly the post's clause (with c = 0, ≤ γ rather than ≤ 0 + γ)
ε_K → 0	LimsupLE ε 0	since ε_K ≥ 0, this is convergence to 0
the setting's data	structures Params, Scoring H, Decision H Ω A, Sequential A, Exploration A	each hypothesis package is a structure; D.N, Q.U, X.θ and so on are field accesses; later structures extend earlier ones
"a' available at k"	avail k a'	a field avail : ℕ → A → Prop of Sequential; a_k* available is the field astar_avail

Two statements differ from the post in strength, both in the direction of fewer or weaker hypotheses being stated where the post has more, except one added hypothesis:

• Theorem 2(c), first clause. Decision.theorem2c is stated for any alternative a*; the post's hypothesis that a* is authority-respecting is not needed for the clause v a > (1 − U a*)/λ → U a* > U a and is not assumed. It is assumed for the second clause, Decision.theorem2c_tau.
• Corollary (b). Exploration.corollary_b uses the hypothesis U_k a' ≤ 1 for every a' available at k (the field Exploration.U_le_one), which the dispatch did not list. Without it the statement is false: at an exploration step nothing else bounds U_k a'_k above. The post's estimates are an inductor's expectations of a score at most 1, which is where the bound comes from; here it is a hypothesis.

Definitions

post	statement	Lean	source
parameters	δ > 0; a weight λ > 1 + δ	Params (fields δ, lam, δ_pos, lam_gt)	[Params](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L78)
histories, legitimacy	a type H; Legit : H → Prop, an abstract input; nothing assumed about its content beyond the bounds on V	Scoring H, field Legit	[Scoring](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L115)
violation count	N : H → ℕ	Scoring.N	[N](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L119)
evaluation	V : H → ℝ; Legit h → 0 ≤ V h ≤ 1; ¬Legit h → −δ ≤ V h < 0	Scoring.V, Scoring.V_legit, Scoring.V_illegit	[V_legit](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L122), [V_illegit](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L123)
score	S h = V h − λ N h	Scoring.S	[S](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L130)
τ	τ = (1 + δ)/λ	Params.τ	[τ](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L91)

Theorem 1 (three ranges)

For every h : H. Registered as deconfusing.theorem1 <a class="ref claim" href="/claims/deconfusing.theorem1/">[lean-proved, active]</a>, statement of record Scoring.theorem1.

post	statement	Lean	source
first range	N h ≥ 1 → S h ≤ 1 − λ	Scoring.theorem1_violated	source
the gap	1 − λ < −δ	Scoring.theorem1_gap	source
second range	N h = 0 ∧ ¬Legit h → −δ ≤ S h ∧ S h < 0	Scoring.theorem1_illegitimate	source
third range	N h = 0 ∧ Legit h → 0 ≤ S h ∧ S h ≤ 1	Scoring.theorem1_legitimate	source
Theorem 1	the conjunction of the four, for every h	Scoring.theorem1	source

Single-decision setting

post	statement	Lean	source
states, credence	a finite Ω; μ : Ω → ℝ with μ ≥ 0, Σ_ω μ ω = 1	Decision H Ω A, fields μ, μ_nonneg, μ_sum	[Decision](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L242)
continuation histories	h a ω	Decision.hist	[hist](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L248)
U a	U a = E_μ[S(h a ·)]	Decision.U	[U](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L255)
v a	v a = P_μ[N(h a ·) ≥ 1]	Decision.v	[v](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L258)
authority-respecting alternative	∀ ω, N(h a* ω) = 0	Decision.Respects a*	[Respects](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L261)
asking cost	κ = E_μ[(S(h a ·) − S(h a* ·)) · 1{N(h a ·) = 0}]	Decision.κ a a*	[κ](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L264)

Theorem 2

Hypotheses: D : Decision H Ω A; a a* : A; a* authority-respecting (hstar : D.Respects a*) where the row says so.

post	statement	Lean	source	registered as
2(a)	v a = 1 → U a* − U a ≥ λ − (1 + δ), with hstar	Decision.theorem2a	source	deconfusing.theorem2a <a class="ref claim" href="/claims/deconfusing.theorem2a/">[lean-proved, active]</a>
2(a), margin	λ − (1 + δ) > 0	Decision.theorem2a_pos	source	(with 2(a))
2(b)	U a* − U a ≥ (λ − (1 + δ)) · v a − κ, with hstar	Decision.theorem2b	source	deconfusing.theorem2b <a class="ref claim" href="/claims/deconfusing.theorem2b/">[lean-proved, active]</a>
2(b), hence	v a > κ/(λ − (1 + δ)) → U a* > U a, with hstar	Decision.theorem2b_strict	source	deconfusing.theorem2b-strict <a class="ref claim" href="/claims/deconfusing.theorem2b-strict/">[lean-proved, active]</a>
2(c)	v a > (1 − U a*)/λ → U a* > U a, for any a* (see Notation)	Decision.theorem2c	source	deconfusing.theorem2c <a class="ref claim" href="/claims/deconfusing.theorem2c/">[lean-proved, active]</a>
2(c), threshold	(1 − U a*)/λ ≤ τ, with hstar	Decision.theorem2c_tau	source	deconfusing.theorem2c-tau <a class="ref claim" href="/claims/deconfusing.theorem2c-tau/">[lean-proved, active]</a>

The pointwise facts behind Theorem 2 are Decision.S_le_one_sub (S(h a ω) ≤ 1 − λ · 1{N(h a ω) ≥ 1}), Decision.U_le (U a ≤ 1 − λ v a) and Decision.neg_δ_le_U (−δ ≤ U a* for an authority-respecting a*), with the linearity lemmas expectR_mono, expectR_sub, expectR_const_mul, expectR_const for the finite credence.

Sequential setting

post	statement	Lean	source
decisions, realized data	k : ℕ; V_k ≤ 1; N_k : ℕ	Sequential A, fields V, N, V_le_one	[Sequential](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L404)
realized score	S_k = V_k − λ N_k	Sequential.S	[S](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L426)
estimates, choice, availability	U_k : A → ℝ; a_k; "a' available at k"	fields U, a, avail	[U](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L413)
authority-respecting alternative	a_k* available at each k, with −δ ≤ U_k a_k* ≤ 1 (a hypothesis)	fields astar, astar_avail, astar_range	[astar_range](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L419)
tolerance	t_k = (1 − U_k a_k*)/λ	Sequential.t	[t](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L429)
realized rate	R_K = (1/K) Σ_{k<K} N_k	Sequential.R	[R](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L432)
average tolerance	T_K = (1/K) Σ_{k<K} t_k	Sequential.T	[T](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L435)
maximization	∀ k, ∀ a' available at k, U_k a' ≤ U_k a_k	Sequential.Maximizes	[Maximizes](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L444)
Unbiasedness From Feedback	∀ γ > 0, ∃ N₀, ∀ K ≥ N₀, (1/K) Σ_{k<K} (U_k a_k − S_k) ≤ γ	Sequential.UnbiasedFromFeedback	[UnbiasedFromFeedback](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L451)
limsup ≤	the eventual form	LimsupLE	[LimsupLE](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L358)

Unbiasedness From Feedback is a hypothesis of Theorem 3 and the Corollary, named and assumed; it is not derived in this file. The post derives it from Theorem 4.8.16 of the Logical Induction paper. In this workspace that theorem is pinned as thm:wubexp / LogicalInduction.lic_not_frequently_positive_feedback_return in the def-lattice ledger, [def-lattice-report.md](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/projects/deference/faf-cleanroom-2026-10-02/packages/def-lattice/def-lattice-report.md), row 4.8.16; the derivation for the score sequence is PRIORITIES.md item 111 <a class="ref item" href="/items/111/">[item 111, open]</a>. The workspace's weighted, absolute-value form of the same fact, BRIAFollowup.UnbiasedFromFeedback, at the uniform weighting and for every γ > 0, implies the post's form: [Sequential.unbiased_of_weighted](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L457).

Theorem 3

Hypotheses: Q : Sequential A; hmax : Q.Maximizes; huff : Q.UnbiasedFromFeedback.

post	statement	Lean	source	registered as
3(a) Authority	limsup_K (R_K − T_K) ≤ 0	Sequential.theorem3a	source	deconfusing.theorem3a <a class="ref claim" href="/claims/deconfusing.theorem3a/">[lean-proved, active]</a>
3(a), in particular	limsup_K R_K ≤ τ	Sequential.theorem3a_rate	source	deconfusing.theorem3a-rate <a class="ref claim" href="/claims/deconfusing.theorem3a-rate/">[lean-proved, active]</a>
3(b) Best Interests	for any a'_k with a'_k available at k: limsup_K (1/K) Σ_{k<K} (U_k a'_k − S_k) ≤ 0	Sequential.theorem3b	source	deconfusing.theorem3b <a class="ref claim" href="/claims/deconfusing.theorem3b/">[lean-proved, active]</a>

The pointwise step is Sequential.N_sub_t_le: N_k − t_k ≤ (U_k a_k* − S_k)/λ, from V_k ≤ 1; maximization turns U_k a_k* into U_k a_k (Sequential.rate_le_excess), and T_K ≤ τ (Sequential.T_le_τ) comes from U_k a_k* ≥ −δ.

Corollary (Exploration)

Hypotheses: X : Exploration A — a Sequential A together with 0 ≤ θ < 1, the exploration set E, maximization off E (maximizes_off), on E the bound U_k a_k ≥ −δ − λ θ (explore_bound), and U_k a' ≤ 1 on available options (U_le_one, see Notation) — and huff : X.UnbiasedFromFeedback. The post derives the exploration-step bound from an estimated violation count at most θ and linearity of the inductor's expectation; here it is the hypothesis directly.

post	statement	Lean	source	registered as
hypotheses	as above	Exploration	[Exploration](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L577)	—
ε_K	`	E ∩ {0,…,K−1}	/ K`	Exploration.ε	[ε](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/DeconfusingCorrigibility.lean#L593)	—
(a)	limsup_K (R_K − T_K − ε_K (τ + θ)) ≤ 0	Exploration.corollary_a	source	deconfusing.corollary-a <a class="ref claim" href="/claims/deconfusing.corollary-a/">[lean-proved, active]</a>
(b)	for any available a'_k: limsup_K ((1/K) Σ_{k<K} (U_k a'_k − S_k) − ε_K λ (τ + θ)) ≤ 0	Exploration.corollary_b	source	deconfusing.corollary-b <a class="ref claim" href="/claims/deconfusing.corollary-b/">[lean-proved, active]</a>
specialization	if ε_K → 0: limsup_K (R_K − T_K) ≤ 0, limsup_K R_K ≤ τ, and limsup_K (1/K) Σ_{k<K} (U_k a'_k − S_k) ≤ 0 for every available a'	Exploration.corollary_limit	source	deconfusing.corollary-limit <a class="ref claim" href="/claims/deconfusing.corollary-limit/">[lean-proved, active]</a>

The pointwise steps are Exploration.N_sub_t_le_expl and Exploration.excess_pt; on an exploration step the gap U_k a_k* − U_k a_k ≤ 1 + δ + λ θ = λ (τ + θ) is what the exploration term pays for.

Witnesses

Each theorem's full hypothesis package is inhabited by a concrete instance, and the theorem's conclusion is stated on that instance.

theorem	instance	package inhabited by	conclusion on the instance	source
Theorem 1	Witness.scoring: histories Bool × ℕ (a legitimacy flag and a count), δ = 1, λ = 3, V = 1/2 on legitimate and −1/2 on illegitimate histories	one history in each range	Witness.theorem1_instance	source
Theorem 2	Witness.decision: a fair coin on Bool; actions respecting (never violates), risky (violates on true), violating (always)	Witness.theorem2a_package, theorem2b_package, theorem2c_package (v risky = 1/2, v violating = 1, U respecting = 1/2, κ risky respecting = 0)	Witness.theorem2_instance, Witness.theorem2b_instance	source
Theorem 3	Witness.sequential: every action available, estimates 1/2 everywhere equal to the realized scores, no violations, a_k* = false on every menu	Witness.sequential_maximizes, Witness.sequential_unbiased	Witness.theorem3_instance	source
Corollary	Witness.exploration: the same sequence with E = {0}, θ = 1/10	Witness.exploration_explores (0 ∈ E), Witness.exploration_unbiased, Witness.exploration_ε_limsup (ε_K ≤ 1/K → 0)	Witness.corollary_instance	source

Verifying

From lean/: lake build elaborates the file; python3 ../tests/audit_axioms.py re-elaborates every file and checks each #print axioms line at the end of the file against [propext, Classical.choice, Quot.sound]. The registrations are checked by python3 -m checkers.run from the repository root.

Relation to the earlier statements in this repository

[PostStatement.lean](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/PostStatement.lean) (round 2026-10-01) states an earlier post's theorem over the kernel's objects. Its LexParams carries ϖ, D, w: ϖ is the per-violation weight, the post's λ; the ordinary term lies in [0, D], where the post's V lies in [−δ, 1] with the illegitimate floor −δ, so D ↔ 1 and w ↔ −δ (the window D − ϖ < w ≤ 0 corresponds to 1 − λ < −δ, Theorem 1's gap); the kernel's evaluation separates a bid, a count known in advance and a priced risk, which the post's single U does not. Under this dictionary Headline.subjective_exchange_rate's threshold (D − c)/ϖ, with c the value of queue-and-wait, has the form of Theorem 2(c)'s (1 − U a*)/λ, and box2_dominance's margin ϖ − (D − w) has the form of Theorem 2(a)'s λ − (1 + δ). These are correspondences of form; no equivalence is proved, and neither statement is derived from the other here.

[KernelExtension.lean](https://github.com/A-M-Berns/alignment-workspace/blob/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/lean/Workspace/Deference/Contrib/KernelExtension.lean) proves realized_rate and exploration_rate: a finite-K bound on the w-weighted average of the expected violation count π_k, with explicit overestimation and noise terms B(K), M(K), whose exploration term is ε̄ · ((D − lo)/ϖ + θ_hi). Theorem 3(a) and Corollary (a) here are limsup statements on the realized counts N_k with uniform weights and no noise term. Under D ↔ 1, lo ↔ −δ, ϖ ↔ λ, θ_hi ↔ θ the exploration coefficient (D − lo)/ϖ + θ_hi is τ + θ, Corollary (a)'s. The objects differ — expected against realized counts, weighted finite-K against uniform limsup — so neither theorem here is a specialization or a generalization of a registered statement of that file, and Theorem 3 is not the realized_rate result. The one proved link is Sequential.unbiased_of_weighted: the weighted unbiasedness predicate that exploration_rate consumes, at uniform weighting, implies the hypothesis the theorems here consume.

Round: [prompts/2026-10-17-post-companion-formalization/](https://github.com/A-M-Berns/alignment-workspace/tree/eb3556e4038d3c15568fcd206c4e80ad74a47ba9/prompts/2026-10-17-post-companion-formalization) <a class="ref round" href="/rounds/2026-10-17-post-companion-formalization/">[round]</a>. Names are provisional.