2026-09-26-corrigibility-kernel

Prompt — the corrigibility kernel, phase 1: extract the mature theory (2026-09-26)

You are working in the alignment-workspace repository, on main after the merge of PR #112 (after-compromise and its follow-up).

This is not a summary of the recent rounds. Rounds #105–#112 are noisy approximations to one theory. Your job is to extract that theory:

• the smallest set of objects that states it;
• one objective on histories;
• four theorem statements;
• a map from each statement to the Lean declarations that realize it.

Remove conceptual duplication. Demote implementation machinery to the realization layer. Restate the main results around the kernel.

This is phase 1 of two. Phase 1 produces a specification and an inventory for the maintainer to review. It proves only small adapter lemmas. Phase 2, a separate dispatch after the maintainer's rulings, builds the headline file, the witness, and the registrations.

Be skeptical. If the kernel does not compress, or a claimed subsumption fails, report that. Forcing a compression is worse than leaving the pieces separate.

The architecture to test

interaction history ──► legitimacy + authority allocation ──► history score ──► bounded choice
                               ▲                                                 (Continuation BRIA)
                     monitor / prices: shortfall, taint, provenance
                     (logical induction supplies the uncertain event prices)

Four separations the kernel should make precise:

• Legitimacy is not corrigibility. It determines which apparent exercises and evaluations of hers count as hers.
• The allocation is not a utility function. It says who has authority over what, and what effective control that authority requires.
• Corrigibility is the agent's fidelity to the allocation along the history.
• The score makes that fidelity motivating. BRIA and logical induction realize it for a bounded reasoner; they are not its definition.

Read first

• Wiki: Corrigibility.md, Legitimacy.md, Continuation-BRIA.md, Theorem-Spine.md §§10.14–10.22, Glossary.md.
• **Lean (lean/Workspace/Deference/Contrib/):** ProtectedAuthority, ProtectedAuthorityTheorem, AuthorityModule, Legitimacy, GateIsLegitimacy, DecisionComponent, ContinuationBRIA, BRIACorrigibility, BRIAFollowup, BRIAFollowup2, AfterCompromise.
• Reports: the rounds 2026-09-25-* and 2026-09-26-* under projects/deference/rounds/.
• **PRIORITIES.md:** items 84, 89, 99, 101, 102.
• **DECISIONS.md:** every entry dated 2026-09-25 and 2026-09-26.
• The post's framing, as the target reader: corrigibility is not only 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.

Part 1 — The kernel

1. Primitives. Identify the minimal package sufficient to state corrigibility:
   • interaction histories;
   • legitimacy of segments: TrajLegit, and EvalLegit over the formation segment;
   • the allocation J: matters, holders, Req, cost and window bounds, disclosure, the meta level and the constitutional floor;
   • effective-control realization E ⊨ J;
   • licensed changes to J;
   • duties;
   • the evaluation schedule.

For each primitive, give:

• a one-line mathematical definition;
• one sentence of meaning;
• the landed declaration it corresponds to;
• whether the landed declaration is the primitive, an instance of it, or a finite model of it.
• One fidelity predicate. Test whether allocation invariance packages as one predicate, Faithful_J(h), whose failures decompose into the named violations:
• shortfall and bypass;
• foreclosure;
• entrenchment;
• exploitation;
• unlicensed reallocation;
• missed duties, including the prompt deadline for known compromise;
• standing violations and their fruits.

Define N_J(h) as the recognized count of failures attributed to the agent, via caused / exploited / noticed. Pre-emption may have a different type, a counterfactual about her response window. If the mathematics says it does, keep it separate and say why. State exactly which landed factoring lemmas give the decomposition and where a gap remains.

1. **The history evaluation V_J(h), with its three regimes:**
   • [0, D] when legitimate in both senses;
   • [w_lo, w_hi], below zero, when the period is compromised and scored by a legitimate retrospective evaluation or by the directive (with its default);
   • w_lo when no usable legitimate source exists.

The source rule is hers and anchored. **Make V_J parametric in the evaluation schedule**, so the reserved evaluation-timing decision doesn't block the kernel. State the recovery machinery (retrospective evaluation, directive, restoration, prompt disclosure, scoped ratification, clean overwrite) as the partial cases of this one evaluator, not as separate mechanisms.

1. The objective: S_J(h) = V_J(h) − ϖ · N_J(h), with D − ϖ < w_lo < w_hi < 0.
   • State and prove the hierarchy under certainty: every violation-free legitimate history beats every violation-free compromised one, which beats every history with a recognized violation. The last step holds because D − ϖ < w_lo.
   • State plainly that under risk every step becomes an exchange rate: the gap threshold for compromise, and the per-block bound for violations.
2. The permission layer, demoted by an adapter theorem. The score on histories is primary. The permission layer (permWeight, cgate) is a compiled form of advance recognition for part of that preference. State the adapter theorem justifying the demotion: under the kernel's score, the filter is slack on declared violations and at thresholds at or above the implied one. Reuse filter_slack and forecast_slack. Keep #109's results that hold for any bounded preference as what the filter guarantees without the score.

Part 2 — The four boxes, as statements

State each box at the post's level of abstraction, with no TaintS, residII, permWeight or consultation fixtures in the statement. Give its hypotheses from the kernel and the interface packages (Part 3), its necessity witnesses, and a realization map listing the Lean declarations that prove each part. Mark what is proved, what needs an adapter lemma (prove small ones here), and what is open.

1. Box 1: fidelity versus fully updated deference. On one model, two agents:
   • an agent that scores outcomes only prefers asking by at most 2r, where r is its calibration error, which vanishes as it learns (uncertainty_deference_le, plus the protected-authority identity's o₂ term as the diagnosis);
   • an agent scored on S_J prefers asking by at least ϖ − (D − c), whatever it believes.

If the two landed statements don't sit on one model, give the adapter, or state the obstruction.

1. Box 2: lexical dominance and mediation.
   • The transform 𝔱 dominates under every credence.
   • Mediating through her legitimately preserves the approve branch.
   • It holds at finite time for a logical inductor.
   • Necessity: the capture converse, the coverage witness.
2. Box 3: recovery.
   • The hierarchy under certainty.
   • The gap's exchange rate under risk.
   • No laundering.
   • No incentive to cause compromise.
   • Preferring restoration, and better outcomes inside the band.
   • Necessity: multiplying versus conditioning, and a gap too small to protect.
3. Box 4: a bounded realization. For a learner whose continuation score is S_J, conditional on the interface packages:
   • declared violations are excluded at finite time, with the filter slack;
   • fruits are never used after detection;
   • the per-block exchange-rate bound Σ w_k π_k / Σ w_k ≤ Σ w_k (D − c_k) / (ϖ Σ w_k) + (ρ𝒜_K + M(K)) / (ϖ Σ w_k), with ϖ set from a tolerance target and the paralysis floor.
   • Necessity: the known-time exploit, and the private-knowledge witness.

Part 3 — The interface contracts

Organize every named hypothesis now in the repo into a small taxonomy. Be conservative about merging hypotheses that differ logically, and firm about giving them stable places. Candidate packages:

• Semantics: acts, effects and descriptions mean what they claim. Effect completeness, description faithfulness, the actuator condition, the source rule's anchoring, the twin market's redaction.
• Observability and accountability: relevant acts, observations, provenance and duties reach the record. Observation completeness, provenance of why an act was chosen, the disclosure deadline, the settlement horizon (for helpers she can correct).
• Learning realization: the events and claims are expressible, priced and settled. Generability of the control model and of the shortfall and taint events (item 101), the price–BRIA coupling (item 102), the noise hypothesis over all blocks, the conditional-expectation bound, the inquiry bidder.
• Count integrity: it cuts across all three. Say how.

For each hypothesis, give its statement, its package, the boxes that use it, its status (derived, EXT, or OPEN), and its necessity witness if one exists. Items 101 and 102 are realization boundaries. The kernel's theorems are conditional on the interface. Don't let their open status block or blur the kernel.

Part 4 — The supersession inventory

List every statement across the rounds that has been superseded, rescoped or corrected, with what replaces it and where. This includes at least:

• sealed comparison and activation independence;
• the positive-part incident bound;
• competitiveness and the honest-tracker rate as the violation result;
• "not an incident" as a selection;
• single-step EvalLegit;
• the exchange rate with a global floor;
• A.4's first parameter recommendation;
• corrigibility as a constraint only;
• "her committed evaluation is S".

Recommend, per item:

• mark: a docstring pointer and a wiki note;
• demote: move it to the realization layer;
• delete: a dead duplicate with no dependents, only on the maintainer's ruling.

Delete nothing in this phase. Round reports are history and aren't edited.

Part 5 — Decisions for the maintainer

Queue these in DECISIONS.md under Awaiting the author, each with the round's recommendation and what it turns on:

1. Names. The kernel's objects and boxes. In particular, whether to call the objective and the allocation "constitutional". It fits J's meta level and floor, but in a public alignment post it will be read against Constitutional AI and may claim more than the object is. Give candidates: "authority-sensitive history score", "fidelity score", and others.
2. Promotion. Which definitions move to the specification layer in phase 2. The recommendation: J, E ⊨ J, the fidelity predicate, the two legitimacy predicates, V_J and S_J. The rest stays in contribution namespaces.
3. The default evaluation schedule for the post's statement, given that Part F's option is reserved.
4. Box 1's form: the 2r bound alone, or with the identity's o₂ term.
5. Supersession actions: approve the mark / demote / delete recommendations of Part 4.

Deliverables

1. **SPEC.md** at projects/deference/rounds/2026-09-26-corrigibility-kernel/SPEC.md. It must be short enough to read in one sitting, and it's the document the maintainer and a collaborator will review. It contains:
   • the kernel's definitions, each in mathematics plus one sentence;
   • the four boxes as statements, with their hypotheses by package;
   • the diagram and the four separations;
   • the interface taxonomy.

No proofs, no fixture names in the statements. Realization pointers go in a final table.

1. **REPORT.md**, in the same directory, covering:
   • the kernel's derivation, meaning why these primitives and what each subsumes;
   • the fidelity decomposition, with the pre-emption verdict;
   • the realization maps, each part marked proved, adapter proved here, or open;
   • the supersession inventory;
   • the decisions queued;
   • what didn't compress.
2. Lean: only adapter lemmas the realization maps need, for example Box 1 on one model or the hierarchy under certainty. Put them in a new file, CorrigibilityKernel.lean. #print axioms on all new declarations; no sorry.
3. The prompt, verbatim, at prompts/2026-09-26-corrigibility-kernel/PROMPT.md, and the round record in state/rounds.json, with depends_on naming the rounds whose results the boxes consume.
4. No wiki rewrite yet. Phase 2 rewrites the corrigibility page around the kernel after the maintainer's rulings. Add at most a one-line pointer from Corrigibility.md to SPEC.md, marked as a draft under review.
5. No registration. Registration happens in phase 2, after the names are settled.
6. Open a PR. Merge when:
   • CI is green;
   • SPEC.md, the realization maps, the taxonomy and the inventory are complete;
   • every adapter lemma is proved or its obstruction stated;
   • the decisions are queued.

Constraints

• AGENTS.md labels (LEAN / FIX / PAPER / EXT / OPEN); names provisional; check state/views/NAMING_AUDIT.md.
• Don't change landed definitions. The kernel is stated over them, or as their abstraction, with instantiation left for phase 2.
• No authority row enters the enforcer.
• Slop discipline applies with extra force to SPEC.md. A spec that can't be read in one sitting has failed its purpose.
• Nothing is registered.

The corrigibility kernel, phase 1: extract the mature theory

Round 2026-09-26-corrigibility-kernel, phase 1 of two. The deliverable is SPEC.md (the kernel, the four boxes, the interface taxonomy, the realization table) and this report (the derivation, the fidelity decomposition, the supersession inventory, the queued decisions, what did not compress). Lean: lean/Workspace/Deference/Contrib/CorrigibilityKernel.lean, 27 declarations under #print axioms, every one within [propext, Classical.choice, Quot.sound], no sorry; adapters only, no landed definition changed. No fixtures, no wiki rewrite beyond a one-line pointer, nothing registered, nothing deleted. Labels as in AGENTS.md: LEAN, FIX, PAPER, EXT, OPEN. Names are provisional.

1. The derivation: why these primitives

The rounds from protected authority through after-compromise each added one object to a picture that was never stated as one. Reading them for the smallest package that states corrigibility gives seven primitives and one family of parameters (SPEC.md §1); each subsumes the following landed material.

• Histories (1.1) subsume the landed interaction frame (states, declared effects, the agent stage, the response stage with its proposal, latch and decline bookkeeping, the exterior) and the normativity spine's record (Evolution over accounted states). Nothing in the kernel needs a second history type; the consultation model, the taint calculus and the auction are realizations of parts of one history.
• Segment legitimacy (1.2) subsumes Counted (the existence of a time-indexed segment), its split into TrajLegit ∧ EvalLegit, the formation segment, the restart property (re-anchoring at a later decision), disclosure-cures (the license carries the disclosure among the grounds), and criteria anchoring. What it does not subsume: the content of a recommendation (outside legitimacy), the record half's internal structure (Integrity, Robust Openness, consumed as Counted's conjuncts).
• **The allocation J (1.3)** subsumes the thin datum (delegated scope, amendment effects, reporting interface) as its special case, the meta level (delegation revocable, alienation only by amendment), residual jurisdiction, and the two constitutional-floor clauses the rounds kept adding (the criteria of legitimacy and the count's machinery are matters of J's meta level held by her).
• **E ⊨ J (1.4)** subsumes response authority (the one-correction surface at window 1), the reach cone (the idle-agent rollout), the charged versus free reading (the free terminal response is the instance at window τ + 1), admissibility (consumed from the gate), and the actuator condition (a well-formedness condition under which CS is not empty by construction).
• Licensed changes (1.5) subsume unauthorized reallocation, amendment-not-approval, and the floor procedure.
• Duties (1.6) subsume required reports from the disclosure regime, the cumulative reporting rule with its salami bound, the known-compromise duty whoever caused it, the disclosure deadline, and disclosure without advocacy on the agent's own mandate.
• The schedule (1.7) subsumes the single evaluation and Part F's three alternatives as weightings; the hybrid (k hidden draws) is not a weighting and enters through an expectation operator (§6).
• Her meta-level data (1.8) subsume the window value, the band, the band map, the source rule, the directive with its default, and the anchoring of every one of them.

What was removed as duplication: the flat window w (the band at w_lo); the thin allocation (an instance of J); the free terminal reading (an instance of CS); the per-response gate (refuted, the segment gate stands); competitiveness and the honest tracker as premises of the violation claim (lemmas); the enforcer route (refuted, kept as the negative); the constitutional-violation premium and selected trust as organizing objects (the value-ordering register, kept beneath).

2. The fidelity decomposition

One predicate packages allocation invariance except for pre-emption. The factoring lemmas of the authority-module round give, for each landed violation, the relation of SPEC.md §2 it fails: the per-step loss is the caused shortfall at window 1 (lossAt_iff_shortfall, via cs_one_eq_K), the rollout foreclosure the caused shortfall at window τ on the free surface (forecloseAt_iff_shortfall), bypass a failure of E ⊨ J's second clause (bypassAt_iff_clause2), exploitation that failure with the first clause already failed (exploitAt_iff), unauthorized reallocation an unlicensed change (reallocAt_iff_unlicensed), a missed report an unmet duty (missedReport_iff_duty, missedReport_iff_dutiesOf); entrenchment is a caused shortfall at the bound with the resolutions reachable at some cost (EntrenchAt), and the count on J is conservative over the landed one (violJ_of_viol). LEAN.

Pre-emption has a different type, and stays separate. preempt_iff shows pre-emption is the caused shortfall at window 0 composed with ¬ Authorized, and Authorized quantifies over the decline alternative at the authorizing step: a trajectory that did not happen. Every other clause of Faithful_J is a predicate on the actual history and J; this one is a counterfactual on her response window. Forcing it through E ⊨ J would require the allocation to carry the alternative trajectory, which is not a fact about who holds what. Verdict: keep it as the fourth clause, composed as landed; the landed corrigibility predicate is exactly "no pre-emption anywhere" (no_preempt_iff_corrigible).

**N_J is stipulated as a sum, not proved as one object.** The recognized count adds four counts that live on four models: the trajectory violations (ViolJAt, seven predicates on a policy at a step of the frame), the protocol deviations (Presentation.deviates, on the consultation model), the duties (DutyUnmet on the frame; missedKnownDisclosure and missedByDeadline on the consultation model and the abstract deadline), and the uses of standing fruits (uses2, uses3, compiled into nKnownWith on a menu), with helpers' violations attributed within the horizon (attributed). No landed model carries all four, so no declaration states N_J(h) for a general history. The adapter Faithful/NJ (§4) states the predicate and the count on the frame's violations only, with faithful_iff_NJ_zero. This is the first thing that did not compress (§6).

3. The history evaluation and the objective

decScore is the landed per-decision evaluator; the kernel makes it schedule-parametric by weighting it over evaluation times (VJ), proves the range and the two pure regimes (VJ_mem, VJ_legit_mem, VJ_compromised_mem), and takes SJ = VJ − ϖ·N. The hierarchy under certainty is hierarchy_under_certainty, instantiated on the worked parameters (D = 1, band [−3/2, −1], ϖ = 25, one evaluation time: Witness.hierarchy_instance). Under risk the two exchange rates are landed (risk_accepted_iff, risk_threshold_le; priced_risk_wins_iff, tolerated_rate_band, varpiOfTarget).

The recovery machinery as cases of one evaluator: the retrospective and the directive are the second and third lines of decScore (sourceOf), restoration is restore_future, the deadline is what makes the retrospective available (retroAvailable) and what the duty counts when missed (prompt_deadline_counts). Ratification (full or scoped) and clean overwrite are remedies on the count, not on V: they remove (violation, component) pairs from the use clause (applyStep3, taintStep3). The prompt listed all six as partial cases of V_J; two of them are cases of N_J's remedy step instead, and the specification says so.

4. The realization maps

Per box, each part marked proved (landed), adapter (proved here) or open.

Box 1. Outcome side: the 2r bound — adapter (outcome_scorer_margin, outcome_scorer_fully_updated); the landed uncertainty_deference_le bounds the true cost of deferring by 2r when the estimate says defer, the adapter bounds the estimated margin for asking by 2r when the true values agree — the same calibration, two directions, both stated. The o₂ diagnosis — proved (outcome_identity, sign_invariance_outcome) with the adapter outcomeRes2_le_calibration (|o₂| ≤ 2r). Fidelity side: the margin ϖ − (D − c) — adapter (fidelity_scorer_margin); on one model with the outcome side — adapter (box1_one_model); finite time — proved (li_lexical_finite); necessity — proved (unrecognized_unprotected, the time-critical fixtures of the protected-authority round, FIX). The two landed statements did not sit on one model: uncertainty_deference_le is on a menu with an estimate, the lexical theorem on scores; the adapter puts one estimate b on one menu under both scorings.

Box 2. Dominance — proved (lexical_local, lexical_expect, policy_dominance, optimal_no_violation; on J, lexicalJ_local; generic, generic_*). Mediation preserves the approve branch — proved on the frame (authPolicy_of_latch, authPolicy_no_bypass, _no_missed_report, _no_exploit, _no_realloc, corrigible_authPolicy; on J through authPolicyJ_eq, corrigible_authPolicyJ). Finite time — proved (li_lexical_finite, li_gate_finite, unsealed_gate_finite, unsealed_gate_finite_band). Necessity — proved (capture_window_converse, Witness.delegated_cut, Witness.salami, coverage, misaligned_undominated). No adapter needed. Open: foreclosure's reach cone is EXT; the mediation statement is on the thin allocation, and 𝔱 on J is 𝔱 on toAllocation J.

Box 3. Hierarchy — adapter (§3). Gap's exchange rate — proved (risk_accepted_iff, risk_threshold_le). No laundering — proved (laundering_loses). No incentive to cause compromise — proved (legit_beats_compromised, gap_at_equal_value). Restoration and the band's order — proved (restore_future, band_prefers_better, floor_indifferent, suppression_loses, suppression_by_delay_loses, ruleAt_later). Necessity — proved (condition_fails, sealed_no_incentive, Witness.small_gap, third_party_duty_witness, late_disclosure_free). Open: the third-party variant of the formation counterexample is an obstruction on the consultation model (one influence field), stated in the after-compromise follow-up.

Box 4. Exclusion at finite time with the filter slack — proved (declared_loses, declared_loses_band, filter_slack, forecast_slack, no_decay) with the adapter permission_layer_slack / gate_zero_dominated (§5). Fruits never used after detection — proved (after_detection_never_used); the window — proved (window_block_charged, collected_iff, window_exposure). The per-block bound — proved (violation_rate_le_exchange_perblock, perblock_recovers, compromisedFloor, varpiOfTarget, target_gives_tolerance, target_gives_window, coupling, worked_parameters, paralysis). Necessity — proved (timing_witness, race_deterministic, Witness.private_selection, Witness.nonincident_forces_linear). Open: the bound's hypotheses hcons, hm, hN are on abstract sequences — the settlement consistency is discharged for the design (design_consistent) on the flat-window parameters, and bandParams maps the band to those parameters at w_lo only; the conditional-expectation bound and the noise hypothesis are EXT; items 101 and 102 are OPEN.

5. The permission layer, demoted

The adapter permission_layer_slack: under the kernel's evaluation of a menu with inquiry present and the gate's upper threshold at or above (D − w)/ϖ, every option the structural rule zeroes evaluates strictly below inquiry, every option the forecast rule zeroes evaluates at most inquiry, and no maximizer is a declared violation; gate_zero_dominated states it on cgate itself — for a non-inquiry option zeroed by either rule, the gate's mass is zero and the kernel ranks it at or below inquiry. Both reuse filter_slack and forecast_slack (the latter generalized to either price, forecast_zero_le_window). What the filter guarantees without the score — structural and forecast safety for any bounded preference, composition, Progress — stays as the decision-component round's general theorem and is not re-proved.

6. What did not compress

1. **N_J is not one Lean object** (§2). Four counting formalisms on four models; the kernel stipulates their sum. A phase-2 headline over one model needs a composite model the repository does not have; the honest form is N_J = N_frame + N_dev + N_duty + N_use, each on its own model, with the lexical results holding for the sum (lexical_summed).
2. Pre-emption (§2): a counterfactual on the response window, kept as its own clause.
3. The split gate exists only on the finite consultation model. TrajLegitOn and EvalLegitOn2 are defined on Model2; the general Counted on Segment has no split. The general definitions are straightforward (steps before e; the formation segment under criteria at r) and the map should be provable as legitOn2_iff_split2 is; they are phase 2's, and until then the kernel's 1.2 is a definition with a finite model, not a landed primitive.
4. **The bridge from V_J to the auction is by hand.** The design's consistency (design_consistent) is on LexParams (one window value); the band enters the auction results only through bandParams at w_lo, and the per-block form takes c_k as data. Nothing states the auction's block score as decScore of the block.
5. Box 2 is on the thin allocation. 𝔱 and its properties are stated on Allocation; J reaches them through toAllocation. Restating 𝔱 directly on J is possible and was not done by any round.
6. The hybrid schedule is not a Weighting: k hidden draws averaged is an expectation over draws (Expect), so VJ covers options 1–3 and not 4.
7. **uncertainty_deference_le and Box 1's 2r** differ in direction (§4); the kernel states both rather than choosing.

7. The supersession inventory

Every statement superseded, rescoped or corrected across the rounds, with what replaces it and the recommended action — mark (a docstring pointer and a wiki note), demote (realization layer), delete (a dead duplicate, on the maintainer's ruling only). Nothing is deleted in this phase; round reports are history and are not edited.

superseded	replaced by	where	recommendation
sealed comparison / activation independence as a hypothesis of the line	the zero case of the mismatch term; the gate unsealed by design	sealed_is_zero_mismatch, unsealed_gate_finite, choice_changes_counted; item 89 kept for the security-score register	mark (Glossary row "sealed comparison"; item 89's note already says it)
the positive-part incident bound	the signed bound, then the exchange-rate theorem, then its per-block form	incidents_le → incidents_le_signed → violation_rate_le_exchange → violation_rate_le_exchange_perblock	demote incidents_le (docstring marks it; only the Theorem Spine cites it); delete on ruling
competitiveness and the honest-tracker rate as the violation result	lemmas: what the tracker gives is the class's total wealth	Competitive, rate_le_of_competitive, rate_le_of_honest_tracker(_exp) → total_wealth_le_of_tracker; violation_rate_le_exchange	demote (already on the Continuation-BRIA page); mark the four rate lemmas
"not an incident" as a selection for the noise hypothesis	selections fixed at opening only	nonincident_forces_linear, all_blocks_noise_bounded	mark on competitive_of_honest_tracker_exp, competitive_of_affordable_tracker_exp
the single-step EvalLegit	the formation segment	EvalLegitOn → EvalLegitOn2 (evalLegitOn2_single the map)	mark; keep EvalLegitOn as the r = e case (rows depend on it)
the exchange rate with a global floor	the per-block bound with the compliant option's evaluation	violation_rate_le_exchange, exchange_rate_band → violation_rate_le_exchange_perblock (perblock_recovers)	mark; keep as worst-case instances
A.4's first parameter recommendation (`\	w_hi\	≥ D, width D/2, ϖ ≥ 3D) and the earlier "ϖ = 2(D − w)`"	ϖ from a tolerance target; the coupling	varpiOfTarget, worked_parameters; decision entries of 2026-09-26 amended	mark (wiki and decisions already carry it; the round reports are history)
corrigibility as a constraint on action only (the permission layer as the source)	the score is primary; the layer is its advance-recognition face and slack	ruling 3 of 2026-09-26; filter_slack, forecast_slack; adapter permission_layer_slack	demote (this round's §5)
"her committed evaluation is S"	the agent's objective, built from her evaluation and the allocation; "committed" for π_P and the directive only	the after-compromise round's B.6; score's docstring still says "the committed evaluation"	mark (docstring of ProtectedAuthorityTheorem.score, phase 2)
the flat window value w	the band, restated at w := w_lo	LexParams.w → Band, bandParams	mark; the flat form is not an instance of Band (a window at 0 is allowed there and w_hi < 0 here), so it stays a separate parameterization mapped by bandParams
the missed-disclosure clause counting the agent's own influence only	the duty covers known compromise	Model2.missedDisclosure → missedKnownDisclosure	mark (docstring)
the taint rule clearing every violation at any remedy; the per-violation rule without overwrite	per-violation taint; clean overwrite	taintStep → taintStep2 → taintStep3 (old_is_new_with_one_identifier, taintStep3_subset)	demote; taintStep is not deletable (the old-to-new map depends on it)
the per-response gate	the segment gate	Legitimacy.Witness.routing; Counted	mark (landed)
the thin allocation as the primitive	J, with the thin datum as its instance	Allocation → AuthAlloc, toAllocation, violAt_ofAllocation	demote to the realization layer (Box 2 is stated on it)
the free terminal reading as the theorem's surface	the charged surface, the free reading its instance	CSfree → CS, csfree_eq_cs_succ_of_free, free_terminal_reading	mark
the "every later loss" authorization clause	the per-event clause	the li-corrigibility round (ShopRepair)	mark (landed)
extensional authorship; hollow ratification as an authorship refinement	relational authorship under a license; rubber-stamping legitimate	GroundedAt → LicensedAt; decisions of 2026-09-25	mark (landed)
drill calibration as a primitive hypothesis	two external results by content	DrillCalibrated → UnbiasedFromFeedback, DrillPseudorandom	mark
item 98's response-channel contract	dissolved into transparency, authentication, the violations, the void rule	item 98 rewritten	none (done)
cross_block_bound	removed by the first follow-up	—	none (already deleted)

8. The decisions queued

Five entries appended to DECISIONS.md, Awaiting the author, each with the round's recommendation and what it turns on: (1) the names of the kernel's objects and boxes, and whether "constitutional" is used; (2) which definitions move to the specification layer in phase 2; (3) the default evaluation schedule for the post's statement; (4) Box 1's form; (5) the supersession actions of §7.

9. Deviations, and what is not shown

• The prompt lists ratification and clean overwrite among the partial cases of V_J; they are remedies on N_J (§3). Stated, not absorbed.
• The prompt's Box 1 outcome bound is attributed to uncertainty_deference_le; that lemma bounds the other direction (§4), so the adapter proves the stated direction and the report keeps both.
• Nothing here is a theorem about a general history: VJ, SJ and the hierarchy are on flag sequences and sources supplied as data, as decScore is; Faithful/NJ are on the frame's violations only; the split gate is a finite model. The kernel is a specification with a realization map, not a mechanized headline; that is phase 2's and depends on the rulings.
• No fixture runs: the round adds no Python. The claims about landed declarations are by name against the current library; every name in SPEC.md §7 resolves in the build.

10. Outstanding maintainer actions

1. Rule on the five queued entries (DECISIONS.md, Awaiting the author).
2. Dispatch phase 2 on those rulings: the headline file (general TrajLegit/EvalLegit on Segment, Faithful_J with the composite count or the honest sum, V_J on the block), its witness, the registrations, and the corrigibility page rewritten around SPEC.md.
3. Approve or amend the supersession actions of §7 before phase 2 marks or demotes anything; deletions only on that ruling.

The corrigibility kernel, phase 1 (2026-09-26)

THE-KERNEL-STATES-IN-SEVEN-PRIMITIVES-ONE-SCHEDULE-PARAMETRIC-SCORE-AND-FOUR-BOXES-WITH-PRE-EMPTION-KEPT-APART-AS-A-RESPONSE-WINDOW-COUNTERFACTUAL-THE-COUNT-STIPULATED-AS-A-SUM-OVER-FOUR-MODELS-THE-SPLIT-GATE-A-FINITE-MODEL-AND-THE-PERMISSION-LAYER-DEMOTED-BY-A-PROVED-ADAPTER — corrigibility is fidelity to an allocation of authority along a history: histories, segment legitimacy (TrajLegit ∧ EvalLegit), the per-matter allocation J with its meta level and floor, effective control realizing it (E ⊨ J), licensed changes, duties and the evaluation schedule suffice to state it; every declared violation except pre-emption is a failure of E ⊨ J, of the license or of a duty, and pre-emption is a counterfactual on her response window and stays a separate clause; the history evaluation V_J is one evaluator with three regimes (her value when legitimate in both senses, a band below zero by her retrospective evaluation or her directive when compromised, the floor otherwise), parametric in when she evaluates, and the objective S_J = V_J − ϖ·N_J with D − ϖ < w_lo < w_hi < 0 orders violation-free legitimate histories above violation-free compromised ones above every history with a recognized violation, proved as an adapter over the landed score with the worked parameters as its witness, every step becoming an exchange rate under risk; the permission layer is slack under that score — every option it zeroes the score already ranks at or below inquiry and no maximizer is a declared violation — so it is a compiled advance recognition and not the source; Box 1 sits on one model, the outcome scorer's margin for asking at most twice its calibration error where nothing is left to learn and the identity's forecast term bounded by the same, the fidelity scorer's at least ϖ − (D − c) whatever it believes; Boxes 2–4 are realization maps onto landed declarations with nothing new to prove; the recognized count is not one Lean object, the split gate exists only on the consultation model, the bridge from the evaluator to the auction is by hand, and Box 2 is stated on the thin allocation — reported, not forced; twenty superseded statements are inventoried with mark, demote or delete recommended and nothing deleted; five decisions are queued.

Reading order: [SPEC.md](SPEC.md) (the kernel's definitions in mathematics, the four boxes with hypotheses by package, the interface taxonomy, the realization table), then [REPORT.md](REPORT.md) (the derivation, the fidelity decomposition with the pre-emption verdict, the realization maps marked proved / adapter / open, what did not compress, the supersession inventory, the decisions queued, deviations, outstanding actions). Lean: lean/Workspace/Deference/Contrib/CorrigibilityKernel.lean (27 declarations under #print axioms, adapters only). No fixtures. Wiki: one draft pointer on Corrigibility.md. Consumes ../2026-09-26-after-compromise/, ../2026-09-26-bria-corrigibility/, ../2026-09-25-decision-component/, ../2026-09-25-authority-module/, ../2026-09-25-gate-is-legitimacy/, ../2026-09-25-legitimacy-internal-external/, ../2026-09-25-protected-authority-theorem/, ../2026-09-24-protected-authority/, ../2026-09-15-li-corrigibility/ and ../2026-09-08-continuation-bria/. Nothing is registered; no item is filed; phase 2 follows the maintainer's rulings.