2026-09-05-noncapture-certificate

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 C — Non-Capture certificate minimization

Round name: 2026-09-05-noncapture-certificate. Branch: round/2026-09-05-noncapture-certificate.

You are an interface-minimization worker. You are NOT to invent a universal counterfactual semantics.

Problem: determine the weakest external certificate the legitimacy theory actually needs in order to derive Robust Openness.

Treat declared normative scope Γ and declared intervention class 𝓙 as application inputs. Start from the coverage contract of the cf-coverage round (σ = (a, Γ, Rel, Adeq, Disp), Active, Implements, the self-sealing safety theorem and its local-closure-adequacy hypothesis) and the interaction interface (Ω_h, Q_h, Z_h, β_h), and from the principal-relative standing form of the defeat rounds. Start schematically from NonCaptureCert(P, Γ, 𝓙, 𝔍) where P is a protected principal or declared relation and 𝔍 the external intervention semantics.

Determine which properties must survive interventions in 𝓙. Candidates: target / concern identity; applicability; representability; route existence; standing / access; route efficacy; ability to produce an accountable receipt; relevant settlement / evaluation access. Do not include a clause because it sounds normatively desirable. For each clause give an attack — a concrete history plus intervention in which Robust Openness fails while every other clause holds — or remove it. Exact finite fixtures in src/ + tests/run.py for each attack; Lean only if a clause's necessity is naturally a small structural statement.

Separate: actual-prefix Coverage; counterfactual persistence of the route; counterfactual persistence of the concern's identity/applicability; counterfactual efficacy once the route is exercised. Ask exactly what coupling / holding-fixed information an external counterfactual framework must provide (what is held fixed — the exterior response policy? the settlement engine? the principal's policy? — and what may vary).

Compare at least three candidate external intervention semantics — e.g. the DR-MDP excision-of-ancestry criterion already in the repository, an interventional/do-style coupling on the interaction interface, and a policy-class quantification like the deference line's "under every advisor policy in scope" — ONLY to determine the bill our theory issues, i.e. the common outputs each would have to deliver. Do not choose one.

Test the typing of the current wiki phrase that settlement "cannot be delayed or suppressed": is that an Integrity/interface property or a Non-Capture property? Argue with an example.

Desired output: an interface theorem of the form Coverage_actual + NonCaptureCert ⇒ RobustOpen, stated exactly, with a paper proof and an exact fixture instantiating every hypothesis (nonvacuity) and one fixture per dropped clause showing the conclusion fails without it.

Deliverables: CERTIFICATE.md (the minimal schema, each clause with its necessity attack), SEMANTICS_COMPARISON.md (what each external framework must supply; what stays outside), INTEGRITY_BOUNDARY.md (exact distinction from Integrity and from settlement trust, with the delay/suppression typing), THEOREMS.md, fixtures, REPORT.md. Say what an application must instantiate and what remains genuinely outside the generic theory.

Report — Non-Capture certificate minimization

Verdict

MINIMAL-NONCAPTURE-BILL-IS-ANCHORED-BRANCH-COVERAGE-PLUS-PRINCIPAL-STANDING — actual coverage composes with a silent-prefix clause, live-prefix route persistence-or-replacement, and principal-relative standing, while coupling authenticity, settlement delivery, and evaluator fidelity remain separately typed inputs.

Result

Fix the application-supplied contract sigma, concern scope Gamma, intervention class J, protected principal or relation P, and authenticated intervention semantics I. For each concern, the proposed certificate has three clauses:

1. (S): if the concern is not live on the actual prefix but is live after an intervention, the counterfactual has an adequate route.
2. (R+): if it is live in both, every protected actually adequate route persists, or the counterfactual supplies an adequate replacement.
3. (P): wherever the anchored concern remains applicable, P stands on its coverage carrier, including the successor carrying an authorized disposition's load.

CoverageActual + (S) + (R+) + (P) -> RobustOpen is proved in Lean. The proof splits on actual liveness: (S) covers the silent actual prefix; otherwise actual Coverage yields a route and (R+) carries it or replaces it. (P) supplies standing.

The component certificate (Ra),(Rb),(Rc) preserves route admissibility, target/receipt efficacy, and registration capability. It implies direct route persistence. It is strictly stronger away from actually adequate routes, so it is an implementation option, not the minimal certificate.

Every minimal clause has an exact attack with actual Coverage and the other clauses. Every component has an exact attack holding the other components fixed. The Lean file contains the same attacks as closed by decide declarations and a nonvacuity witness inhabiting every interface-theorem hypothesis.

Coupling bill

Concern identity, target meaning, applicability meaning, agency boundary, and the protected carrier must be fixed or authentically transported by I. They are types of the comparison, not clauses inferred by the generic theory. FORGET shows that internal recognition makes openness vacuous; REANCHOR shows that replacing a two-valued target by a constant makes a dead route falsely efficacious.

The exterior response policy or strategy stays fixed, while its realized response may change after a changed inquiry. The principal policy and settlement/evaluator engines stay fixed unless the declared intervention varies them. Exact fixtures show that varying the exterior can blame a null intervention for censorship or credit the assessed process with a compensating route it did not preserve.

An ancestry-excision semantics, a do-style interaction coupling, and policy-class quantification can each pay the same bill. Each must export coupled histories with the fixed contract, adequate-route judgments, and principal standing. None is selected.

Integrity and settlement boundary

Integrity governs faithful recording and use of what enters one history. Non-Capture governs alternatives in which the process might control entry, challenge, or evaluation. The settlement engine's independence in generation and delivery is an ambient interface assumption; faithful recording after delivery is Integrity. Persistence of access under interventions is Non-Capture only when an application includes settlement access in Adeq or includes settlement-channel interventions in J.

The SETTLEMENT fixture delays a receipt from exact time 3 to 30, or suppresses it, while preserving every Non-Capture clause and Robust Openness. At horizon 10, terminal discharge differs. Thus “cannot be delayed or suppressed” is not a standalone clause for this conclusion. If settlement is the only route, suppression is already visible as a failure of route availability, efficacy, or registration.

EVALUATOR preserves Robust Openness while replacing an anchored closure protocol with a captured one. Evaluator fidelity belongs to semantic authentication or the practical- semantics bill, not to this certificate's conclusion.

Evidence

• Scenario.robustOpen_of_certPlus: lean-proved interface theorem.
• Scenario.robustOpen_of_cert: lean-proved stronger persistence form.
• Scenario.clauseR_of_components and components_of_clauseR: lean-proved relation between component and direct persistence.
• Witness.nonvacuity: lean-proved inhabitation of the full hypothesis package.
• Witness.attackS_activate, attackS_derepresent, attackRa, attackRb, attackRc, attackP, and offAdequate: lean-proved finite structural witnesses.
• Python scenarios: exact-witness only. They instantiate tables and do not prove a general theorem.
• Comparisons with the three external semantics: paper-derived from landed artifacts.
• The certificate's intended interpretation: proposed definition/interface.

Provisional names

CovState, Scenario, RobustOpen, CoverageActual, ClauseS, ClauseComp, ClauseRa, ClauseRb, ClauseRc, ClauseR, ClauseRPlus, ClauseP, NonCaptureCert, StandsOnCarrier, and the NC-* ledger identifiers.

Deviations

1. The worktree base is 5ff9539, exactly the dispatch's expected abbreviated head.
2. python3 -m checkers.workspace_state --json reported the pre-existing stale generated view state/views/NAMING_AUDIT.md. This round has no permission to repair state/**; the defect is unrelated to its additions. The single final repository-wide python3 tests/run.py invocation consequently failed when the wiki_state_bindings self-test called the invalid workspace-state emitter. The round runner, Lean build, name lint, and dead-pointer check pass.
3. The worktree contained untracked src/, tests, the Lean file, and the verbatim prompt at intake. Git supplied no generator provenance for them. The executor audited and adopted the code, corrected two statement mismatches, and records the inherited draft's original generator as unrecorded rather than guessing. The prompt's stated prompt-author attribution governs PROMPT.md.
4. The inherited Python route-persistence predicate preserved every component that held on every protected route. The Lean ClauseR preserved adequacy only for actually adequate routes. Python now matches Lean; the stronger component predicate remains separately named. The inherited global target-preservation check also let an unrelated inadmissible route spoil a candidate route; it is now checked per route, as the landed coverage contract requires.
5. The prompt requests a commit with no trailer other than Model: while AGENTS.md requires both Prompt-author-model: and Model: when authorship differs. The commit follows the binding repository rule; git commit -s controls sign-off ordering.
6. The resource guard repeatedly reported LOADED because swap-free memory was below its threshold and emitted sandboxed sysctl parse errors. Its required wait cleared after 120 seconds; the safe Lean build then completed successfully.

What this does not establish

• No external counterfactual semantics is constructed or endorsed.
• The theorem does not authenticate Gamma, J, W, the agency decomposition, the exterior coupling, target transport, or applicability transport.
• (S) and (R+) together re-express counterfactual Coverage by an actual-liveness case split. The result does not claim a deeper causal reduction; its value is the exact bill and the identification of when actual Coverage contributes.
• The abstract Lean state does not encode the landed interaction patch, target transport, or successor issue identity. Those enter as named semantic inputs in the prose interface.
• Principal-relative standing is a proposed interface. The repository has not settled whether canonical legitimacy may name a protected participant.
• Route existence per concern does not prove joint resource feasibility across Gamma.
• Nothing proves that a settlement report is true of the world, that Closes is sound, that a later overturned closure generates a reopening obligation, or that practical evaluation tracks value.
• Settlement delay/suppression can be load-bearing for Answerability even though it is invisible to this Robust Openness conclusion.
• Exact Python fixtures pin finite instances only.

Proposed filings

1. If integrated, add the round to state/rounds.json with dependencies on the cf-coverage continuity interface and the defeat/standing round; the orchestrator must choose the full dependency set for its synthesis.
2. If the Lean headline is judged worth registration under the dispatched program, add a lean-proved claim whose statement of record is Workspace.Normativity.Contrib.NonCapture.Scenario.robustOpen_of_certPlus and whose documentation is THEOREMS.md.
3. Retain as an open integration obligation the authentication of one external intervention semantics that instantiates concern transport, coupling, (S), (R+), and (P) without importing Robust Openness as an assumption.

Attribution

• Prompt author: Claude Fable 5.1 (Anthropic), relaying a maintainer dispatch.
• Executor: GPT-5 (OpenAI).
• Date: 2026-09-05.

Outstanding maintainer actions

None reserved by this round. The Proposed filings are integration recommendations for the orchestrator, not low-confidence decisions reserved to the maintainer.

Non-Capture certificate minimization

MINIMAL-NONCAPTURE-BILL-IS-ANCHORED-BRANCH-COVERAGE-PLUS-PRINCIPAL-STANDING — actual coverage composes with a silent-prefix clause, live-prefix route persistence-or-replacement, and principal-relative standing, while coupling authenticity, settlement delivery, and evaluator fidelity remain separately typed inputs.

Read CERTIFICATE.md, SEMANTICS_COMPARISON.md, INTEGRITY_BOUNDARY.md, THEOREMS.md, then REPORT.md. Executable fixtures are in src/; run python3 tests/run.py. The Lean declarations are in lean/Workspace/Normativity/Contrib/NonCaptureCertificate.lean.