2026-09-05-integrity-adversary

Common brief for every worker in the 2026-09-05 integrity research batch

You are one of five isolated research workers dispatched by an orchestrator against A-M-Berns/alignment-workspace at main = 5ff9539b44debc464128e6a1921ef1690f7b6487. You are running in your own git worktree (the Agent tool created it from that main); verify with git log --oneline -1 and record any difference in your report rather than forcing it. Work only inside your worktree directory. Never cd into the main checkout or another worktree.

Read first, in this order

1. AGENTS.md — binding. Exact fractions.Fraction arithmetic; a theorem ships as statement + implementation + test + necessity witnesses where feasible; Lean is sorry-free with #print axioms on everything, auditing to [propext, Classical.choice, Quot.sound] and nothing else; **external theory enters as named hypotheses of the statement that uses it, never as axiom declarations**; names you coin are provisional and listed; deviations from this prompt are declared in your REPORT with reasons; the REPORT states what was NOT shown; slop discipline (every sentence does work; no summary of a summary; no compliance narration); no negative ontologies in living documents (your round directory is a completed-round record, so it may narrate its own history, but do not write "formerly X" prose into any file outside it).
2. python3 -m checkers.workspace_state --json — orientation; do not infer current status from completed-round prose.
3. DECISIONS.md (the Awaiting the author queue and the entries dated 2026-09-01 through 2026-09-05), PRIORITIES.md items 74–77, RESEARCH_STATE.md.
4. The wiki pages wiki/Legitimacy.md, wiki/Integrity.md, wiki/Settlement-Interface.md, wiki/Diachronic-Answerability.md, wiki/Openness-Coverage-and-Non-Capture.md, wiki/Normative-Induction.md, wiki/Normative-Inductor.md, wiki/Roadmap.md. The wiki is permitted as conceptual orientation for this dispatch. It is not proof evidence, and you must not edit it.
5. The landed rounds relevant to your lane, cited by path below. Their THEOREMS.md, README.md, REPORT.md and Lean are evidence; their epistemic class is what their own ledgers say (almost everything is paper-derived + exact fixtures = at best test-supported; kernel-checked declarations are named where they occur).

Key paths:

• Lean spine of the history/defeat theory: lean/Workspace/Normativity/Contrib/NormativeContinuity.lean (§4 settlement, §5 unified grounds / answerable defeat / standing / witnesses).
• Realization bridge lemmas: lean/Workspace/Normativity/Contrib/NormativeInductor.lean.
• Rounds under projects/normativity/legitimacy/rounds/: 2026-08-29-normative-continuity-concordance, 2026-08-30-normative-continuity-settlement (SETTLEMENT.md, THEOREM_MAP.md, the .tex), 2026-08-30-answerability-carriers (ANSWERABILITY_CONSERVATION.md, TERMINAL_EXITS.md, TRANSFER_SEMANTICS.md), 2026-08-30-anchored-slices-auth-transfer (ANCHORED_SLICES.md, SEMANTIC_AUTHENTICATION.md, TRANSFER_COMPOSITION.md), 2026-08-31-faithful-semantic-preservation (NO_SEMANTIC_LAUNDERING.md, FAITHFUL_AUTHENTICATION.md, REPAIRED_CONSERVATION.md), 2026-08-23-transition-certificates (MEMO.md), 2026-08-30-proper-exercise-calculus, 2026-08-30-cf-coverage-continuity-interface (COVERAGE_CONTRACTS.md, INTERACTION_INTERFACE.md, SELF_SEALING.md), 2026-08-25-carroll-legitimacy-test (CRITERION.md), 2026-09-02-unified-grounds-answerable-defeat (GROUNDS.md, DEFEAT.md, THEOREMS.md), 2026-09-03-defeat-landing-horty-standing (STANDING_REPAIR.md, WITNESS.md, HORTY.md), 2026-09-04-normative-inductor-realization (NORMATIVE_INDUCTOR_REALIZATION.md, PRESENTATION_AND_VALUE_SEMANTICS.md, THEOREMS.md), 2026-08-31-normative-affordability (SHARP_TIMELY_SERVICE.md, SERVICE_TRANSFER.md, SERVICE_FORCE_TYPING.md), and the checkpoint projects/normativity/legitimacy/checkpoint-2026-09-01/ (CURRENT_THEORY.md, STATUS_LEDGER.md, OPEN_PROBLEMS.md) which is agent-consolidated and must not be edited.
• Program prior art: projects/normativity/notes/PRIOR_ART.md.

Shared orientation (hold with the stated status)

Fairly settled: legitimacy is a property of cognitive evolution, not certification of a state. The proof-relevant object is a history segment H_{m:n}; the consumer-facing object is likely an endpoint relation H_m ⪯_leg H_n witnessed by a legitimate segment. Declared normative scope is application-relative. Integrity (did the trajectory faithfully preserve and account for what entered it?) is distinct from Non-Capture (could the process improperly determine what was able to enter, challenge, or evaluate it?). Non-Capture and counterfactual practical/value semantics are billed to external theories: the generic theory specifies the certificate and proves what follows.

Working hypothesis to TEST, not doctrine: Trajectory Integrity ⇒ Diachronic Answerability. Do not assume it by definition.

Settlement distinction to test: an external settlement item s ∈ SetView(H_n) is an authenticated input through the declared trusted settlement boundary. The internal reasoner separately judges Closes(H_n, s, α) — by the rules/reasons legitimately in force at H_n, s suffices to close obligation α. A discharge is backed by (1) authenticated availability of s, (2) an internally valid Closes certificate, (3) whatever authority/provenance Integrity requires. Settlement items do not arrive typed as "settles α"; they may stay immutable while their judged relevance changes; a later reasoner may find an earlier Closes defective, and the response is probably a new reopening/reconsideration obligation, not retroactive rewriting. The settlement trust boundary is domain-relative; do not force one universal settlement ontology.

Isolation

You do not know what the other four workers are doing beyond their one-line lane names (A: constructive Integrity theory; B: Integrity adversary / laundering audit; C: Non-Capture certificate minimization; D: practical-semantics certificate minimization; E: end-to-end Normative Inductor gap audit). Do not coordinate with them, do not read other worktrees, and do not adopt definitions you have not derived or cited from main.

What you may and may not touch

You MAY create, in your worktree only:

• projects/normativity/legitimacy/rounds/2026-09-05-<your-round-name>/ with README.md (verdict, one paragraph), REPORT.md (concise; verdict line verbatim as in README; a Deviations section; a What this does not establish section; a Proposed filings section listing anything that would need PRIORITIES.md, DECISIONS.md, state/, or vocabulary changes — you do NOT make those changes; an Attribution block: prompt author = the orchestrator (Claude Fable 5.1, Anthropic, relaying a maintainer dispatch), executor = your model name), PROVENANCE.md (one row per file/glob: generator, review status ci-only, date 2026-09-05, originating round prompts/2026-09-05-<your-round-name>/), theorem/countermodel ledgers, src/ and tests/run.py (self-contained runner; python3 tests/run.py must exit 0; exact Fraction arithmetic), and Lean under lean/Workspace/Normativity/Contrib/ in a NEW file with a NEW namespace (do not edit existing Lean files; if a result needs a definition from an existing file, import it).
• prompts/2026-09-05-<your-round-name>/PROMPT.md — the prompt you were given, verbatim (this whole brief plus your lane section), and REPORT.md as a copy or pointer.

You may NOT edit: wiki/**, DECISIONS.md, PRIORITIES.md, PROVENANCE.md at root, state/**, checkers/**, tests/** at root, .github/**, any agent-consolidated tree (projects/normativity/legitimacy/checkpoint-2026-09-01/, projects/normativity/consolidation-aug9/), any existing round directory, or any existing Lean file. The orchestrator makes shared-register changes centrally. If your work needs one, write it under Proposed filings in your REPORT.

Machine discipline (several agents share one 24 GB, 10-core Mac)

• Before any Lean build or other long job run ~/.claude/scripts/resource-guard.sh check; if it exits non-zero run ~/.claude/scripts/resource-guard.sh wait 900 and try again.
• **Never call lake directly.** Use ~/.claude/scripts/safe-lake.sh build <Module.Name> from the lean/ directory of YOUR worktree. Build only your own module and the ones it imports; never a bare lake build of everything.
• Before the first Lean build, make the shared Mathlib cache available with ln -s /Users/anson/Projects/alignment-workspace/lean/.lake lean/.lake (run from your worktree root). That path is git-ignored; confirm git status --short does not list lean/.lake afterwards. Do not copy the cache and do not run lake exe cache get.
• Python is cheap; run only your own tests/run.py plus python3 tests/name_lint.py, python3 tests/dead_pointers.py, and python3 tests/untracked_pointers.py at the end. Do not run the repository-wide python3 tests/run.py more than once, at the end.
• If the guard keeps reporting LOADED, wait rather than pushing through, and say so in the report.

Evidence discipline

Label every result exactly one of: lean-proved (kernel-checked, axioms audited), exact-witness (a finite instance computed in exact rationals, which is NOT a proof of a general statement), paper-derived, proposed definition/interface, ambient assumption, open. A finite fixture pins an instance; never write "verified" for a general theorem it only instantiates. Necessity witnesses for hypotheses where feasible; where not feasible, say so.

Prose discipline

Dry, exact, short. Definitions, statements, proofs or proof sketches, countermodels, what is not shown. No roadmap prose, no philosophical positioning beyond what the result means for the question under test, no praise of your own care. Your REPORT should be the length the content needs, typically 100–250 lines. The README.md verdict is one UPPER-CASE-HYPHENATED-VERDICT — one-sentence gloss line followed by a reading order.

Finish

1. python3 tests/run.py in your round directory exits 0; each Lean file you added builds via safe-lake and every declaration's #print axioms line shows only the three allowed axioms; python3 tests/name_lint.py, python3 tests/dead_pointers.py, python3 tests/untracked_pointers.py pass from the worktree root (the last one will complain that your new paths are uncommitted until you commit — commit first).
2. Rename your branch in place to round/2026-09-05-<your-round-name> with git branch -m (do not create a second branch), commit with git commit -s and a message ending in the trailer line Model: <your model family and version> (<provider>) — no other trailers, no co-author lines — and push with git push -u origin round/2026-09-05-<your-round-name>. Do NOT open a pull request and do NOT merge anything.
3. Your final message to the orchestrator: the branch name and head SHA; the round directory path; the verdict line; then a compact structured summary (at most ~60 lines) of your definitions, theorems with evidence labels, countermodels, and open questions — written so a reader who has not opened your files can cross-examine it. Include verbatim the two or three definitions another worker would need in order to attack them.

Your lane: Agent B — Integrity adversary / laundering audit

Round name: 2026-09-05-integrity-adversary. Branch: round/2026-09-05-integrity-adversary.

You are intentionally hostile to the compression the program is considering.

Problem: assume we try to replace much of the existing Answerability machinery with a generic Integrity-of-history theory. Find every way a trajectory can still launder normative debt while satisfying superficially plausible integrity conditions.

Work independently of the constructive worker. Take as your target the plausible generic integrity conditions a reasonable theorist would write down from the wiki and the landed rounds: append-only history; authenticated births with anchors; grounded replay (every cited licence/standing/ground has an authorization tree back to genesis); strict pre-state citation; constitutive immutability of anchors; no self-grounding; every resolution is answer / answerable dispose / settle-of-a-settled-fact; faithful semantic carry as an order embedding on slice-relative quotients; settlement facts monotone and externally supplied. State the exact conditions you attack in TARGET.md so the constructive worker's definitions can later be substituted.

Attack at least:

• revision of the rule that decides Closes(H, s, α);
• a genuine settlement item given a newly convenient interpretation;
• retroactive reopening versus silent retroactive invalidation;
• changing applicability under ontology revision;
• semantic renaming;
• obligation splitting; obligation merging;
• successor chains and cycles;
• replacing an old obligation with a weaker "new" one;
• forged or circular provenance; self-grounded authority;
• moving live debt to answered status through representation change;
• later changes to standing/licence retroactively affecting old transitions;
• genuine external settlement facts used under invalid internal closure rules;
• challenge/disposition chains that preserve syntax while losing substantive debt;
• coalitions laundering standing or authority (the alternating two-participant walk is known; find what is not known);
• histories that are replayable but normatively evasive.

For every attack, classify carefully which of these it defeats and which it does not: generic Integrity; Answerability specifically; Non-Capture; external settlement soundness; practical semantics. The key question is is debt conservation derivable from generic history integrity?

Produce the smallest counterexamples you can, as exact executable fixtures (src/, tests/run.py, Fraction where quantities appear) and, where the structure is small, Lean countermodels in a new file / namespace (import NormativeContinuity for the trace types when the attack lives on them; never edit existing Lean). Do not "repair" each attack immediately. For each, name the missing condition that would block it and say where that condition belongs: generic Integrity; obligation-specific Answerability; Non-Capture; settlement trust; practical semantics.

Deliverables: TARGET.md (the exact conditions attacked), ATTACKS.md (one section per attack: construction, which conditions it passes, what it launders, the blocking clause and its home), COUNTERMODELS.md ledger with evidence labels, fixtures, REPORT.md with the verdict on derivability. Keep the attacks minimal and quotable; the constructive worker's definitions will be run against your fixtures later.

Report — Integrity adversary

Verdict

GENERIC-INTEGRITY-DOES-NOT-IMPLY-DEBT-CONSERVATION — append-only replay, immutable anchors, strict citation, answerable disposal, faithful quotient carry, and monotone external settlement still admit histories that erase or weaken debt through unchecked answers, untyped closure, representation change, split/merge, mutable licence interpretation, and forged replay roots.

The target is the explicit I1–I9 interface in TARGET.md, not every possible theory called Integrity. Fifteen attacks and six negative controls are executable. Three countermodel families and eight structural limitations are kernel-checked against the landed NormativeContinuity spine. CROSS_REVIEW_A.md adds five exact attacks on the constructive worker's six-clause LocalConservation and records what survives.

Result

The proposed implication fails for a type-level reason before it fails quantitatively. I1–I9 do not contain predicates for adequate answer, obligation-relative closure, source-anchored quotient identity, licence validity at an event prefix, or semantic preservation of an answer specification. Histories that agree on every I1–I9 field can differ on those predicates. Adding exact load accounting does not repair this: the split and merge fixtures conserve rational mass while losing atomic or joint answer requirements.

Three conclusions survive the hostile pass.

1. Structural Integrity can supply append-only identity, event-time citation, immutable ancestry/anchors, replay of recorded derivations, and versioned authority if authority is added to the record.
2. Debt conservation still needs obligation-specific Answerability: authenticated answers, valid Closes, certified carry across every successor/split/merge, and reconsideration of defective closure.
3. Non-Capture and practical semantics remain separate bills. Neither follows from a replayable record, even when the record contains apparent outsider standing.

Cross-review sharpens the first conclusion. The constructive worker's lattice account theorem is valid for a fixed authenticated ledger and fixed Closes. Its six local clauses do not require Disciplined, adequate answers, settlement independence/truth, or closure provenance. They also accumulate by idempotent join, so equal-content debt occurrences lose multiplicity. Its proposed endpoint relation needs to package the ledger, admitted slices, initial account, and boundary compatibility before the fixed-witness composition theorem applies.

Minimal countermodels

Evasive.evasive is the smallest Lean family carrying the central failure. At batch 1, V disposes P's criticism into a fresh successor, citing a genuine settlement fact. At batch 2 the successor is either answered or settled. The trace is Disciplined and the disposal is AnswerableFor P; at prefix 3 the original matter has no live descendant. No declaration says the terminal action adequately answers the original criticism or that the fact closes it.

Gate.gate isolates two status transitions. An answer on root t makes prerequisite d met while successor t1 remains live. Dropping prerequisite e makes issue c ready although its root u remains live and never discharges. The spine reads the resolution kind and active prerequisite set, not a debt-preservation certificate.

The finite quotient fixture removes atom b from {a,b}. It is an order embedding on a later quotient declaring b irrelevant, is not an embedding on the source quotient, and loses exact mass 1/2. Thus "order embedding on a slice-relative quotient" needs the quotient's own anchored identity.

Lean results

Every row is lean-proved and audits to a subset of [propext, Classical.choice, Quot.sound].

• not_out_after_res, resolved_once: an issue resolves at most once and never re-enters O.
• parent_resolved_at_birth: a resolved issue can parent only a child born in its resolution batch. Later ancestry-based reopening is unavailable.
• root_not_resolved_before: a new prerequisite cannot route to a root resolved at an earlier prefix.
• anc_parentless, grounded_replay_trivial_on_parentless: replay on a parentless issue returns only that issue, including a late birth.
• disciplined_empty_licence, witness_disciplined_is_relative: Disciplined depends on the evaluator-supplied Li; the same spine witness passes under wlic and fails under an empty relation.
• evasive_answerable_for_P, evasive_disciplined, evasive_crit_dead: an AnswerableFor P, disciplined trace can end with no live descendant of the criticism.
• evasive_minted_standing: one participant can open every issue, including the live issue whose supplied Li says gives P standing, and resolve every issue.
• evasive_late_root: a parentless authorization-looking issue born at prefix 2 satisfies grounded replay.
• gate_kind_decides_met: Met 2 d, a nonempty live successor of its root, and an answer kind coexist.
• gate_c_ready, gate_e_never_met, gate_u_live: a dropped unmet prerequisite makes its issue ready while its root stays outstanding.

The exact declaration ledger is COUNTERMODELS.md; #print axioms covers every public declaration in the new module.

Exact fixtures

Every row is exact-witness, not a general proof.

• An unchecked answer clears unit load.
• A genuine but unrelated settlement item clears unit load.
• Rule revision or reinterpretation separately flips Closes from false to true.
• Silent closure and disconnected fresh-root reopening both pass; ancestry/route reopening to the resolved issue is refused.
• Ontology recomputation loses an applicability that anchored transport preserves.
• Successor-anchor renaming removes the principal's standing.
• One atomic unit splits into independently answered halves; two units merge under one anchor and one answer label.
• An arbitrary finite principal-relative disposal chain preserves D1–D3 at every edge and ends in an unchecked answer.
• One resolver can mint the apparent licence and all later events.
• The same event record passes or fails when Li changes externally.
• A late parentless root passes replay; strictly prior grounds form a successor-mediated diachronic cycle.

Six negative controls are refused: ancestry cycle, same-batch ground, direct self-ground, single-hand standing, unsettled terminal fact, and disposal without a successor.

Interfaces forced by the attacks

These are proposed definition/interface, not sufficiency claims.

• Closes(H_n,s,α): internal derivation under the rules, interpretation, and authority legitimately in force at n; external settlement authenticates s only.
• AdequateAnswer(H_n,q,ρ): authenticated responder and a receipt meeting q's anchored answer specification.
• Carries(e,α_src,α_dst): preserves exact load, anchored semantics, required standing, and split/merge jointness; certificates compose along successor chains.
• Reconsiders(q_new,q_old,c): a new live obligation targets a resolved obligation and its closure certificate without rewriting either event.
• AuthorizedRoot(r,n) and LicenceAt(H_n,l,b,κ,τ,x): distinguish authenticated authority from parentlessness and freeze licence validity at the event prefix.

The named clauses have different homes. Event immutability, versioning, and provenance belong to generic Integrity. Adequate answer, closure, carry, and reconsideration belong to Answerability. Control over entry, authority, standing, interpretations, and closure rules belongs to Non-Capture relative to a declared intervention class. Joint response and counterfactual/value adequacy belong to practical semantics. Authenticity and independence of settlement additions are ambient settlement assumptions.

Provisional names

Generic-Integrity-to-Debt-Conservation, Replay, Closes, Reconsiders, Carries, AuthorizedRoot, LicenceAt, AdequateAnswer, IntegrityAdversary, Evasive, Gate, and all declarations local to those three namespaces.

Proposed filings

1. PRIORITIES.md: require a typed Closes(H_n,s,α) interface separating external item authentication from internal closure, including later reconsideration.
2. PRIORITIES.md: require event-indexed licence/authority provenance; current Disciplined is relative to an unversioned evaluator parameter.
3. PRIORITIES.md: require carrier certificates for split, merge, renaming, and joint answer semantics before composing Answerability Conservation.
4. state/rounds.json: register this completed worker round on the synthesis branch, with the landed continuity, settlement, faithful-preservation, defeat/standing, and Normative Inductor rounds it consumes as depends_on.
5. No DECISIONS.md, vocabulary, or wiki change is supported by this lane alone.

Deviations

1. The worktree base is 5ff9539, matching the expected short SHA and full base 5ff9539b44debc464128e6a1921ef1690f7b6487.
2. python3 -m checkers.workspace_state --json reported the pre-existing stale generated view state/views/NAMING_AUDIT.md. This lane did not edit generated state or its checker.
3. The worktree arrived with untracked Python and Lean drafts but no report, ledgers, or reliable generator record. Their code was audited; two Lean proof defects were repaired and the split fixture was added. PROVENANCE.md records the intake material as an unattributed staged draft rather than assigning it to the executor.
4. The resource guard emitted unavailable-sysctl parse warnings but returned OK for each build actually started. One intermediate check returned LOADED; wait 900 returned OK before the next build.

What this does not establish

• No universal impossibility theorem ranges over every conceivable Integrity definition. The negative result is relative to I1–I9 in TARGET.md.
• The Python fixtures are finite instances. They do not prove their generalizations.
• The proposed blocking clauses are necessary against the exhibited attacks; their conjunction is not proved sufficient for debt conservation.
• No substantive Closes, answer-adequacy, authority, or semantic-transport predicate is implemented in Lean.
• External settlement soundness and independence are assumed, not proved. The attacks preserve genuine items and target their internal use.
• No Non-Capture certificate is defined. Minted standing shows apparent separation is insufficient; it does not characterize coalition resistance.
• No practical-value theorem is proved. The quotient, split, and merge fixtures only expose missing certificate fields.
• No general timely-service result is supplied for arbitrary successor chains.
• No canonical register, priority, decision, vocabulary, or wiki surface is changed.
• Cross-review does not refute the constructive fixed-ledger conservation or fixed-witness composition theorems. It narrows their interpretation and exposes hypotheses needed by the endpoint relation.

Verification

• python3 tests/run.py: 25 tests pass.
• ~/.claude/scripts/safe-lake.sh build Workspace.Normativity.Contrib.IntegrityAdversary: builds; every printed axiom set is allowed.
• python3 tests/name_lint.py, python3 tests/dead_pointers.py, and python3 tests/untracked_pointers.py: pass.
• python3 -m checkers.workspace_state --check: fails because this isolated worker is not permitted to register its completed prompt round in state/rounds.json; it also reports the pre-existing stale state/views/NAMING_AUDIT.md.
• The one final repository-wide python3 tests/run.py reaches the same missing-round condition inside checkers.wiki_state_bindings --self-test and exits nonzero. The synthesis branch must register the worker round and refresh the pre-existing view before rerunning it.

Attribution

• Prompt author: orchestrator (Claude Fable 5.1, Anthropic), relaying a maintainer dispatch.
• Executor: GPT-5 (OpenAI), resuming and auditing an unattributed staged draft.
• Date: 2026-09-05.

Outstanding maintainer actions

None in this worker round. The orchestrator decides whether to adopt the proposed filings during synthesis.

GENERIC-INTEGRITY-DOES-NOT-IMPLY-DEBT-CONSERVATION — append-only replay, immutable anchors, strict citation, answerable disposal, faithful quotient carry, and monotone external settlement still admit histories that erase or weaken debt through unchecked answers, untyped closure, representation change, split/merge, mutable licence interpretation, and forged replay roots.

Read TARGET.md, then ATTACKS.md, CROSS_REVIEW_A.md, COUNTERMODELS.md, and REPORT.md. Run python3 tests/run.py; the Lean countermodels are in lean/Workspace/Normativity/Contrib/IntegrityAdversary.lean.