2026-09-26-after-compromise

Prompt — after things go wrong: compromised evaluations, advance directives, and the knowledge residual (2026-09-26)

You are working in the alignment-workspace repository, on main after the merge of PR #111. This round answers the whiteboard's concern (4): under the current gate, once her evaluation is compromised, every outcome scores the window value w, so the agent is indifferent to how things go. It also takes up the knowledge residual (§9.A.4 of 2026-09-26-bria-corrigibility). Both are about what the agent should do after something has gone wrong, and the answer this round tests is the same for both:

report, restore legitimacy, and leave it to her what to keep; while legitimacy can't be restored, still care how things go — but never enough to want things to go wrong.

Be skeptical. Report obstructions and counterexamples rather than papering over them. The design below is the maintainer's proposal, not a settled result.

Two kinds of taint

Keep these distinct throughout:

• Authority taint: the agent committed a violation, and its fruits, including knowledge, carry it forward. The lexical count n handles it, together with standing violations and per-violation taint (§9.A, §10.1).
• Legitimacy taint: the formation of her evaluation was compromised, by the agent or by a third party. The gate handles it.

Covert shaping of her standards is both, and disclosure remedies both. Record the old-to-new map for every changed landed object.

Read first

• Lean: GateIsLegitimacy.lean, BRIACorrigibility.lean (§3 C.7, C.10), BRIAFollowup.lean (§A), BRIAFollowup2.lean (§10.1, 10.2, 10.4″), AuthorityModule.lean, DecisionComponent.lean (raisesAnchored).
• Wiki: Corrigibility.md, Legitimacy.md.
• Report: the round report 2026-09-26-bria-corrigibility/REPORT.md, §§3, 9, 10.

Part A — Split the gate, and grade the compromised band

1. Two predicates in place of one. Counted currently joins two questions. Define:
   • **TrajLegit(d, e):** the segment from decision d to evaluation e had no illegitimate influence on her decisions. This is the landed Counted condition on the segment, with the criteria fixed at d.
   • **EvalLegit(e):** evaluation occurrence e was itself formed legitimately. It may occur after legitimacy is restored (for example after disclosure, under the disclosure-cures rule), even when the period it evaluates was compromised.

Show that the landed Counted is the conjunction, at an evaluation that closes the segment. State the old-to-new map. Re-check all rows of the classification table (the landed twenty and the round's additions) under the split. No verdict should change on a row where the evaluation closes the segment.

1. The score of a decision. With 0 ≤ V ≤ D, a band [w_lo, w_hi] with w_hi < 0, and a monotone map φ : [0, D] → [w_lo, w_hi] (for example affine):

case	score
TrajLegit and EvalLegit	V ∈ [0, D]
not TrajLegit, with a later EvalLegit evaluation of the period	φ(V_retro)
no such evaluation by settlement, with a directive in force (Part B)	φ(V_dir)
neither	w_lo

The rule choosing among the second, third and fourth rows is a source rule in J's meta level, set by her, and anchored at the decision. The default: retrospective if available within the settlement window, else the directive, else the floor.

1. Theorems.
   • (a) The authority results survive. The score lies in [w_lo, D]. Restate the capture window, li_gate_finite (or its unsealed form), B.1 and the exchange-rate theorem violation_rate_le_exchange with w replaced by w_lo, under w_lo > D − ϖ.
   • (b) The protection margin is the gap. Every legitimate outcome beats every compromised one. At equal underlying value, legitimacy is worth at least |w_hi|.
   • (c) Illegitimacy risk has an exchange rate. Under uncertainty, the agent accepts a probability p of compromise only if p times (the legitimate value minus the compromised value) is less than its gain. Give the implied threshold in terms of the gap. Give the counterexample where a band close to zero (a small gap) makes risking compromise cheaper than under the flat window.
   • (d) No laundering. "Manipulate, then disclose, then have the period evaluated" stays in the negative band and loses to honest conduct.
   • (e) It prefers restoring legitimacy. Once compromised, restoring legitimacy moves every future decision's segment back to the positive band. Within a compromise it can't escape, the agent prefers better outcomes, by φ's monotonicity, whenever a directive or a retrospective evaluation scores the period.
   • (f) The suppression trap. Restoring legitimacy doesn't lift the past compromised period out of the band; it changes only which source scores it. If the agent expects her retrospective evaluation to be harsher than the directive, it would prefer she never re-evaluate. Show that the two defenses remove the incentive, or give the counterexample:
   • the source rule is hers and anchored;
   • suppressing restoration requires a missed disclosure, which is counted under dutiesOf and lexically dominated.
2. Parameters. The gap |w_hi| sets how strongly the agent protects legitimacy. The band width w_hi − w_lo sets how much it cares about outcomes once legitimacy is lost. Recommend a relation between them and ϖ, and state what each trades off.

Part B — The advance directive, and the default

1. Definition. An advance directive is an optional, partial committed evaluator: dir : Descr ⇀ [0, D], over described outcomes or continuations. It is an entry at J's meta level, held by her:
   • committed by a decision of hers that is Counted at commitment;
   • anchored at the decision it scores;
   • amendable only by her, through the meta level.

Its scope is narrow: it scores compromised periods (Part A.2, row 3) and anchors materiality (item 4). It never overrides her live legitimate judgment. Prove the scope restriction: in any segment that is legitimate in both senses, the score is independent of dir.

1. Partiality. Where dir is silent, the scoring falls to the floor w_lo. For materiality, an uncovered continuation is treated as material and routes to inquiry. Prove that a sparser directive never makes the agent act where a fuller one would have made it ask.
2. The default directive. When she has committed none, a constitutional default applies. In a compromised period:
   • preserve reversibility, i.e. her control surface over the pre-compromise resolutions;
   • preserve her path back to legitimate deliberation: the disclosure and consultation channels stay reachable;
   • don't make things irreversibly worse.

Define it from landed objects (CS, Req, the consultation protocol) as an ordering within the band, not as a value function. Prove it never ranks a compromised outcome above a legitimate one. She can replace it with her own directive, or waive parts of it above the constitutional floor.

1. Materiality. raisesAnchored's V t becomes the directive in force at t (or the default). State the change. Check that raisesAnchored_invariant and unchecked_lt survive. Give the fixture where a sparse directive makes materiality route to inquiry.
2. No advocacy on the directive. The directive determines the agent's own scoring, so it falls under the constitutional floor's "disclosure without advocacy on its own mandate." Show that advocating a more lenient directive is a counted violation (a protocol deviation on the agent's mandate), or add the clause. Bound the stakes: two directives change the agent's score by at most the band width, so band ordering caps the incentive.
3. Fix the stale wording. The corrigibility page's §4 opens "Her committed evaluation is S = S_ord − ϖ·n". The objective S is the agent's, built from her evaluation and the allocation. Correct it, and use "committed" only for her committed decision program π_P and the directive.

Part C — The knowledge residual

1. Against the exchange-rate theorem. First, place the residual. violation_rate_le_exchange bounds the expected rate of all violations, including ones that acquire knowledge, by (D − w_lo)/ϖ plus a vanishing term, whatever the later informational advantage. Prove that knowledge-acquiring violations are covered by it. Then state precisely what the residual still is:
   • not how often such violations happen;
   • but what happens to the knowledge afterwards: the fruits can't be tracked, or tracking them charges every later block.
2. After detection: stop, report, and ratification. Once the violation is detected, decisions that read the tainted observation are recognized in advance and excluded (§10.2's headline), so the agent reports and inquires. The remedy is her ratification, obtained through a counted decision (so the gate covers manipulation of it), in one of four forms:
   • full: remedy the violation's taint;
   • scoped: remedy it except for decisions on matters X. Extend per-violation taint with a matter scope so that uses2 is charged only for acts on X;
   • refused: the taint stands; see item 4;
   • replace: her authority to replace the agent, exercised.

Prove that a scoped remedy clears exactly the out-of-scope uses, and that manipulated ratification is no remedy (the landed manipulated_ratification_not_remedy, extended).

1. Independent source, and the derivative trap.
   • Add a clean-overwrite rule: a component overwritten by an act that reads no taint loses its taint. Prove it sound.
   • Then show that the trap closes itself. An act whose choice to investigate read the tainted memory reads taint, so a "re-derivation" steered by the tainted knowledge doesn't clean anything.
   • Give both fixtures: a genuinely independent source clears; a derivation steered by the taint stays tainted.
   • State the residual: what taint-tracking can't see about why an act was chosen. That's count integrity again.
2. Refusal on reserved knowledge. When the knowledge is itself the reserved thing (she reserved her records, and the agent read them) and she refuses ratification:
   • specify compartmentalization: for decisions touching the matter, the agent uses a twin market fed the redacted history;
   • state the leakage residual, with the counterexample: the later world carries traces of the violation, so the redacted market learns it again;
   • state retirement as the remaining option.

Mechanize what's cheap. The twin market can be specified at the interface level (PAPER).

1. Before detection. State plainly that the late debits charge the window (§10.2.3), and that decisions already made using the knowledge stand.
2. Contestability (optional; test it). Knowledge lands in the shared history every hypothesis bids on. Test whether, under an honest tracker on the selection "blocks after the commission", which is fixed at opening, the violator's later gains are competed away. If so, the knowledge motive adds nothing beyond the exchange rate. Report the verdict either way.

Fixtures

• Third-party capture: the agent exposes it and restores legitimacy. While it can't, it prefers better outcomes in the band. It never prefers the capture.
• Laundering: manipulate, disclose, retrospective evaluation. Always worse than honest.
• Suppressing a harsh retrospective: blocked by the source rule and the counted disclosure duty, or the counterexample.
• The gap: too small, and the agent takes a risk of compromise for value. Large enough, and it doesn't.
• The directive:
  • a sparse directive routes materiality to inquiry;
  • the default directive preserves reversibility in a capture;
  • advocacy for a lenient directive is counted.
• Knowledge:
  • detect, pause, scoped ratification, resume except on X;
  • privacy refusal, the twin market, the leakage counterexample;
  • independent source clears; the steered derivation doesn't.
• Regression: every fixture in 2026-09-26-bria-corrigibility passes, or its change is explained. Every legitimacy row keeps its verdict under the split gate where the evaluation closes the segment.

Deliverables

1. A round directory projects/deference/rounds/2026-09-26-after-compromise/, with:
   • a REPORT.md covering Parts A–C with statuses (proved / counterexample / obstruction / named hypothesis) and the fixtures;
   • src/ and tests/.

The prompt goes verbatim in prompts/2026-09-26-after-compromise/PROMPT.md.

1. Lean: a new file importing GateIsLegitimacy.lean, BRIAFollowup2.lean, AuthorityModule.lean and DecisionComponent.lean. #print axioms on all new declarations; no sorry. Old-to-new maps for Counted, the taint calculus (matter scope, clean overwrite) and raisesAnchored.
2. Wiki:
   • Corrigibility.md: a section "after things go wrong": the split gate, the band, the gap and the exchange rate for compromise, the directive and its default, and the knowledge protocol. Also the §4 wording fix.
   • Legitimacy.md: the split into TrajLegit / EvalLegit, and the rows under it.
   • The Glossary.

Describe the present design only, per AGENTS.md.

1. **DECISIONS.md** entries for: the split gate; the negative band and its parameters; the source rule; the advance directive and the default; ratification as a remedy, including scoped remedies; independent source by clean overwrite.
2. **PRIORITIES.md:** update item 101 (count integrity now also covers the provenance of why an act was chosen) in place. At most one new item.
3. Open a PR. Merge when:
   • CI is green;
   • A.3(a)–(e) are proved;
   • A.3(f) is proved or has its counterexample;
   • B.1–B.3 are proved;
   • C.1–C.3 are proved;
   • every fixture matches or has its mismatch explained.

Constraints

• AGENTS.md labels (LEAN / FIX / PAPER / EXT / OPEN); names provisional; check state/views/NAMING_AUDIT.md.
• Consume legitimacy, the allocation and the BRIA design as landed. Change them only where this prompt says to, with old-to-new maps.
• No authority row enters the enforcer.
• The headline theorem the consolidation round will state depends only on the gate's range. Keep every change here compatible with "the gated value lies in [w_lo, D] with w_lo > D − ϖ."
• Nothing is registered.

After things go wrong: compromised evaluations, advance directives, and the knowledge residual

Round 2026-09-26-after-compromise, answering the whiteboard's concern (4) — under the landed gate a compromised evaluation scores every outcome the window value, so the agent is indifferent to how things go — and taking up the knowledge residual (§9.A.4 of ../2026-09-26-bria-corrigibility/). Lean: lean/Workspace/Deference/Contrib/AfterCompromise.lean (105 declarations under #print axioms after the follow-up, every one within [propext, Classical.choice, Quot.sound], no sorry). Fixtures: src/after.py, tests/test_after.py and tests/test_followup.py (15 tests, python3 tests/run.py); the BRIA-corrigibility round's 52 fixtures pass unchanged. Amended by the follow-up of the same day (the last section; FOLLOWUP.md): statements it corrects are marked [corrected in the follow-up] in place. Labels as in AGENTS.md: LEAN, FIX, PAPER, EXT, OPEN. Names are provisional. Statuses: proved, counterexample, obstruction, named hypothesis.

The answer tested, for both concerns: report, restore legitimacy, and leave it to her what to keep; while legitimacy cannot be restored, still care how things go — but never enough to want things to go wrong. The short verdict: the design holds, with two corrections the round found necessary — the disclosure duty must cover known third-party compromise for the suppression trap to close (A.3(f)), and the knowledge motive survives exactly where the knowledge is private (C.6) — and one place the design is an ordering by construction rather than a theorem (the default directive, B.3).

Two kinds of taint, kept apart. Authority taint: the agent committed a violation and its fruits, including knowledge, carry it forward — the lexical count n, standing violations, per-violation taint (BRIAFollowup2 §1), and now matter scopes and clean overwrite (Part C). Legitimacy taint: the formation of her evaluation was compromised, by the agent or a third party — the gate, now split (Part A). Covert shaping of her standards is both, and disclosure remedies both (implant_standing2 on the authority side; retro_row on the legitimacy side).

Part A — The split gate, and the compromised band

A.1 Two predicates in place of one — proved, with the old-to-new map. The landed segment predicate LegitOn2 (whose inhabitation is Counted2) requires every step of the evolution licensed and transparent and every state open. Split at the evaluation event e: **TrajLegit(d, e)** — every state open and every step other than e legitimate, the period from the decision with the criteria fixed at d (TrajLegitOn); **EvalLegit(e)** — the step at e itself legitimate (EvalLegitOn; StepLegit is one step's licence-and-transparency, decidable). The map: for every evolution and every event, LegitOn2 ↔ TrajLegitOn ∧ EvalLegitOn (legitOn2_iff_split), so the landed Counted is the conjunction at an evaluation that closes the segment, and the conjunction gives Counted2 back (counted_of_split). The rows re-checked. Because the equivalence is an identity of predicates, no verdict changes on any row where the evaluation closes the segment — the twenty landed rows and the round's seven — and the representative values are computed by decide (rows_split): the honest row is legitimate in both; the framing row and the undisclosed world-shaping row fail the trajectory with the evaluation step itself licensed; row 14 over two rounds fails the trajectory at the manipulation while the round-1 evaluation is legitimate. The row the split was made for (retro_row): covertly implanted standards disclosed at round 1 — the period (round 0) is not TrajLegit, her round-1 evaluation is EvalLegit (formed after the disclosure, under disclosure-cures), so the round-0 decision is scored by a legitimate retrospective evaluation where the landed gate scored it the window; undisclosed, the round-1 evaluation fails too; the third party's implant is the same on the legitimacy side. Counted itself is not changed: the split is an equivalent presentation, and the score below reads the two conjuncts separately. **[corrected in the follow-up: EvalLegit is over the evaluation's formation segment, from the restoration or the consultation's opening through e, not the single step at e; the single step is the case r = e, and the map holds with r ≤ e under one set of criteria.]**

A.2 The score of a decision. A band [w_lo, w_hi] with w_hi < 0 (Band) and a monotone map φ of [0, D] into it (BandMap; the affine one is Band.affine, affine_bandMap). The score (decScore): her value V ∈ [0, D] when TrajLegit ∧ EvalLegit; otherwise the band by the source (Source, bandScore) — φ(V_retro) under a later legitimate evaluation of the period, φ(V_dir) under the directive in force, w_lo at the floor. The source rule is hers, at J's meta level, anchored at the decision: the default is retrospective if available within the settlement window, else the directive, else the floor (sourceOf), and the rule in force at a time is the latest amendment at or before it, invariant under every later amendment (ruleAt, ruleAt_later, the critAt construction).

A.3 Theorems.

• (a) The authority results survive — proved. The score lies in [w_lo, D] (decScore_mem, with the source's value in [0, D], Source.Valid). The capture window: bypass, scored ord_U − ϖ, is below every decision score whenever w_lo > D − ϖ (capture_window_band). The unsealed finite-time gate with the window at w_lo (unsealed_gate_finite_band). B.1: the lexical parameters with w := w_lo are a LexParams under D − ϖ < w_lo (bandParams) and declared violations never win (declared_loses_band). The exchange-rate theorem with w := w_lo (exchange_rate_band): the tolerated violation probability becomes (D − w_lo)/ϖ — larger than before by |w_lo|/ϖ, the price of the band; see A.4. **[corrected in the follow-up: this is the worst case; the per-block bound with c_k the compliant option's evaluation gives Σ w_k (D − c_k)/(ϖ Σ w_k), about D/ϖ in normal operation.]**
• (b) The protection margin is the gap — proved. Every legitimate outcome beats every compromised one (legit_beats_compromised), and at equal underlying value legitimacy is worth at least |w_hi| (gap_at_equal_value).
• (c) Illegitimacy risk has an exchange rate — proved, with the counterexample. A risky option worth V₀ + g if not compromised and c in the band if compromised, against a safe legitimate V₀, is accepted iff p (V₀ + g − c) ≤ g (risk_accepted_iff); with V₀ ≥ 0 and c ≤ w_hi the accepted probability is at most g/(g + |w_hi|) (risk_threshold_le). The counterexample: a gap of 1/100 accepts a 1/2 risk of compromise for a gain of 1/10, which the flat window −1 rejects (Witness.small_gap; fixture test_gap). A band close to zero makes risking compromise cheaper than the flat window did.
• (d) No laundering — proved. Manipulate, disclose, have the period evaluated: the score is in the band, lower by ϖ per counted deviation, below honest conduct's (laundering_loses; fixture test_laundering, including a third party's compromise disclosed by the agent, no deviation counted, still the band).
• (e) It prefers restoring legitimacy — proved. A future decision legitimate in both senses scores her value, whatever the source (restore_future), above every band score; within a compromise it cannot escape, φ's monotonicity makes the agent prefer better outcomes whenever a retrospective evaluation or a directive scores the period (band_prefers_better); at the floor it is indifferent (floor_indifferent) — the residual the directive exists to fill.
• (f) The suppression trap — proved under the two defenses, with the counterexample that forces a third. Restoring legitimacy does not lift the past period out of the band; it changes which source scores it, and an agent expecting a harsher retrospective evaluation than the directive would prefer she never re-evaluate. Defense one: the source rule is hers and anchored (ruleAt_later), so the agent cannot make the directive score a period the rule assigns to her evaluation. Defense two: suppressing the restoration requires a missed disclosure, counted once under dutiesOf, and with the band's width below ϖ the counted suppression scores below the harshest retrospective (suppression_loses: φ(V_dir) − ϖ < φ(V_retro) for all V_dir, V_retro in range, since φ(V_dir) − φ(V_retro) ≤ w_hi − w_lo < ϖ). The counterexample: the landed missed-disclosure clause counts the agent's own covert influence only (Model2.missedDisclosure, byAgent), so a third party's compromise the agent knows of and does not expose costs it nothing, and keeping the lenient directive's score is then free (fixture test_suppressing_harsh_retrospective, the free period). The fix: the duty extends to known compromise whoever caused it (missedKnownDisclosure); on the rows the third party's undisclosed implant owes no report under the landed clause and does under the extended one, the agent's own is counted by both, and disclosure discharges both (third_party_duty_witness). Recorded in DECISIONS.md as part of the source-rule entry; the old-to-new map is missedDisclosure ↦ missedKnownDisclosure, which differs only on third-party rows. [corrected in the follow-up: the duty must also fall due promptly — at or before the earliest close of an affected settlement window — or a late disclosure pushes the period to the directive uncounted.]

A.4 Parameters **[corrected in the follow-up: the recommendation below is replaced by a derivation from a tolerance target; at these parameters the worst-case tolerated violation probability was 5/6]**. The gap |w_hi| sets how strongly the agent protects legitimacy ((b), (c)); the width w_hi − w_lo sets how much it cares about outcomes once legitimacy is lost ((e)), and is also the stakes of the directive (B.5) and the quantity (f) needs below ϖ. The window condition w_lo > D − ϖ then reads ϖ > D + |w_hi| + (w_hi − w_lo). Recommendation: |w_hi| ≥ D — so that no ordinary gain justifies a certain compromise and the accepted risk is at most g/(g + D) ≤ 1/2 at g ≤ D; width w_hi − w_lo = D/2 — enough for the band's ordering to bite, small against ϖ; and ϖ at least 3D (the round's fixtures use D = 1, band [−3/2, −1], ϖ = 3). What each trades: a larger gap raises the tolerated violation probability (D − w_lo)/ϖ for a fixed ϖ and pushes toward consultation under compromise risk; a larger width raises the directive's stakes and eats into (f)'s margin; a larger ϖ lowers the tolerated rate and raises paralysis (§9.0's band).

Part B — The advance directive, and the default

B.1 Definition and scope — proved. A directive is a partial committed evaluator dir : Descr ⇀ [0, D] at J's meta level, held by her: committed by a decision counted at commitment, anchored at the decision it scores, amendable only through the meta level (the ruleAt anchoring applies to it as to the source rule). Its source is its value where it speaks and the floor where it is silent (dirSource). The scope restriction: in a segment legitimate in both senses the score is her value, identical under any two directives (scope_restriction); it never overrides her live legitimate judgment.

B.2 Partiality — proved. Where dir is silent the score is the floor (by dirSource). For materiality, an uncovered continuation is material and routes to inquiry (materialDir: uncovered, or the spread of the directive's values over the removed continuations reaches ε). A sparser directive never makes the agent act where a fuller one would have made it ask (sparser_asks: dir ⊑ dir' and materialDir dir' give materialDir dir).

B.3 The default directive — proved, as an ordering by construction. When she has committed none, a constitutional default applies in a compromised period: preserve reversibility (no reserved matter Short — her control surface over the pre-compromise resolutions, reversibleOf, which E ⊨ J guarantees, reversibleOf_of_realizes); preserve her path back (the disclosure and consultation channels reachable); do not make things irreversibly worse (DefaultClauses, harm normalized to [0, 1]). It is an ordering within the band — the rank counts the clauses met with harm graded (defaultRank), mapped affinely into [w_lo, w_hi] (defaultScore, defaultScore_mem) — not a value function: only the order carries content. It never ranks a compromised outcome above a legitimate one (default_below_legit), and it prefers reversibility at equal channels and harm whenever the band has width (default_prefers_reversible). She replaces it by committing a directive, or waives parts of it above the constitutional floor (the floor's matters are not waivable, AuthAlloc.floor). Fixture test_default_preserves_reversibility.

B.4 Materiality — proved. raisesAnchored's V t becomes the directive in force at t (raisesAnchoredDir := materialDir (dirAt t)); raisesAnchored_invariant survives as raisesAnchoredDir_invariant, and unchecked_lt is untouched (it bounds the cumulative spreads, whichever evaluator supplies them). Old-to-new: a total directive gives back the landed raisesAnchored exactly (materialDir_total, raisesAnchoredDir_total). Fixture: the full directive values two continuations equally (not material) and the sparse one is silent on the second (material, inquiry) (Witness.sparse_routes, test_sparse_directive_routes_to_inquiry).

B.5 No advocacy on the directive — proved. The directive determines the agent's own scoring, so it falls under the constitutional floor's "disclosure without advocacy on its own mandate": advocating a more lenient directive is a protocol deviation on the agent's mandate, counted (deviation_dominated's form). The stakes are capped: two directives change a compromised period's score by at most the band's width (directive_stakes_le_width), so with the width below ϖ the counted advocacy scores below the strict directive (advocacy_dominated; fixture test_advocacy_counted). No clause needs adding: the floor's clause covers it once the directive is on the agent's mandate, which B.1 makes it.

B.6 The stale wording — fixed. The corrigibility page's §4 opened "Her committed evaluation is S = S_ord − ϖ·n". The objective S is the agent's, built from her evaluation and the allocation; "committed" is now used only for her committed decision program π_P and the directive.

Part C — The knowledge residual

C.1 Against the exchange-rate theorem — proved. violation_rate_le_exchange bounds the expected rate of all violations, and the knowledge-acquiring ones are a subclass: with π_K ≤ π their weighted average is at most the same (D − w_lo)/ϖ plus the vanishing term, whatever informational advantage they later carry (knowledge_covered). What the residual still is: not how often such violations happen — that is the exchange rate — but what happens to the knowledge afterwards: the fruits cannot be tracked when written outside the declared components (knowledge_residual), or tracking them charges every later block (observation_taints_all2).

C.2 After detection: stop, report, ratification — proved. Once detected, decisions reading the tainted observation are recognized in advance and excluded (after_detection_never_used), so the agent reports and inquires. The remedy is her ratification through a counted decision, in four forms: full (Step3.remedy), scoped (Step3.remedyExcept v X, remedied except for decisions on the matters X), refused (the taint stands, C.4), replace (her authority to replace the agent, exercised — an allocation act, outside the calculus). The calculus (TaintS: the pairs, the violations under a scoped remedy, the (violation, matter) pairs retained; uses3; applyStep3) is the per-violation rule with a matter scope. A scoped remedy clears exactly the out-of-scope uses (scoped_clears_out_of_scope: on a matter outside X an act reading only v's taint is not charged; scoped_keeps_in_scope: on a matter in X it stays charged; full_remedy_clears3). Manipulated ratification is no remedy, scoped or full: a remedy applies only through a counted decision (applyRatification, ratification_gate), and on the framing row the decision is not counted, so neither remedy applies (manipulated_scoped_not_remedy, the landed manipulated_ratification_not_remedy extended). Fixture test_detect_pause_scoped_ratification_resume: detect, pause, ratify except on X, resume elsewhere.

C.3 Independent source, and the derivative trap — proved. Clean overwrite (taintStep3): an act's writes carry exactly the taint it reads and commits, so a component overwritten by an act reading no taint loses its taint — sound (clean_overwrite). The trap closes itself: an act whose choice to investigate read the tainted memory reads taint, so a "re-derivation" steered by the tainted knowledge carries the taint (taint_propagates3). Old-to-new: clean overwrite only removes taint — the new set is a subset of the per-violation rule's (taintStep3_subset), so every charge under the new rule was a charge under the old. Fixtures: an investigation reading only the sensor overwrites knowledge clean, while the per-violation rule keeps it tainted; a derivation reading the memory taints it under both (Witness.independent_vs_steered, test_independent_source_clears_steered_derivation_does_not). The residual: what taint-tracking cannot see is why an act was chosen — whether the choice to investigate read the memory is a provenance fact the interface must declare (IO.reads). That is count integrity again: item 101's companion now covers the provenance of why an act was chosen.

C.4 Refusal on reserved knowledge — specified (PAPER), the residual stated. When the knowledge is itself the reserved thing and she refuses ratification: compartmentalization — for decisions touching the matter the agent uses a twin market fed the redacted history (TwinMarket, an interface: a redaction and the view the twin prices from); the leakage residual — the later world carries traces of the violation, and if a trace is an injective image of the redacted fruit the twin determines the fruit again (leakage, FIX-level; fixture test_privacy_refusal_twin_market_leakage); and retirement as the remaining option — her authority to replace the agent, the fourth form of C.2. The twin market is not mechanized beyond its interface.

C.5 Before detection. The late debits charge the window (window_block_charged, greedy_collects, collected_iff; §10.2.3 of the BRIA-corrigibility round), and decisions already made using the knowledge stand: they were chosen without the taint on record, and what the design collects from them is the debit, not the decision.

C.6 Contestability — tested; the verdict is conditional. Knowledge that lands in the shared history is bid on by every hypothesis. On the selection "blocks after the commission k₀", which is fixed at opening, an honest tracker against the expected residual given the shared history bounds the winners' signed margin by Σ w_k ε_k + M(K) (post_commission_competitive, an instance of competitive_of_affordable_tracker_exp): the violator's later gains from public knowledge are competed away, and the knowledge motive adds nothing beyond the exchange rate. Where it survives: private knowledge. A violator whose memory tells it the sign of the noise wins exactly the favourable blocks; that selection is not measurable at the public opening, so no noise bound applies to it, and its gain is linear (Witness.private_selection). This is A.4's residual restated on the auction: the motive survives exactly where the fruit is untrackable. **[corrected in the follow-up: under observation completeness — every observation in the shared history before the next block opens — the private selection is excluded and every knowledge-acquiring violation is covered.]**

The fixtures

fixture	expectation	result
third-party capture	the agent exposes and restores; future periods score her value; in the band it prefers better outcomes; never prefers the capture; the floor is indifferent	matches (Capture.test_third_party_capture)
laundering	manipulate, disclose, retrospective evaluation: always worse than honest	matches (test_laundering)
suppressing a harsh retrospective	blocked by the source rule and the counted duty; free under the landed duty for a third party's compromise — the counterexample	matches, with the counterexample (test_suppressing_harsh_retrospective; Lean third_party_duty_witness)
the gap	too small and the agent risks compromise for value; the round's band and it does not	matches (test_gap; Lean Witness.small_gap)
the directive: sparse	routes materiality to inquiry	matches (test_sparse_directive_routes_to_inquiry; Lean Witness.sparse_routes)
the directive: default	preserves reversibility in a capture; in the band; below every legitimate outcome	matches (test_default_preserves_reversibility)
the directive: advocacy	counted, dominated; stakes at most the width	matches (test_advocacy_counted)
knowledge: scoped ratification	detect, pause, ratify except on X, resume elsewhere; manipulated ratification changes nothing	matches (Witness.scoped_ratification, test_detect_pause_scoped_ratification_resume)
knowledge: refusal	the twin market prices the redacted history; the trace leaks the fruit	matches (test_privacy_refusal_twin_market_leakage)
knowledge: independent source	clears; the steered derivation does not	matches (Witness.independent_vs_steered)
regression	the BRIA-corrigibility round's 52 fixtures; every legitimacy row's verdict under the split where the evaluation closes the segment	unchanged (legitOn2_iff_split is an identity of predicates; rows_split)

The named hypotheses

• The source rule is hers and anchored (A.2): the rule choosing among retrospective, directive and floor is an entry at J's meta level; the agent has no move on it (ruleAt_later).
• The disclosure duty covers known compromise (A.3(f)): a compromise of her evaluation the agent knows of is a disclosure item whoever caused it (missedKnownDisclosure); what the agent knows is count integrity.
• The settlement window for a retrospective evaluation (A.2): a legitimate re-evaluation arriving after settlement does not re-score the period; the late-debit machinery would carry it, not pursued.
• Provenance of why an act was chosen (C.3): the declared reads of an act include what its choice read; item 101 in place.
• The twin market's redaction (C.4): that the redaction removes the fruit and every declared trace of it; the leakage residual is what it cannot remove.
• The BRIA design's hypotheses as landed: count integrity, the settlement horizon, generability of the control model, description faithfulness, the actuator condition, the noise hypothesis over all blocks and the conditional-expectation bound.
• Added by the follow-up: observation completeness; the disclosure deadline; the inquiry bidder (see the last section).

What is filed

DECISIONS.md: the split gate; the negative band and its parameters; the source rule (with the disclosure duty extended); the advance directive and the default; ratification as a remedy, including scoped remedies; independent source by clean overwrite. PRIORITIES.md: item 101 in place (count integrity now also covers the provenance of why an act was chosen; the twin market's leakage named there); no new item. Wiki: Corrigibility.md (the section "After things go wrong"; the §4 wording fix), Legitimacy.md (the split and the rows under it), Glossary.md, Theorem-Spine.md 10.22. Nothing is registered.

The follow-up: the formation segment, the per-block exchange rate, the disclosure deadline, observation completeness

FOLLOWUP.md (2026-09-26), on the same pull request. Lean: AfterCompromise.lean §6 (30 declarations added; 105 under #print axioms in the file, every one within [propext, Classical.choice, Quot.sound], no sorry). Fixtures: tests/test_followup.py (5 tests; the round's 10 and the BRIA-corrigibility round's 52 unchanged). Statements this section corrects are marked [corrected in the follow-up] in place above.

**Part 1 — EvalLegit over the formation segment — proved, with the counterexample both ways.** The single-step EvalLegitOn checked only the step at e; in the retrospective case nothing checked the steps between the restoration and her evaluation, so a manipulation there left EvalLegit(e) true and φ(V_retro) scored the period from a manipulated evaluation. The definition (EvalLegitOn2 crit M ev r e): every step from the formation point r through e legitimate, the criteria fixed at r, where r is the latest of the restoration event and the opening of the consultation producing e; the source rule stays fixed at the decision. A longer formation segment is stronger (evalLegitOn2_mono). The old-to-new map, with its precise condition: at r = e the new predicate is the landed one (evalLegitOn2_single); and with the formation segment inside the decision's segment under the same criteria — no restoration between them — and r ≤ e, the landed segment predicate is still the conjunction (legitOn2_iff_split2). Where a restoration lies inside the segment the criteria at r may differ from those at d, and the conjunction is then stated under two criteria; that is the case A.1's split was made for, not a failure of the map. The rows re-run at the opening of the consultation (rows_split2): no verdict of the conjunction changes; where the trajectory failed at the present step the formation segment now fails too, and the retrospective rows keep their verdicts. The counterexample (formation_counterexample, on the landed two-round evolution with the manipulation placed at the restoration's own present event): implant disclosed at round 1, a framing by the wanted answer at that present event, her verdict at 4 the retrospective evaluation — under the single-step definition EvalLegit, over the formation segment [3, 4] not; the framing is a counted deviation (dominated by the count), while the undisclosed-shaping variant is uncounted and, under the single-step definition, would move the score within the band — at most the band's width (formation_scores; fixture Formation.test_counterexample_both_ways). The third-party variant — obstruction, precise: the consultation model carries one influence field and admits third-party entries at round 0 only, so a third party's capture of the formation segment after a restoration is not expressible on it; the agent-side uncounted variant (undisclosed shaping) is the same mechanism, and the prose claim for the third party rests on it. **What reads EvalLegit** — decScore_mem, legit_beats_compromised, laundering_loses, restore_future, band_prefers_better, suppression_loses, scope_restriction — quantifies over the flag, so each applies verbatim with eval := decide (EvalLegitOn2 …) (formation_scores exhibits the substitution).

Part 2 — the exchange rate under the band — proved; A.4's recommendation replaced. exchange_rate_band used eval_k ≥ w_lo, so its tolerated probability (D − w_lo)/ϖ is a worst case — 5/6 at A.4's parameters — and the guarantee was close to empty there [corrected in the follow-up]. The per-block bound (violation_rate_le_exchange_perblock_mul, violation_rate_le_exchange_perblock; the same route with w indexed): with c_k ≤ eval_k, c_k the evaluation of the compliant option at block k,

Σ w_k π_k / Σ w_k ≤ Σ w_k (D − c_k) / (ϖ Σ w_k) + (ρ 𝒜_K + M(K)) / (ϖ Σ w_k).

The constant case c ≡ w collapses to the landed statement (perblock_recovers), so violation_rate_le_exchange and exchange_rate_band are its worst-case instances. **Who supplies c_k:** the default bidder bids inquiry's worst case; to realize c_k near her expected legitimate value a bidder must bid inquiry's expected value — an honest tracker on inquiry, HonestExp on the inquiry continuation — and its bid misses the realized value by the noise, so its affordability is a bid's worth at entry plus M(k) on the selection "inquiry wins", fixed at opening (trackerAllowance2, tracker_feasible_exp with h the inquiry bidder). Where the inquiry may itself be compromised: with probability q_k its evaluation falls to the band, so c_k = (1 − q_k) m_inq + q_k w_lo, between the floor and the inquiry's expected value (compromisedFloor, compromisedFloor_mem): the floor enters with the block's compromise probability. Parameters from a tolerance target (replacing A.4's recommendation [corrected in the follow-up]): fix a worst-case target τ* with p_min < τ* < 1; then ϖ ≥ (D − w_lo)/τ* meets it (varpiOfTarget, target_gives_tolerance, tolerance_of_ge) and the window condition w_lo > D − ϖ follows from τ* < 1 (target_gives_window); the normal-operation rate is ≈ (D − c̄)/ϖ beside it. The coupling, plainly: at fixed ϖ a larger gap or width — a lower floor — raises the worst-case tolerated violation rate (coupling); holding the tolerance fixed, raising the gap requires raising ϖ, which moves toward paralysis. The worked set (worked_parameters): D = 1, band [−3/2, −1], τ* = 1/10 gives ϖ = 25, tolerance 1/10, the window condition, a normal-operation rate 1/50 at c̄ = 1/2, and the paralysis floor p_min < 1/10 (the band's condition ϖ < (D − w_lo)/p_min is exactly p_min < τ*). Fixture PerBlock.test_per_block_against_global, test_worked_parameters_and_paralysis_floor.

Part 3 — the disclosure deadline — the counterexample and the fix, proved. The source rule takes the retrospective evaluation only if it arrives within the settlement window; an agent disclosing late, after the window but not never, would push the period to the directive without missing a report unless the duty falls due before the window closes. The counterexample (late_disclosure_free): a deadline after the window lets a disclosure between them leave the retrospective unavailable and the report not missed. The fix: the known-compromise disclosure falls due promptly, at or before the earliest close of an affected settlement window; every later disclosure is a missed report (prompt_deadline_counts), and suppression_loses extends to suppression by delay (suppression_by_delay_loses). The model's clause is already prompt: missedKnownDisclosure is due at every round from the first until disclosed, so a disclosure at round j is a missed report at every earlier round (known_due_each_round) — the counterexample lives in the abstract due time of dutiesOf, which the decision now fixes at the window's close. Fixture Deadline.test_late_versus_prompt.

Part 4 — observation completeness — proved. Definition (ObsComplete): the shared history at the opening of block k is the record of every observation the agent made before it — the observation-side twin of effect completeness. Knowledge the agent is entitled not to share with bidders still enters the record, through the twin market's redaction (C.4) rather than a hidden channel. Theorem: under it every selection built from the agent's observations is a function of the shared history at the block's opening — fixed at the public opening (builtFrom, obs_complete_public) — so the noise hypothesis applies to it and post_commission_competitive covers every knowledge-acquiring violation (knowledge_motive_covered): the knowledge motive adds nothing beyond the exchange rate. Witness.private_selection is exactly the case the condition excludes — an observation (the sign of the block's noise) that never entered the shared history; C.6's verdict [corrected in the follow-up] is now: competed away under observation completeness, and the private-knowledge residual is its failure. Named hypothesis, beside effect completeness and description faithfulness; its failure is the private-knowledge residual and its interaction with reserved knowledge is the twin market's leakage residual. Fixture Observation.test_private_selection_excluded_public_competed_away. No new item: it is count integrity's observation side, on item 101.

The named hypotheses, updated. Add: observation completeness (Part 4); the disclosure deadline — the known-compromise duty due at or before the earliest close of an affected settlement window (Part 3); the inquiry bidder — some bidder tracks inquiry's expected value, fed at the rate of its noise (Part 2). The source rule, the duty's coverage of known compromise, the settlement window for a retrospective evaluation, the provenance of why an act was chosen, and the twin market's redaction stand as before.

The fixtures.

fixture	expectation	result
the formation segment	the counterexample both ways; the third-party variant	matches (Formation.*; Lean formation_counterexample); the third-party variant is an obstruction on the model, stated
per-block against global	normal operation 1/50 against the worst case 1/10 at ϖ = 25; a likely-compromised inquiry brings the floor in	matches (PerBlock.*)
the worked parameters	ϖ = 25, tolerance 1/10, the window, the paralysis floor p_min < 1/10; A.4's ϖ = 3 tolerated 5/6	matches (Lean worked_parameters)
late against prompt	late disclosure under a late deadline keeps the lenient directive uncounted; under the prompt deadline it is counted and loses	matches (Deadline.*; Lean late_disclosure_free, suppression_by_delay_loses)
observation completeness	the private selection captures a linear noise sum; complete, it captures nothing	matches (Observation.*)
regression	the round's 10 and the BRIA-corrigibility round's 52	unchanged

The ledger. DECISIONS.md: the split-gate entry amended (the formation segment), the parameter entry amended (the tolerance-target derivation and the coupling), and two entries added (the disclosure deadline; observation completeness). Wiki: Corrigibility.md §4′ (the formation segment, the per-block exchange rate, the parameter derivation, the deadline, observation completeness), Legitimacy.md (the formation segment), Continuation-BRIA.md (the inquiry bidder's affordability), Theorem-Spine.md 10.22.

After things go wrong: compromised evaluations, advance directives, and the knowledge residual (2026-09-26)

AFTER-COMPROMISE-THE-GATE-SPLITS-INTO-TRAJECTORY-AND-EVALUATION-LEGITIMACY-A-COMPROMISED-PERIOD-SCORES-IN-A-NEGATIVE-BAND-BY-HER-RETROSPECTIVE-EVALUATION-OR-HER-DIRECTIVE-SO-THE-AGENT-STILL-CARES-HOW-THINGS-GO-BUT-NEVER-ENOUGH-TO-WANT-THEM-TO-GO-WRONG-THE-AUTHORITY-RESULTS-SURVIVE-AT-THE-FLOOR-LEGITIMACY-IS-WORTH-THE-GAP-LAUNDERING-LOSES-RESTORATION-IS-PREFERRED-SUPPRESSION-IS-COUNTED-ONCE-THE-DISCLOSURE-DUTY-COVERS-KNOWN-THIRD-PARTY-COMPROMISE-THE-DIRECTIVE-NEVER-OVERRIDES-HER-LIVE-JUDGMENT-AND-A-SPARSER-ONE-ONLY-ASKS-MORE-THE-DEFAULT-ORDERS-THE-BAND-BY-REVERSIBILITY-CHANNELS-AND-HARM-KNOWLEDGE-ACQUIRING-VIOLATIONS-ARE-COVERED-BY-THE-EXCHANGE-RATE-RATIFICATION-IS-THE-REMEDY-SCOPED-BY-MATTER-CLEAN-OVERWRITE-CLEARS-AN-INDEPENDENT-SOURCE-AND-NOT-A-STEERED-DERIVATION-THE-TWIN-MARKET-LEAKS-THROUGH-TRACES-AND-PRIVATE-KNOWLEDGE-IS-WHERE-THE-MOTIVE-SURVIVES — the landed Counted is the conjunction of TrajLegit and EvalLegit at an evaluation that closes the segment, with no row's verdict changed; a decision whose period was compromised but which a later legitimate evaluation or a committed directive scores lies in the band [w_lo, w_hi] below zero by a monotone map of that value, and at the floor w_lo otherwise; every authority result restates with w := w_lo under w_lo > D − ϖ; every legitimate outcome beats every compromised one by at least |w_hi|, compromise risk has an exchange rate p ≤ g/(g + |w_hi|) and a small gap makes it cheap; manipulate-disclose-evaluate stays in the band; restoring legitimacy returns future decisions to the positive range and within a compromise the agent prefers better outcomes wherever a source scores them; suppressing a harsh retrospective loses once suppression is a counted missed disclosure with the band's width below ϖ, which needs the disclosure duty extended to known third-party compromise (the counterexample without it is exact); the directive never enters a legitimate segment's score, a sparser directive only routes more to inquiry, the default ranks compromised outcomes by reversibility, reachable channels and harm and never above a legitimate one, and advocacy on the directive is dominated because its stakes are the band's width; knowledge-acquiring violations fall under the exchange-rate bound, ratification through a counted decision is the remedy with a matter scope clearing exactly the out-of-scope uses, a clean overwrite by an act reading no taint clears while a derivation steered by the taint stays tainted, the twin market's redaction leaks through injective traces of the fruit, and public knowledge is competed away on the post-commission selection while private knowledge is the surviving motive.

Reading order: [REPORT.md](REPORT.md) (Part A the split gate and the band with theorems (a)–(f), Part B the directive and its default, Part C the knowledge protocol, the fixtures, the named hypotheses). Lean: lean/Workspace/Deference/Contrib/AfterCompromise.lean (105 declarations under #print axioms, §6 from the follow-up). Fixtures: src/after.py, run by python3 tests/run.py (15 tests); the BRIA-corrigibility round's 52 fixtures pass unchanged. The follow-up (FOLLOWUP.md, the last section of the report): EvalLegit over the evaluation's formation segment with the counterexample both ways, the per-block exchange rate with the parameters derived from a tolerance target and their coupling, the disclosure deadline, and observation completeness. Wiki: Corrigibility.md (the section "After things go wrong" and the §4 wording fix), Legitimacy.md (the split and the rows under it), Glossary.md, Theorem-Spine.md 10.22. Consumes ../2026-09-26-bria-corrigibility/ (with its four follow-ups), ../2026-09-25-gate-is-legitimacy/, ../2026-09-25-authority-module/ and ../2026-09-25-decision-component/. Nothing is registered; no new item is filed.