2026-09-03-defeat-landing-horty-standing

Research round: Defeat Principle Landing, Horty Check, and Standing Repair

Prompt-author model: Claude Fable 5.1 (Anthropic), via chat. Executor: unrecorded in the dispatch; the executor was Claude Opus 5 (Anthropic), recorded in the round's PROVENANCE.md.

Work against the live alignment-workspace at current main with PR79 landed (2026-09-02-unified-grounds-answerable-defeat). Inspect the actual head. This round closes the two of PR79's outstanding maintainer actions the author has ruled on, performs the prior-art check that PRIORITIES.md item 77 names as part of its deliverable, and repairs one weakness in PR79's Lean that its report did not flag. It does not touch items 58, 61, 75, 76, and it does not rule on the load-discount, settlement-independence, or protected-participant reservations, which stay in the queue.

Preserve: the settled IssueTrace layer (byte-identical), every PR79 theorem that survives the repair in §3, the carriers/anchored-slices/faithful stack, and the frozen affordability files.

1. First commit: the author's ruling

The author has ruled: the Defeat Principle is adopted. No participant extinguishes a debt; a participant may pay it or move it onto the grounds for saying it is not owed; only settlement extinguishes. Land this as a dated DECISIONS.md entry as the round's first commit, per the standing practice that chat rulings land as the next round's first commit (the Aug 24 entry on the reservation bar and epistemic debt). Cite the ruling by date and content. Then strike the corresponding "agent-decided, reversible" status from PR79's entry, remove the Defeat Principle from Awaiting the author, and drop the "conditional on the Defeat Principle" qualifier from every PR79 theorem statement it now governs — in THEOREMS.md, DEFEAT.md, and the Lean docstrings — leaving a one-line note that the round ran under it as hypothesis before the ruling. Do not strike the other three reservations.

2. The Horty check

Item 77 says a prior-art check is part of its deliverable, names Horty's priority orderings among defaults as the obvious place to look, and predicts they are not enough: a priority ordering says which reason wins, not what licenses the loser to stop being owed. PRIOR_ART.md §2 (Horty 2012, Pollock 1987) and its dependency note record the same open question. Settle it.

Work from the actual texts — Reasons as Defaults (2012), and Pollock 1987 for the rebut/undercut distinction the round's answer/dispose kinds are built on. Do the following, in order, and report each as a finding with a verdict:

1. Expressibility. Can a Horty priority ordering express dispose? Take the round's three kinds and ask what each corresponds to in Horty's apparatus: is a defeated default disposed, answered, or neither? State precisely what Horty's theory says happens to a default that loses — whether it retains any standing, whether it can be reactivated, whether anything is owed on its account — and compare to D2's successor-bearing transfer.
2. The direction of the gap. If Horty cannot express disposal, say which of D1–D3 has no image. The prediction to test: priority orderings have grounds (D1) but no successor (D2) and no separation (D3), because the ordering is exogenous and unauthored. If the prediction is wrong, say how.
3. Undercutting. Horty's treatment of exclusionary reasons and Pollock's undercutters are the closest things to dispose. Determine whether either is answerable in the round's sense — whether the exclusion is itself a claim that can be attacked in the same system — or whether it sits at a level the system cannot challenge. This is the crux: if an exclusionary reason is unchallengeable, it is a settlement fact in the round's typing, not a disposal, and the theory has one summand where the round has two.
4. What survives as new. State in one paragraph what the round's defeat theory adds that Horty and Pollock do not have, phrased so a reader of those books could check it, and what it inherits from them that PRIOR_ART.md must now cite as a dependency rather than a resemblance.
5. Argumentation. Do the same for ASPIC+ (Prakken 2010 / Modgil–Prakken 2013) in one section, not a full treatment: whether argument defeat there has a successor, and whether the attack relation is authored. Prakken 2018 is already cited for the statics; do not re-derive that.

Deliverable: HORTY.md in the round directory, with the five findings, and a dated append to PRIOR_ART.md §2 and to its dependency note replacing "open question" with the verdict. If the verdict is that Horty can express disposal, that is a finding that changes what the round claimed as new; report it prominently and do not soften it.

3. Repair Answerable.contested

PR79's Licence has lic : Q → K → Ty → X → Prop and standsFor has no participant argument. So Answerable.contested reads ∃ b, b ≠ resolver ∧ (someone stands for q') and b is unused: any participant type with two elements satisfies the first conjunct, the standing side of D3 is vacuous, and PR79's laundering result rests entirely on foreign_ground. DEFEAT.md's D3 says "some b ≠ resolver has standing on the successor," which the Lean does not say.

Repair by putting the participant into the licence: lic : Q → A → K → Ty → X → Prop, standsFor Li n b κ τ x := ∃ q ∈ O n, Li.lic q b κ τ x, and contested : ∃ b, b ≠ resolver n q ∧ standsFor Li n b (κ q') (τ q') (x q'). Carry the participant through AnchorStanding and anchor_grounded (the licence-issue licensing a fresh issue's protocol now licenses it for someone). Re-elaborate every PR79 declaration; report which ones needed more than the type change.

Then prove the laundering theorem on both sides: a disposal walk whose resolvers, ground-openers, and standing-holders all lie in one hand is refused, with a fixture showing the standing side is now doing work — a disposal with a foreign ground but standing held only by the resolver, refused by contested alone.

State, as a definition only, the principal-relative form: AnswerableFor P requires standsFor Li n P … on the successor. Prove the P-relative laundering theorem (no coalition excluding P can walk a disposal to completion). Do not present this as the general non-capture predicate; the protected-participant question is the author's and stays in the queue.

4. Nonvacuity

PR79 has no Lean witness for DefeatTrace or Disciplined; every fixture is Python, and the report's own "nothing shows a defeat-disciplined trace exists" is the same gap. Supply one in Lean, in the style of the spine's fixA/fixB fixtures: a finite trace with one answered issue, one settled issue, and one answerable disposal with its successor, satisfying Disciplined after the §3 repair, with #print axioms on the witness. Add a second witness that fails Disciplined by exactly one clause (a self-grounded disposal), proved to fail. If constructing the witness reveals that Disciplined is unsatisfiable as stated, that is the finding; stop and report it.

5. Hostile fixtures (Python, exact rationals)

Add to PR79's runner: standing held only by the resolver (refused by the repaired contested); standing held by a second participant who is the opener of every ground (accepted — the coalition case, unchanged, restated under the new type); the P-relative walk where P holds standing at every successor (P-laundering theorem's positive case); the same walk with P absent from one successor (refused). Keep PR79's 24 tests passing.

6. Out of scope and reservations

Out: the coalition repair beyond the P-relative definition, load discount, settlement independence, market realization of the contest charge, and composition with the scorekeeping move grammar.

Reserve to the author only if the Horty check produces one: whether the round's kind settle and Horty's exclusionary reasons are the same object (turns on whether the program wants exclusion to be challengeable, which is the settlement-independence reservation seen from prior art). Otherwise reserve nothing new. Append per the reservation bar in AGENTS.md's reserved- items standard, with a one-line turns on.

7. Deliverables

Round directory under projects/normativity/legitimacy/rounds/: REPORT.md first, then HORTY.md, STANDING_REPAIR.md, WITNESS.md, PROVENANCE.md, src/, tests/. Lean edits in the spine file. Update item 77's status to whatever the Horty verdict supports — it closes only if the check is done and the licence predicate stands; say which. Provisional names listed in the report per the provisional-naming standard. Fill depends_on in state/rounds.json. Report every deviation. Do not edit wiki/; propose wiki changes in the report for the maintainer.

Report — Defeat Principle Landing, Horty Check, and Standing Repair

Closes two of PR79's outstanding maintainer actions, performs the prior-art check PRIORITIES.md item 77 names as part of its deliverable, and repairs a defect in PR79's Lean that its report did not flag.

Verdict

DEFEAT-PRINCIPLE-LANDED-HORTY-CANNOT-EXPRESS-DISPOSAL-AND-THE-STANDING-CLAUSE-WAS-VACUOUS — the Defeat Principle is adopted by maintainer ruling and its consequences are no longer conditional; Horty's machinery cannot express authorized disposition, and the reason is deeper than item 77 states, since his theory says what to conclude rather than what is owed and therefore has no account for a licence to operate on, while his exclusion mechanism turns out to be challengeable in-system and so is closer to disposal than to settlement, leaving the round's two summands intact rather than collapsed, a verdict Horty states himself when he writes that exclusionary reasons can themselves be excluded and rejects a stratified hierarchy of orders; ASPIC+ has neither a successor nor an authored attack relation, and its reinstatement is computed by the semantics rather than licensed by a participant, which is the opposite of a transfer; PR79's separation condition bound a participant its body never mentioned, so the standing half of D3 was vacuous and every laundering result in that round in fact rested on the foreign-ground clause alone, a defect the Python model did not share and therefore did not catch; with the participant carried into the licence the standing side alone refuses a single-handed disposal, which closes the case of a disposal citing only settlement facts, since such a disposal satisfies the foreign-ground clause vacuously; and the specification PR79 wrote down now has a Lean model, together with a second trace proved to fail it at exactly one clause, which turns the round's first finding from a remark into a checked pair.

1. The ruling, landed

The Defeat Principle is adopted (DECISIONS.md, 2026-09-03, maintainer ruling), landed as this round's first commit. The reservation is struck from Awaiting the author; PR79's entry no longer reads "conditional on the Defeat Principle"; and the qualifier is gone from THEOREMS.md, DEFEAT.md and the two Lean docstrings that carried it, each leaving a one-line note that the round predates the ruling. The other three reservations are untouched.

2. The Horty check — five findings

Full text in HORTY.md. Headlines:

1. Expressibility — no. And the item's own reason concedes too much. Horty computes a proper scenario: a defeated default is simply not selected, with no residue and nothing attached to it. His theory says what to conclude, not what is owed, so there is no account for MayDispose to operate on and the question does not arise inside it.
2. **Direction of the gap — the prediction is right about which clauses have images and wrong about why. Grounds yes, successor no, separation no. But separation is missing not because the ordering is exogenous: Horty specifically built variable priority default logic, where priorities are established by higher-order defaults. What is missing is authorship, not endogeneity** — a default theory has no participants. So the gap is not repairable by making priorities more dynamic.
3. Undercutting — the crux resolves the other way. Horty implements undercutting as a triggered default lowering the undercut rule's weight below a threshold. The undercutter is itself a default and so is itself defeasible: exclusion is challengeable in-system. An exclusionary reason is therefore a dispose without a successor, not a settle. The theory does not have one summand where the round has two, and the round's separation of the two survives.
4. What is new, checkable by a reader of the books: proper scenarios and ASPIC+ extensions are a function of the current theory and of nothing in the history of defeats. Delete the record of which defaults lost, recompute, same answer. The round's successor-bearing transfer makes the future depend on that history. What becomes a dependency rather than a resemblance: answer/dispose is Pollock's rebut/undercut, transposed from a belief's warrant to a debt's.
5. ASPIC+ — no successor; reinstatement exists but is computed by the semantics rather than licensed, which is the opposite of a transfer; preference ordering exogenous in the canonical framework, so the attack relation is unauthored. Here the dispatch's prediction is exactly right.

3. The standing repair

STANDING_REPAIR.md. PR79's contested bound b and never used it, so it reduced to (∃ b, b ≠ resolver) ∧ (someone stands) — vacuous for any participant type with two elements. Repaired by putting the participant into the licence.

Two things worth stating plainly:

• No PR79 theorem was false. Everything it proved is true; the definition was weaker than its own prose, and the laundering claim rested on one clause while appearing to rest on two.
• The repair closes a case, not just a binder. foreign_ground is satisfied vacuously by a settlement ground, since no participant opened it. So a disposal citing only settlement facts previously satisfied all of D3 uncontested. After the repair contested is what refuses it. foreign_ground_dichotomy states exactly what the grounds side gives, rather than overstating it.

Nothing needed more than the type change — which is itself the confirmation that no prior result was consuming contested.

4. Nonvacuity

WITNESS.md. Witness.witness_disciplined is the first Lean inhabitant of Disciplined; Witness.witnessBad fails Answerable at not_self and is proved to satisfy grounded, born and inherits, turning PR79's first finding into a checked pair.

5. Deviations (standard 8)

1. PR79 had not landed. The dispatch says to work "at current main with PR79 landed"; main was 51898f2 and PR79 was open. This round is stacked on PR79's head rather than on main, since merging is the maintainer's and the ledger says a merge is never a queue entry. If #79 merges first this rebases cleanly.
2. The Horty check began without the primary text and was completed with it. The first pass could not reach Reasons as Defaults — author-site certificate mismatch, blocked archive, paywall — and said so, marking three findings unverified. The maintainer then supplied Horty's 2006 paper, which carries the whole apparatus, and the findings were rechecked against it: two sharpened, none withdrawn. HORTY.md §0 records both states rather than presenting the result as if the text had been in hand throughout. The 2012 book is still unread, so a claim about what the book says is not licensed by this round. Pollock 1987 was not read either.
3. **PRIOR_ART.md's Pollock URL is dead**, though marked "citation verified 2026-09-01". Recorded rather than quietly repaired; the verification stands as a fact about its date, the link does not.
4. No new reservation was appended. The dispatch permits one if the Horty check produces it. Finding 3 answers the settle-vs-exclusion question rather than raising it, so there is nothing to reserve.
5. A fixture bug of my own, found while writing §5 and recorded in STANDING_REPAIR.md §5: standing was first read at the live prefix instead of the disposal's own batch. Same class of error as the defect being repaired.

6. Provisional names (standard 6)

InOneHand, LaunderingWalk, AnswerableFor, not_in_one_hand_of_contested, foreign_ground_dichotomy, no_laundering_walk, no_coalition_excluding_principal, Witness.* (bornAt, resAt, Resolves, witness, witnessBad, wlic), StandingModel, standing_holders, edge_holders, principal_holds_throughout, coalition_walks_excluding, single_handed_edges.

7. What this does not establish (standard 9)

• The 2012 book was not read, only the 2006 paper it develops. Every finding is about an apparatus that paper carries in full, so the theory question is answered; a claim about what the book says is not licensed here.
• The coalition hole is not closed. AnswerableFor is a definition plus a one-line theorem, deliberately not offered as the general non-capture predicate. The two-participant alternating walk still launders under plain separation.
• The P-relative form names a party, which is exactly what the open reservation is about. Nothing here argues that a legitimacy predicate may do so.
• The witness is small. It exercises the three kinds and not the prerequisite/route machinery; it shows Disciplined is satisfiable, not that any interesting practice satisfies it.
• T1, T3, T4, T5 of PR79 remain paper-derived, unchanged by this round.
• **Auth and grounds-nonemptiness still do not re-derive** from ancestry.
• Findings 1–4 are readings of Horty's 2006 paper and Finding 5 of the ASPIC+ tutorial — both primary. No finding now rests on a secondary source alone.
• **PRIOR_ART.md's Pollock attribution is off: Horty credits the undercutting distinction to Pollock 1970**, not the 1987 paper the ledger cites.

8. Outstanding maintainer actions (standard 10)

1. ~~Merge or rebase PR79~~ Done — PR79 merged to main as 198a86a on 2026-09-03 and this round was rebased onto it.
2. Decide whether item 77's prior-art deliverable is discharged. The theory question is now answered against Horty's own text; only the 2012 book is unread, and its contribution over the paper is a development of §3.2 plus the Dancy material. Either rule the paper sufficient, or obtain the book.
3. ~~**Repair PRIOR_ART.md's Pollock entry~~ Done, 2026-09-05** — the recorded URL redirects to a new host that serves the paper; the entry now carries that address and the DOI, and keeps the Pollock 1970 caution.
4. Three reservations remain in the queue, untouched: load discount, settlement independence, protected participant.
5. Wiki changes proposed, not made (the dispatch forbids editing wiki/): wiki/Normativity.md or a new page has no account of defeat at all, and now could carry one — obligation, the three kinds, and why disposal moves rather than extinguishes. Recommend a short section rather than a page.
6. Register Lean headlines if wanted; nothing is registered.

Defeat Principle Landing, Horty Check, and Standing Repair

Round of 2026-09-03. Closes two of the previous round's outstanding maintainer actions, performs the prior-art check PRIORITIES.md item 77 asks for, and repairs a defect in that round's Lean that its report did not flag.

The Defeat Principle is settled as of this round: DECISIONS.md, 2026-09-03, maintainer ruling. Nothing here is a registered claim.

Read in this order

file	what is in it
[REPORT.md](REPORT.md)	verdict, five declared deviations, what is not established, outstanding maintainer actions
[HORTY.md](HORTY.md)	the prior-art check: five findings, and an explicit account of which texts were and were not read
[STANDING_REPAIR.md](STANDING_REPAIR.md)	the vacuous contested clause, the repair, and laundering reproved from the standing side
[WITNESS.md](WITNESS.md)	the first Lean inhabitant of Disciplined, and one that fails by exactly one clause

Three results in one line each

• **Horty cannot express MayDispose** — not because a priority ordering fails to license the loser, but because his theory says what to conclude, not what is owed, so there is no account for a licence to operate on.
• Exclusion is challengeable in-system, so an exclusionary reason is a dispose without a successor and not a settle. The round's two summands survive the check.
• The standing half of D3 was vacuous, and every laundering result in the previous round in fact rested on one clause while appearing to rest on two.

What the check rests on

Horty's own text, supplied mid-round: Reasons as Defaults, Draft #2, 2006 — the paper the 2012 book develops, carrying the full apparatus. All five findings are checked against it; none was withdrawn when it arrived and two got sharper. The 2012 book is still unread, so a claim about what the book says is not licensed here. HORTY.md §0 records both states of the check rather than tidying the first away.

Verify

python3 tests/run.py # 7 tests; the previous round's 24 also still pass cd ../../../../../lean && lake build Workspace.Normativity.Contrib.NormativeContinuity

The Lean lives in lean/Workspace/Normativity/Contrib/NormativeContinuity.lean §§5.2, 5.4, 5.7–5.9.