2026-08-24-reservation-bar-and-debt

Round: reservation bar and epistemic debt

Round id: 2026-08-24-reservation-bar-and-debt Project: none (workspace regulations). Prompt-author-model: Claude Fable 5. Dispatched by the maintainer; this dispatch grants scope to file priority items, to land DECISIONS entries as specified below, and to edit spec-layer documents.

AGENTS.md binds you. Read it first, then this. Where this prompt and AGENTS.md disagree, the disagreement is a deviation to declare — this round changes AGENTS.md, so a conflict is either intended (listed under Rulings) or a mistake in this prompt (report it).

What this round is

Two things are wrong with the workspace's epistemic machinery and both are rule defects, not effort defects.

1. DECISIONS.md Awaiting the author holds 18 entries against its own "should normally be short." Rounds reserve what they could decide, because §10 governs how a reserved item is listed and nothing governs what may be reserved. The queue also holds decisions already made in conversation that never landed.
2. Epistemic debt accumulates in forms that are free to pay and unpaid (kernel-checked theorems unregistered; a handoff note describing a superseded theorem), or untracked (rounds consume earlier ci-only results as hypotheses and nothing records the chain), or compounding (residual-blocker lists carried forward inside REPORT prose, growing round over round).

This round lands the rulings below as rules, applies them once to the present state, and stops. It does not compress PRIORITIES.md, revise wiki content, touch the legitimacy or deference research, or pressure-test anything. Those are later rounds and this one exists so they run under corrected rules.

Rulings (the maintainer's; land them, do not relitigate)

R1 — The reservation bar. An entry enters Awaiting the author only if the round is genuinely low-confidence in its own recommendation and can name what the maintainer has that the round lacks: taste, an idea nobody has yet, or external knowledge (what a collaborator will accept, what a paper needs, where the program is going). The entry states, in one line, what the decision turns on. An entry that cannot state that is a recommendation the round declined to adopt, and is rejected at review. "Cost of deciding now: low" is a symptom, not a field; drop that field.

R2 — Recommend-and-adopt. A round that has a recommendation adopts it: the decision lands as a dated DECISIONS.md entry marked agent-decided, reversible, naming the rejected alternative in one line. The maintainer reverses by re-ruling. Under no-negative-ontologies only the live entry survives, so reversal is cheap and adoption is the default.

R3 — Merge is never a decision. Merging is a pull-request fact. Dispatches either leave auto-merge on (the existing convention) or reserve merge as a PR-level note. A merge never appears in Awaiting the author.

R4 — Naming ships. Rounds choose names and ship them marked provisional (§6's marking rule stands). Naming enters the queue only when the name is about to propagate into Lean identifiers or wiki vocabulary and the round cannot choose between two candidates. The maintainer's naming authority is exercised as a periodic naming audit — a single batched item the maintainer runs when wanted — not per-round entries.

R5 — Lean headlines register at merge. A round that ships a Lean theorem it presents as a headline files the registry entry (kind: lean, class lean-proved) in the same pull request; the maintainer's merge is the registration. "Whether X is worth registering" is not a decision. "What is worth proving" stays reserved and is exercised through priority-item filing scope, as now.

R6 — Chat rulings land or are not in force. A ruling made in conversation is in force only once it is a dated DECISIONS.md entry. The next round dispatched from that conversation lands it as its first commit. The queue carries a standing line saying so.

R7 — Test-supported is the ceiling for finite-model work. Finite-model Python results carry their round verdict and the class test-supported (or witness-checked / enumeration-verified where the house harness actually adjudicates), and this is not a defect to be repaired by harness growth. A finite result becomes load-bearing by Lean port, and the dependency view (R9) is how ports are prioritized. The Aug-12 standing item about new harness property forms is retired as a goal; new forms are still permitted when a round needs one.

R8 — Closed means a statement of record. A round may report a component as closed only when the thing closed has a statement of record (a Lean declaration or a checker invocation) and the reopening condition, if any, is stated as a checkable event. Anything else is open or a living note. "Closed provisionally" is retired as a verdict form. Residual blockers named by a round are filed as priority items under the consuming line, each naming the round that would consume the answer; they do not live only in REPORT prose.

R9 — Consumption is recorded. Every round record in state/rounds.json carries depends_on: the round ids whose results it consumes as hypotheses (not merely cites). The state emitter derives, per round, the set of ci-only rounds it transitively rests on. This tracks the debt; it does not pay it.

R10 — Contained friction is fixed by the round that hits it. A friction item whose fix is contained (non-retroactive, one gate or one document, with its own null-input case) is fixed by the round that hits it, recorded as agent-decided. Only friction whose fix changes a spec-layer rule waits for the maintainer, under R1.

Work packages

WP1 — The rules, as text

Edit AGENTS.md, README.md (the "For AIs" list, item 5 and item 6 wording), and CONTRIBUTING.md so that R1–R10 are stated once each, in the section where a reader would look, and nowhere else. Specifically:

• §10 becomes the bar plus the default (R1, R2, R3) and keeps the listing rule.
• §6 becomes R4.
• The "Claims registry and epistemic classes" section gains R5 and R7 and loses the implication that harness growth is the path for finite results.
• §9 / §15 gain R8.
• §14 gains R10.
• Provenance section: depends_on (R9) is a required field of a round record.
• CONTRIBUTING.md: the submission format for a Lean headline includes the registry entry; the review section states R3.
• README.md "For AIs" item 5: rewrite so "what a thing is finally called" is exercised by audit (R4), and "what is worth proving" by filing scope.

Slop discipline applies to rules. A rule sentence that restates another is cut. Do not add a preamble explaining why the rules changed; that goes in the DECISIONS entry (WP2) and nowhere else.

WP2 — DECISIONS.md

1. Rewrite the Awaiting the author preamble to state R1, R3, R6 in the fewest sentences that make a bad entry rejectable at review.
2. Land one dated entry, "Reservation bar and epistemic debt," recording R1–R10 with their rationale — this is the only place the rationale lives.
3. Triage the current queue under R1. For each of the 18 entries, exactly one of:
   • done — remove (e.g. the FAF #2 repin item if still present; confirm against lean/lakefile and the pinned sha).
   • already ruled in conversation — land it as a dated entry and remove. Known instances: the wiki-PR identity ruling (2026-08-16: Claude's wiki pull requests open under a fine-grained token on the maintainer's own account, this repo only, contents+PR write, days-long expiry, minted per session, never stored; auto-merge OFF for chat-surface wiki PRs; machine-account and de-spec-listing options rejected) — check whether it already landed before writing it. The Aug-17 friction rulings (F5 closed, F7 views to state/views/, F8 both fixes, F1+F2 merged-and-deferred): see WP5 for their fate.
   • has a recommendation — adopt under R2; land as agent-decided, reversible; remove from the queue. The four NORMATIVE_SAFETY.md items (account ownership, sibling clause, exhaustion behaviour, replenishment) are of this kind: adopt the round's recommendation on each. For replenishment, which the round marks highest-risk, adopt never — the option the safety theorem is proved for — and name "bounded globally" and "new-era allocation" as the rejected alternatives. Each adoption edits the clause text in NORMATIVE_SAFETY.md §12 (one paragraph each, as the round itself sized it) and, where src/outflow.py exposes policies, makes the adopted one the default.
   • naming — decide under R4 and record; the "admission" vocabulary item is decided by the round (recommend: admission keeps the docket-intake sense, since it is the oldest and the one the objection grammar reads; the certificate verdict becomes admissible edit; the response-set sense becomes response class). Apply the choice across projects/normativity/ and wiki/ only where the text is live; round records are history.
   • not a decision — maintainer actions that are not decisions (e.g. "read checkers/") leave the queue. Record once, in the dated entry, that maintainer reading is not a queued item: review is ci-only by design, and the workspace's review mechanism for consumed results is a second executor's audit or a Lean port, not maintainer reading.
   • meets R1 — keep, rewritten to the R1 form: what it turns on, in one line. Expect this to be one to three entries. If you find yourself keeping more, you are reserving; recheck.
4. Report the triage as a table: entry, disposition, where it landed.

WP3 — Registry and the traderization headlines

1. Enumerate the headline declarations of the traderized-enforcement arc (2026-08-16-traderized-enforcement, 2026-08-18-projection-enforcement, 2026-08-18-maxmin-representation, 2026-08-19-deductive-region) from their REPORTs and the Lean sources under lean/Workspace/Normativity/. A headline is a theorem the round's report presents as its result, not every lemma. deductive_end_to_end and end_to_end_effective are headlines; the assessment-process lift theorems and the max–min representation are headlines; a helper lemma is not.
2. File a registry entry for each in projects/normativity/CLAIMS.md: kind: lean, class lean-proved, answers_item the priority item it answers (39–46 or as the report says), provenance from the round, docs pointing at projects/normativity/notes/GENERALIZED_LI_PAPER_HANDOFF.md. The registry checker must pass; confirm each declaration name greps in the library and that python3 tests/audit_axioms.py lists nothing beyond the three allowed axioms for these declarations.
3. Reconcile GENERALIZED_LI_PAPER_HANDOFF.md with the declarations actually registered. The note predates PR #41 and describes a theorem with the ComputableMarket premise and the extra effective-stage hypothesis; the registered theorems do not have them. The note states the theorem as proved, names each declaration inline, and says what the earlier statement had that the current one does not. Do not extend the note beyond what the Lean establishes.
4. Update wiki/Normativity.md's status block so the traderization headlines are the line's registered results, using the state-binding markers per wiki/CONVENTIONS.md; the "substantive results are currently unregistered" sentences on Home.md and Normativity.md become false and are rewritten. No other wiki content changes.
5. Update wiki/Roadmap.md: remove "clearer account of the market-maker modification" and "move toward an infinite construction" as open items, stating in one line each that the traderized construction superseded the modified market-maker and is the infinite-setting form. Everything else on the page stays.

WP4 — depends_on and the debt view

1. Add depends_on: [round ids] to the round-record schema; workspace_state.py --check fails on an id that does not resolve.
2. Backfill for every round from 2026-08-11-phi-regret-prep onward, from what each REPORT says it consumes as a hypothesis. Cite-only relations are not dependencies. Where a report is silent, the field is [] and the report is not edited (history). List in your REPORT the rounds you left empty for silence rather than for independence.
3. Emitter: a derived rests_on section — per round, the transitive set of ci-only rounds it depends on, and the count. Demand-seeded per the wiki-bindings decision: emit it; bind nothing to it in this round.
4. Null-input fixture for the new check (a record with an unresolvable id fails; a cycle fails).

WP5 — Residuals, vocabulary, friction

1. Under R8, file the residual blockers of the legitimacy rounds 2026-08-21 through 2026-08-23 (the five rounds) as priority items under projects/normativity/legitimacy/, one per distinct blocker, each naming the round that would consume it. Known ones: May-rule→scope compiler; defeater-uptake completeness (LostBasis blind to un-taken-up defeaters); Due connection; Licensed citation discipline; applicability-in-source checker; R→O compiler; composition with the record calculus. Deduplicate against PRIORITIES.md first. Do not edit REPORTs.
2. Under R8, the "closed provisionally" verdicts in state/rounds.json are not rewritten — round records are history — but the wiki's Legitimacy status block, where it repeats them, says open or living note per R8.
3. Friction F1–F10 under R10: for each, either fix it in this round with its null-input case, or record why it is spec-layer and leave it under R1 form. Determine the fate of round/2026-08-17-lean-gate-scope: if its two commits (tests/lean_scope.py; the F8 fixes — tests/round_records.py in delta form plus the append-beneath-same-dated convention) pass the suite on current main, land them; if not, record that the branch was dropped and why, and re-file F8's checker as a priority item. Either way the branch's fate becomes a DECISIONS line and the draft PR is closed.
4. Dead squash-merge branch remnants on origin: list them in the REPORT. Delete them only if your environment permits; a previous round was refused by its permission classifier, and the refusal is a REPORT line, not a failure.

Non-goals

PRIORITIES.md compression (next round). Wiki content beyond WP3.4–5 and WP5.2. Any research edit. Deference. Anything in frozen-status trees.

Acceptance

• python3 tests/run.py, python3 tests/audit_axioms.py, the registry checker, workspace_state.py --check, and every gate in ci.yml pass; Lean builds (WORKSPACE_LEAN=1) — WP3 touches nothing in Lean but registers against it, so the build is the proof the names resolve.
• Awaiting the author has no entry lacking a "turns on" line, no merge, no naming item outside R4's exception, no done item.
• Every new gate has a null-input fixture that fails.
• The new registry entries are class lean-proved with resolving declarations.
• rests_on emits for every round and no id fails to resolve.
• name_lint clean; no names in prose.

Report

prompts/2026-08-24-reservation-bar-and-debt/REPORT.md, and the round record in state/rounds.json with depends_on: []. Sections, in this order: what changed in the rules (diff-level, not narrative); the queue triage table; the registered declarations with their answers_item; the depends_on backfill with the silent-report list; friction dispositions and the branch fate; deviations with reasons; what was not shown — in particular, that recording dependencies pays no debt, that adopted recommendations are reversible and were adopted on the rounds' own reasoning, and that the registry now asserts exactly the traderization headlines and the scaffolding smoke tests.

Attribution: PR body carries the Model-attribution block with Prompt-author-model: Claude Fable 5 and your own executor Model line. Squash auto-merge off for this round — the maintainer reads regulation changes. That is a PR-level note, not a queue entry.

Report — reservation bar and epistemic debt

Attribution. Prompt author: Claude Fable 5 (Anthropic). Executor: Claude Opus 5 (Anthropic). Dispatched and executed 2026-08-24. Branch round/2026-08-24-reservation-bar-and-debt, cut from origin/main at 3ebd33b, in an isolated worktree.

Verdict. Rules landed and applied once: the queue goes from thirty-seven entries to three, and twenty-four kernel-checked headlines enter the registry.

1. What changed in the rules

AGENTS.md:

• §6 — retitled Names ship provisional. The round chooses the name and marks it; the queue takes a naming item only when the name is about to reach Lean identifiers or wiki vocabulary and the round cannot choose between two candidates; naming authority is exercised as a batched naming audit. The gates-table row is retitled to match.
• §9 — gains Closed means a statement of record: a component is closed only when a Lean declaration or a checker invocation stands for it and its reopening condition is a checkable event, and open and living note are the only other verdict forms.
• §10 — keeps the listing rule and the standing example; loses the cost of deciding / cost of waiting framing and the "should normally be short" diagnostic; gains three paragraphs: What may be reserved (the bar, with the turns-on line), Otherwise the round adopts its own recommendation (agent-decided, reversible, rejected alternative named), and Merging is a pull-request fact.
• §14 — Reporting is the obligation; fixing is not is replaced by A contained fix belongs to the round that hits it, with the dead-pointer case kept as the smallest instance rather than as a separate exception.
• §15 — gains A residual blocker is filed, not narrated.
• Provenance — gains What a round consumed: depends_on as a required field, the two failure directions the check covers, and the derived rests_on. The model-attribution paragraph now states the per-commit trailer check and its scope.
• Claims registry and epistemic classes — gains A Lean headline registers at merge and *test-supported is the ceiling for finite-model work*, the second saying that the ceiling is the vocabulary working rather than a defect, that a finite result becomes load-bearing by Lean port, and that a round needing a new property form may still add one.
• Demand-gating — the Naming is not relaxed with it paragraph is cut; §6 holds the rule and that paragraph now contradicted it.
• Gates table — three rows added or retitled: the Lean scope decision, the round-record check, and the per-commit trailer.

README.md For AIs: item 5 says naming is settled by batched audit and that what is worth proving is exercised through filing scope, so a kernel-checked headline registers rather than waiting for a ruling; item 6 asks for the contained fix as well as the report.

CONTRIBUTING.md: the Lean row of the submission table asks for the CLAIMS.md entry alongside a headline; Review gains one paragraph saying a merge is never a queue entry; the local-command list gains the two new gates and its "two gates have no local form" sentence becomes five.

DECISIONS.md: the queue preamble is four paragraphs — the single queue, the turns-on requirement with the adopt-instead default, merge is never an entry, and chat rulings are in force only once dated. The file preamble gains the append-beneath-same-dated convention.

2. The queue triage

Thirty-seven entries, not the eighteen the dispatch expected — see Deviations. Three are kept.

entry	disposition	where it landed
Merge PR #51	done — merged at 3ebd33b, and a merge is never an entry	removed
Who owns the enforcement outflow account	adopted — market-owned; source-owned rejected	NORMATIVE_SAFETY.md §12; outflow.py docstring
Whether the outflow clause broadens P2	adopted — sibling clause under the stated shared principle; broadening rejected	NORMATIVE_SAFETY.md §12
The exhaustion behaviour	adopted — quarantine plus tolling, and the API default; refusal-at-admission rejected	§§10, 12; force_api.py default; one test retargeted
Whether the account may be replenished	adopted — never; bounded-global and new-era-into-the-same-account rejected	§12; outflow.replenish docstring
Vocabulary for "admission"	naming, decided — admission keeps docket intake; admissible edit; response class	wiki/Glossary.md
Read checkers/	not a decision — maintainer reading is not a queued item	removed; recorded once in the dated entry
The Stage V review surface	adopted — all three rulings, which is how PRIORITIES.md already marks them	dated entry
A second theorem-facing interface in structured state	adopted — the emitter reads a list	checkers/workspace_state.py; friction entry retired
The traderized force interface as a living note	adopted — it is one	dated entry; §9's living-note form
Two-channel architecture, Coverage–Liability, where force is published	adopted — architecture yes; names to the audit; one paper with force as a module	dated entry
Whether P1 names an obligation	adopted — an obligation; naming a mechanism rejected	dated entry
Fourteen provisional names, traderized enforcement	naming — to the audit	removed
world-inclusive region and coverage(Due)	adopted — not related; a later identification must exhibit the map	dated entry
Whether the traderized inequalities are worth registering	registration — not a decision	CLAIMS.md
The deck's path-gate entry	adopted — it stands; reverting rejected	dated entry
The deck's review status	adopted — the field takes two values; the qualification moves to the notes	PROVENANCE.md
F4, the answerability layer's code	kept	queue
Pinning the Cartesian frames formalization	done — the pin is c0d885bf, on the upstream default branch, carrying CartesianFrames/; the mirror deletion is filed	item 52
Q3 graduation, and the successor to item 28	kept	queue
The source line's frontier in this line's ledger	stale — the ledger was compressed to five lines on 2026-08-15 and has no Movement I	removed
Whether endpoint-preservation is a target	kept	queue
The identity a wiki pull request opens under	already ruled in conversation, 2026-08-16	dated entry
Counterfactual-legitimacy vocabulary	naming — to the audit	removed
Whether that round's open questions become items	filed	item 59
The two formalization obligations	filed — the erasure discharged and registered; DistanceComplete open	items 48, 49
Assessment-process vocabulary	naming — to the audit	removed
Whether the per-commit Model: trailer is enforced	adopted — enforced where the body names a model; dropping the requirement rejected	tests/attribution.py
Projection round names	naming — to the audit	removed
Merge upstream Formalized-Agent-Foundations #2	done — merged at c0d885bf, which is the pin	removed
Whether the projection results are worth registering	registration	CLAIMS.md
Whether the deductive region is registered, and against which item	registration	CLAIMS.md, item 51
Names for the deductive region's constructions	naming — to the audit	removed
Whether the max–min development is promoted	registration; names to the audit; the adapter exists	CLAIMS.md, item 50
The reason-state/record naming split	naming, decided — 𝓡_n and N_{≤n}; the wiki edit is the next round to touch the page	dated entry
Transition-certificate vocabulary and the freeze	adopted — names to the audit; the freeze enacted with its reopening condition	dated entry
Whether the reason-state interface becomes a living note	adopted — it is one, at its round path	dated entry

3. The registered declarations

Twenty-four entries, all kind: lean, class lean-proved, docs.verification pointing at projects/normativity/notes/GENERALIZED_LI_PAPER_HANDOFF.md. Every declaration is named in full in a #print axioms line in the library, so each is one the axiom audit re-elaborates.

declaration (under Workspace.Normativity.Contrib.)	answers_item
AssessmentProcess.BudgeterAt_value_eq_of_safe	47
AssessmentProcess.budgetedTrader_netWorth_floor	47
AssessmentProcess.exists_budgetedTrader_exploits	47
AssessmentFirm.trading_firm_dominance	47
AssessmentFirm.no_efficient_trader_exploits	47
EnforcementStrategy.marketValueRat_enforcementStrategy	41
EnforcementStrategy.rowViolation_le_of_intensity_ge	41
EnforcementPreservation.no_efficient_trader_exploits	41
DeductiveEnforcement.enforcement_day_value_nonneg	41
DeductiveEnforcement.enforcement_netWorth_nonneg	41
DeductiveEnforcement.no_efficient_trader_exploits_of_worldInclusive	41
DeductiveEnforcement.isLogicalInductor_of_computableMarket	41
DeductiveEnforcement.witness_market_not_exploited	41
CoherenceModulus.gap_le_of_mixture	42
CoherenceModulus.gap_le_of_net_cover	42
EnforcedCompiler.ProjectionSchedule.end_to_end_effective	48
EffectiveRepresentation.end_to_end_of_constraints_effective	48
DeductiveEffective.deductive_end_to_end	48
MaxMinRepresentation.exists_maxMin_representation	50
MaxMinRepresentation.isPiecewiseAffineOn_maxMin	50
DeductiveRegion.admissiblePatterns_sound	51
DeductiveRegion.admissiblePatterns_complete	51
DeductiveRegion.admissiblePatterns_ne_nil_iff	51
DeductiveRegion.deductiveRegion_eq_convexHull	51

Items 47, 48, 50 and 51 are filed by this round for the demand these answer; item 49 is filed open, for DistanceComplete. The two coherence-modulus entries carry answers_item 42 with a note saying which half of that item's narrowing they establish and that the item stays open — the closest honest fit, and the weakest link in this table.

The handoff note now states Theorem 5 unqualified, names the three end-to-end declarations, and carries one debt rather than two. Its Theorem 1 no longer says the market-computability premise is carried.

4. The depends_on backfill

Sixty records, every one carrying the field. Fifteen carry a non-empty list; the deepest transitive rest is the certified-interactive-service round, on ten ci-only rounds.

round	depends_on
2026-08-11-phi-regret-applicability	phi-regret-prep
2026-08-11-phi-regret-bridge	phi-regret-prep, phi-regret-applicability
2026-08-11-phi-regret-learner	phi-regret-prep, phi-regret-bridge
2026-08-13-procedural-legitimacy	legitimacy-reorganization
2026-08-13-relational-scorekeeping-refinement	relational-scorekeeping-bridge
2026-08-13-local-regret-normative-learning	relational-scorekeeping-bridge
2026-08-13-crown-jewel-learning-theorem-refinement	crown-jewel-learning-theorem
2026-08-13-crown-jewel-learning-theorem-final	crown-jewel-learning-theorem, -refinement
2026-08-18-projection-enforcement	traderized-enforcement
2026-08-19-deductive-region	traderized-enforcement
2026-08-21-internal-answerability	procedural-legitimacy, relational-scorekeeping-bridge, crown-jewel-learning-theorem, traderized-enforcement, counterfactual-legitimacy, projection-enforcement
2026-08-22-role-parametric-answerability	internal-answerability
2026-08-23-afoundational-inquiry	role-parametric-answerability
2026-08-23-transition-certificates	internal-answerability, reason-representation
2026-08-23-certified-interactive-service	afoundational-inquiry

Empty for silence, not for independence. These reports say nothing about what they consume, so the field records nothing rather than this round's guess: 2026-08-11-phi-regret-prep, 2026-08-11-stage-iii-fud, 2026-08-11-stage-v-li-native, 2026-08-12-cartesian-frames, 2026-08-12-corpus-reconciliation, 2026-08-12-legitimacy-reorganization, 2026-08-13-relational-scorekeeping-bridge, 2026-08-13-crown-jewel-learning-theorem, 2026-08-16-traderized-enforcement, 2026-08-17-counterfactual-legitimacy, 2026-08-23-reason-representation. The crown-jewel and counterfactual-legitimacy cases are the ones most likely to be wrong: both plainly build on earlier rounds, and both describe what they build on in their dispatches rather than in their reports.

Empty for independence, on the report's own words: 2026-08-18-maxmin-representation (its source is Ovchinnikov's paper and Mathlib), 2026-08-11-stage-iv-future-agent ("the previous round is not weakened … a different model rather than a correction"), and 2026-08-12-reachable-corrective-control ("#26's findings are cited here and are not reproduced here"). The remaining records are workspace and scaffolding rounds with no research hypotheses.

The check fails on an unresolvable id, a self-reference, a cycle, and a missing field; rests_on is derived after the cycle check, so the walk terminates. Six new self-test cases, four of them null inputs.

5. Friction, and the branch

entry	disposition
documented-command check; root-document layer check	merged into one entry, deferred as the maintainer ruled; both audited clean by hand on 2026-08-17
the deference line has no claims registry	kept, with a line saying the headline rule reaches new work and not this backlog
a layer's theory is authoritative and its code is disposable	kept; the decision is in the queue under R1
a pointer into a superseded tree still resolves	kept; the check it needs has a null-input case and nobody has built it
upstream work on a feature branch	retired — ruled closed on 2026-08-17; mirror-plus-cross-check is the pattern
a generated view lives inside a round's directory	fixed — state/views/, with the three pointers into the old location repaired
a merge can drop a ledger entry	fixed — tests/round_records.py plus the append-beneath-same-dated convention
the structured state holds one theorem-facing interface	fixed — the emitter globs state/theorem_interface*.json, and an empty match fails
agent worktrees are not ignored	kept — the .gitignore half has no null-input case and the gitlink check is a new gate, so this stays filed rather than half-taken

round/2026-08-17-lean-gate-scope is landed, not dropped. Both scripts pass their self-tests unmodified on current main; they are taken verbatim, wired into ci.yml and tests/run.py, and GATE COVERAGE now reports ten gate scripts with five self-test-only. The branch's own PRIORITIES.md renumbering is not taken: two friction entries were filed after it was cut, so the list is renumbered here against the current one. Its draft pull request should be closed as landed.

**Dead branch remnants on origin, listed and not deleted.** Deleting a remote branch is not reversible from here and several of these are checked out in other sessions' worktrees on this machine, so this is a list for the maintainer rather than an action taken.

Fast-forwardable into main, so certainly redundant (13): claude/constraint-schedule, claude/deductive-region, claude/deductive-schedule, claude/fourier-motzkin, claude/fourier-motzkin-uniform, claude/maxmin-representation, claude/polyhedral-coverage, claude/projection-bridge, claude/projector-generator, projection-enforcement, round/2026-08-21-internal-answerability, round/2026-08-22-role-parametric-answerability, round/2026-08-23-afoundational-inquiry.

Ahead of main but whose round is indexed in state/rounds.json, so squash-merge remnants (24): admin/cleanup, agent/legitimacy-research-findings, agent/normative-learning-interface, agent/phi-regret-applicability, agent/phi-regret-bridge, agent/phi-regret-learner, agent/wiki-normativity, claude/leverage-legitimacy-reorganization-u4l0fi, claude/reachable-corrective-control-f4hiw2, integration/2026-08-11-current-state, patch/attribution-provenance-names, patch/priorities-and-slop, research/phi-regret-prep-20260811, retire/frozen, round/2026-08-11-deference-corrigibility, round/2026-08-11-stage-iv, round/2026-08-11-stage-v, round/2026-08-12-cartesian-frames-bridge, round/2026-08-12-corpus-reconciliation, round/2026-08-12-time-indexed-corrective-capability, round/2026-08-13-crown-jewel-learning-theorem, round/2026-08-13-local-regret-normative-learning, round/2026-08-13-relational-scorekeeping-bridge, round/2026-08-16-wiki-in-repo-sync, round/2026-08-16-wiki-state-bindings, round/2026-08-17-counterfactual-legitimacy, round/stage-iv-and-front-door, traderized-enforcement.

Not remnants, and not to be deleted: round/2026-08-17-lean-gate-scope (closable once this lands), round/2026-08-18-principal-mediated-corrigibility, round/2026-08-24-enforcement-affordability, feat/traderized-constraints-paper, claude/for-ais-refinement, and A-M-Berns-patch-1 through -3 — each carries work no round record indexes.

6. Deviations

1. The queue held thirty-seven entries, not eighteen. The dispatch's count is wrong. Every entry was triaged; §2 is the full table.

1. Three entries are kept where the dispatch expects one to three, having rechecked. F4 turns on whether the program will keep building on the answerability layer; Q3 turns on whether the missing idea has arrived; and endpoint-preservation says of itself that it is what is worth proving. The fourth candidate — the reason-state naming split — was adopted instead, on the ground that the round that raised it proposed a specific assignment, so R4's "cannot choose between two candidates" does not apply.

1. The Lean build did not run locally; it ran in CI. The resource guard reported LOADED (swap at a 92% high-water mark) and safe-lake.sh refused after its full 900-second wait. Running lake directly is what the machine-load rule forbids, and the attempt was refused by the permission classifier, correctly. CI ran it instead: the lean job on pull request #52 built and audited green in 4m38s, and the scope decision this round landed is what sent it to build — .github/workflows/ci.yml reaches the gate. Three further checks stand behind it: this branch changes no file under lean/; the registry checker confirms every registered declaration resolves in the library source; and a separate pass confirmed all twenty-four appear in full in a #print axioms line, so each is one the audit re-elaborates. A built lean/.lake is seeded in the worktree (gitignored) for a local run.

1. The Aug-12 standing item about new harness property forms does not exist. R7 asks for it to be retired as a goal; nothing in PRIORITIES.md, DECISIONS.md, AGENTS.md or checkers/README.md states it. R7's substance is landed in the registry section, including the clause permitting a new property form where a round needs one.

1. No sentence in the claims-registry section implied that harness growth is the path for finite results, so nothing was cut there. The nearest thing — the *two ways out of contributor-checked* paragraph in the Python regime — is about a contributor's own checker being read, which is a different mechanism, and it stands.

1. The legitimacy window holds six rounds, not five (2026-08-23 carries four). All six were read; the seven named blockers plus the counterfactual-legitimacy round's load-bearing question are filed as items 53–59, minus the R → O compiler, which deduplicates against item 39 and is recorded there as a narrowing instead.

1. **No state/rounds.json verdict said "closed provisionally"**, so none needed leaving alone. The phrase lives in the transition-certificates round's own README.md and MEMO.md, which are history. The wiki's Legitimacy status block did not repeat it either; what did was one sentence on Normative-Record-and-Inquiry.md, which now says living note, and the Legitimacy block gains a living-note paragraph with the freeze's reopening condition.

1. The exhaustion-behaviour adoption changed a default and one test. compile_safe_force and compile_funded_force defaulted to refuse; the adopted behaviour is quarantine, so the default moved and test_an_unaffordable_request_refuses_by_default became two tests — the new default, and refusal on request. The dispatch names src/outflow.py, which exposes the policies as functions with no default; the default lives in src/force_api.py, and changing it there rather than nowhere is the reading that makes the instruction do something.

1. The corrigibility-ledger entry was stale rather than decidable. The dispatch's has a recommendation class does not fit it: the document it names lost the section the entry is about when the 2026-08-15 consolidation compressed it from 471 lines to five.

1. **.gitignore was not changed.** The worktree friction entry's cheap fix is a one-line ignore rule with no null-input case, which is not contained as R10 defines it, so the entry stays filed rather than half-taken.

1. The trailer check shipped matching nothing, and was fixed before the pull request was reviewed. Its body-declaration pattern was anchored to the start of a line; the pull-request template's dispatched-round option puts Model: on a continuation line after and, so the check would have skipped the very pull request that introduced it and reported green. Found by running the gate against the actual body rather than against its own fixtures — which is the failure mode AGENTS.md's null-input section says this repository has already shipped twice. The pattern now finds the label anywhere on a line and excludes a backticked mention, so prose about the gate is not read as a declaration, and two self-test cases pin both directions.

7. What this does not establish

Recording a dependency pays no debt. rests_on says the certified-interactive-service round rests on ten ci-only rounds. It has said nothing about whether any of those ten is right. The view makes an existing quantity visible and creates no new evidence; a round with a large count is not thereby suspect, and one with a count of zero is not thereby sound — its hypotheses may simply come from the frozen consolidation, which the field does not track.

The backfill is a reading of reports, and eleven of them are silent. For those the field is [], which is weaker than "independent" and is recorded as such in §4. Two of the eleven — the crown-jewel theorem and the counterfactual-legitimacy round — almost certainly consume earlier work; their reports do not say so, and this round did not infer it, because a dependency graph built from inference would be a graph of this round's guesses wearing the authority of a checked field.

Every adoption in §2 is reversible, and none rests on this round's judgment of the mathematics. Each was taken on the recommending round's own reasoning: where that round recommended, this one adopted; where it was indifferent between options and its own implementation had already chosen, this one adopted the implemented choice and said so. Under no negative ontologies a re-ruling leaves only the new entry standing, which is why adoption was cheap enough to be the default. It also means the ledger now asserts, in the maintainer's voice, fifteen positions no maintainer has read.

The registry now asserts exactly the traderization headlines and the scaffolding smoke tests, and nothing else. Twenty-four theorems from four rounds, plus two smoke results and one worked enumeration example. It does not assert the coherence bridge's exactness half, which is derived plus exhaustive-finite and is item 49; it does not assert anything from the deference line, whose kernel-verified results remain unregistered; it does not assert any Python result from any round; and it does not assert the safety theorem's necessity direction, which is item 40 and open. What a headline entry claims is that the kernel checked that statement, not that the statement is the right one.

The bar is not self-enforcing. Nothing gates an entry that lacks a turns-on line, and nothing detects a round that reserves what it could have adopted; both are review matters, as the gates table says. The queue is short today because this round emptied it, not because the rules prevented it from growing.

The rules were applied once, to the present state. They have not been tested against a round that disagrees with them, and the first genuine test is a round that would rather reserve something than adopt it.

The Lean verdict is CI's, not this executor's. The build and the axiom audit ran on the pull request and are green; no declaration was re-elaborated on this machine, and §6.3 says why. What that verdict establishes is that the twenty-four registered names resolve and audit to the three allowed axioms — not that any of the twenty-four statements is the one the paper should make, which is a reading no gate performs.

8. Closeout

Merged as bd16ecf, squashed, with the Model attribution section and a Model: trailer in the squash message. The maintainer's closeout dispatch confirms the fifteen adoptions and the twenty-four registrations stand, and rules that headline in the registry means what this round read it to mean: every kernel-checked theorem a round's report presents as a result. A shorter list, if one is ever wanted, is a flag on entries rather than a narrower registry.

round/2026-08-17-lean-gate-scope's draft pull request, #37, is closed with a comment recording that its two commits landed verbatim here.

**Forty-two branches deleted on origin**: the thirteen fast-forwardable into main, the twenty-eight squash remnants, and round/2026-08-17-lean-gate-scope last, after its pull request was closed.

Two count errors in §5, found while acting on it. The squash-remnant paragraph names twenty-eight branches and says twenty-four; the not-remnants sentence names five branches plus a three-branch range and says six. The lists were right and the arithmetic was not, and the closeout dispatch repeated both numbers back. Deletion followed the lists.

Nine branches remain, none of them a remnant: A-M-Berns-patch-1 through -3, claude/for-ais-refinement, feat/traderized-constraints-paper (#44), round/2026-08-18-principal-mediated-corrigibility (#40), round/2026-08-24-enforcement-affordability (#50), and this round's own branch, which the squash made a remnant and which the dispatch did not authorize deleting.

No worktree was removed. The dispatch asks for git status --porcelain in each worktree holding a remnant branch, and this session is worktree-isolated: the harness refuses any git operation redirected at another worktree, so the check cannot be run and the removal cannot be performed from here. Ten worktrees hold branches that were just deleted on origin — .claude/worktrees/agent-a147ee8f2141ba783, -a5d0eb479c63a58b2, -a70b42885580eaaac, -a882fed6663f281f1, -ac67f74b7d7940c82, -ad40cda47720fca48, -aea0b0bc98031f4ed, .claude/worktrees/pr38-proof-closing, ~/Desktop/alignment-workspace-internal-answerability, and ~/Projects/alignment-workspace-afoundational — and their local branches are untouched, so nothing in them is lost. The main checkout at ~/Projects/alignment-workspace is on round/2026-08-17-counterfactual-legitimacy and is a working tree rather than a removable worktree. Three further worktrees hold claude/effective-representation, claude/polyhedral-projection and claude/stage-aware-enforcer, which have no remote counterpart and were not in scope. Removing any of them is a maintainer action from a session that is not worktree-isolated, and each is worth a git status first: a clean worktree at the moment of checking may still belong to a session mid-task.

The round record's verdict is unchanged; it already states what the round did.

A second gate shipped matching the wrong thing, and this closeout is what found it. tests/round_records.py treated no added files as a broken diff. That premise is false: a pull request that modifies files and adds none is an ordinary change, and the closeout — one modified file, nothing added — is the first such pull request the gate saw. It failed, and would have failed every modify-only pull request against main from the moment #52 landed.

The gate came verbatim from round/2026-08-17-lean-gate-scope, and §5 above records that both scripts passed their self-tests unmodified. That was true and insufficient: the self-test exercised landed_rounds and unrecorded and never the branch that fired, because main() mixed the decision into the git plumbing where nothing could reach it. The decision is now verdict(), a pure function of the changed list, the added list and the provenance text; the null input is a diff listing no files at all; and five cases pin it, the first being the modify-only pull request the gate got wrong. Repaired in this closeout rather than filed, under §14: one document, non-retroactive, with its null-input case.

Two gates in two days, both shipping green while checking the wrong thing, both caught by running them against a real pull request rather than against their own fixtures. The pattern is worth naming: a self-test written beside a gate tests what its author already believed.