2026-10-21-rebuttal-and-end-to-end

Prompt — rebuttal by settlement, the seed landing, and the first end-to-end run (2026-10-21)

You are working in the alignment-workspace repository, on main after the merge of PR #129 (the warrant-enforcement-semantics round). If lean/Workspace/Normativity/Contrib/WarrantEntitlement.lean is not on main, stop and report. Do not stack this round on an unmerged branch. Two unmerged branches are sources for Part B; they are not bases.

Round directory: projects/normativity/rounds/2026-10-21-rebuttal-and-end-to-end/. The prompt goes verbatim in prompts/2026-10-21-rebuttal-and-end-to-end/PROMPT.md. New priority items start at 117.

What this round is for

PR #129 found that a linear strength row contraposes under settlement and that the contraposition is exploitable (item 113, the orphan pin of item 112). The maintainer has ruled on the repair (M1–M4 below). This round lands the rule, re-proves the affected statements under it, lands the seed-statics and convergence material the end-to-end construction needs, and runs the pipeline end to end once on one fixture — item 35, specified here for the first time. The witness is small on purpose. Its value is that every stage exists on main and is exercised in sequence by one run.

Be skeptical. The rule's interaction with the ported monotonicity theorems was argued in conversation, not proved. A part that fails ships its obstruction with a fixture and does not block the others, except that Part C depends on Part A.

Every declaration named below was read from main, from PR #129's branch, or from the two source branches. Confirm each exists before relying on it, and correct this prompt in the report where it is wrong.

Maintainer rulings

Record each as a dated DECISIONS.md entry as the round's first commit.

M1. Rebuttal by settlement. A strength or applicability form whose consequent coordinate is pinned false by settlement is rebutted: its row leaves the region. The warrant said "X∧A makes Y likely"; it does not say "¬Y, so not X∧A". A linear row that contraposes says more than the warrant did, and the market pays for the difference.

M2. Vacuity and retirement. A strength or applicability form whose antecedent coordinate is pinned false is vacuous and leaves. A premise form whose sentence is pinned false retires its occurrence: every row of that occurrence leaves. A refuted premise is a case that did not arise, not an inconsistency; it must not empty the joint region and withhold force on unrelated warrants.

M3. No discount on applicability. A rebuttal does not lower the applicability claim. Undercut attacks A_ρ(n); rebuttal attacks the conclusion; they stay distinct. (This closes the gap left since the August defeat exposition, where rebuttal had no mechanism in the statics.)

M4. Monotonicity is traded for reopening. Under M1–M2, settlement can widen a forced interval. That is accepted: a rebuttal is a reopening in the sense of the convergence branch (summable reopenings converge), and the global monotonicity of IsForcedInterval.mono is replaced by monotonicity on the coordinates settlement pins plus a reopening account.

M5. [MAINTAINER: land or strike.] The Aug 8 ruling (mechanically filed past-self charges burn) and the Aug 9 ruling (strength selection is locked selection, with the moral reading's objection noted) are not in DECISIONS.md. PR #102's report cites them from conversation. Land them here as dated entries, or strike this item and the round treats them as unruled.

M6. One copy. The seed declarations ported into WarrantEntitlement.lean by #129 and the branch's SeedStatics.lean become one file, SeedStatics.lean, on main; WarrantEntitlement.lean imports it. PR #102 and PR #103 are superseded by this round's Part B and are not merged; the maintainer closes them with a pointer.

Proposals from the prompt's author

Not ruled on. Adopt as agent-decided, reversible, where the mathematics supports them.

P1. The rule as a specialization step. specialize (settled values substituted into a row) already exists. State M1–M2 as a function settleForm : Settlement → Occurrence → Option (List Row) on the form, not on the specialized row: the form knows which coordinate is antecedent and which consequent; the row does not. Then prove that the rows it keeps are exactly the specialized rows that do not have the contraposing shape.

P2. Reopening account. Define, per settlement step, the reopening as the set of occurrences rebutted or retired, and state the convergence branch's hullMass_anti in the form: hull mass is nonincreasing between reopenings and the total reopened mass is what tendsto_of_summable_drops consumes.

P3. Names, provisional: rebutted, vacuous, retired for the three outcomes of settleForm; reopening for a settlement step that removes rows; end-to-end witness for Part C's object.

Part A — the rule, and what it changes

A1. settleForm per P1, on Form and the typed Occurrence of #129. Decidable.

A2. The orphan cannot form. On #129's Fixture (X, X∧A, X∧A∧Y, Y; c_P, c_A, c_S in (0,1); applicability port defeated at n₀; Y refuted at n_E): under settleForm, the strength row leaves at n_E, the region after n_E has a slack world (X true, A open), and liability_of_odds applies with the same 3ρ. State this as Fixture.liability_rebutted. Then show harmonic_buyer_run (src/fixture.py) has nothing to buy against: the enforcer holds no row in X∧A after n_E. Exact rationals; Lean for the liability, the fixture test for the buyer.

A3. The premise guard retired. Under M2, refuting X retires the occurrence and the region is the one the other warrants force. Show on a two-warrant fixture (the second warrant on disjoint sentences) that refuting the first's premise leaves the second enforced. Under #129's rule it emptied the region and withheld both — exhibit that as the countermodel.

A4. Monotonicity restated. IsForcedInterval.mono and forcedInterval_mono (branch §6) are false under M1–M2 in their current form. Prove the replacements: (a) for a settlement step that pins a coordinate and rebuts or retires nothing, the forced interval on every coordinate is nested as before; (b) for a reopening step, the interval on a coordinate can widen by at most the width the removed rows had forced, stated exactly. Record the old statements as superseded in the registry if they were registered (they were not, as of #129; confirm).

A5. Re-verify #129. Every theorem in WarrantEntitlement.lean whose hypotheses mention a schedule or region: state whether it is unchanged, strengthened, or needs restating under settleForm. netWorth_ge_neg_odds should be unchanged (it is about rows, not about where they came from); Fixture.disagree_region_empty becomes false and is replaced by A2; orphan_region_nonempty/orphan_no_slack become the countermodel to the old rule and are kept as such.

Part B — the seed and convergence landing

Sources: round/2026-09-16-seed-statics (SeedStatics.lean and projects/normativity/seed/) and round/2026-09-17-convergence-measure (ConvergenceMeasure.lean). Both are 96+ commits behind main; port, do not merge.

**B1. One SeedStatics.lean on main** (M6): the declarations #129 ported, moved out of WarrantEntitlement.lean, plus from the branch's §6 the elimination machinery and forcedInterval, forcedInterval_spec, forcedInterval_bounds (the mono per A4); from §5 SureLoss, sureLoss_of_cert, FarkasCert.support_sound, MinimalInfeasible; Pins, Refuted, leverage; from §8 seed_independence_strict with its c3_refuted countermodel and sandwichSeed_humble; from §10 eventually_const_of_finite, eventually_const_of_monotone, tendsto_of_summable_drops. Not ported: §7 confinement, §9 transport (its negated-form drop is a known defect — file it, do not fix it here), §11 non-dogmatism. Say what was left and why in one table.

B2. The seed subproject. projects/normativity/seed/ as the branch lays it out, with the branch round's documents (SEED.md, STATICS.md, CRITERION.md, STABILIZATION.md, COUNTERMODELS.md, FIXTURES.md, REPORT.md) landed under projects/normativity/seed/rounds/2026-09-16-seed-statics/ verbatim with an ORIGIN.md saying they are a branch round landed by this one. Same for the convergence round under projects/normativity/seed/rounds/2026-09-17-convergence-measure/. Confirm checkers.workspace_state --check sees the subproject.

B3. The interval-data layer from ConvergenceMeasure.lean §1–§3: IntervalData, Valid, the hull/common/discord definitions, hullMass, overlapMass, discordMass, their bounds, Nested, hullMass_anti, discord_persists, discord_iff_pair, forcedRegionR_anti_warrants. The single-reasoner case (ι = Unit) is what Part C reports; the two-reasoner results land because they are cheap and the convergence round's items need them.

B4. Items from the two branch rounds. PR #102 filed items as 93–94 and #103 as 95–96; those numbers are taken on main. Re-file them from 117 with their content unchanged and a line saying which branch item each was. (The branch's item 93 collides with #101's item 93; the branch's is the one re-filed.)

Part C — the end-to-end witness (item 35)

One run, one fixture, every stage. The fixture is #129's four-sentence fragment extended by one sentence Z and a second warrant, so that there is something left standing after the first is rebutted.

C1. Seed. A Seed with one substantive item (the first warrant, strength < 1), one structural item (coherence of X∧A ≤ X, strength 1), and the constitutive layer empty. HumbleItems holds.

C2. Entry. Both warrants entered as Occurrences with provenance; VerdictCerts issued for the bound on Y and on Z; Licensed holds for both at entry (decideLicensed_iff).

C3. Compile and enforce. forcedInterval computed by elimination (not by hand) for Y and Z at entry; the force presentation built by toForceRow; liability_of_odds instantiated with the fixture's ρ.

C4. Settlement. X settles true at n₁. Intervals recomputed; nested per A4(a).

C5. Undercut. The first warrant's applicability port defeated at n₀ (defeat_widens); the certificate citing it fails Supported (admissible_not_supported); a fresh certificate on the second warrant still holds.

C6. Rebuttal. Y refuted at n_E. settleForm removes the strength row; the reopening is recorded; the interval on X∧A widens by exactly what A4(b) allows; the second warrant's interval on Z is unchanged; liability_rebutted holds; no orphan.

C7. Where it ends. After n_E nothing further settles. Show the interval data is eventually constant (eventually_const_of_finite on the finite docket), report the final forcedInterval on Z, the hull mass of the run as a sequence with its one reopening, and the trace of the run (MarketRun → Record) with docket_mediated holding at every step.

C8. The witness statement. One Lean theorem, EndToEnd.witness, whose hypotheses are the fixture's declared quantities and whose conclusion conjoins: the seed is humble; both entries licensed; IsLogicalInductor for the augmented market under the odds bankroll (via warrant_normative_inductor, keeping computableMarket and the uptake certificate as hypotheses exactly as it does); the interval on Z after n_E equals the value elimination computes; the run's record is neither injective nor constant. #print axioms. This is not registered; it is the object item 35 asked for, and the report says what it does and does not show.

What this round is told not to do

• No change to the force layer, the Normative Inductor architecture, or legitimacy.
• Do not port confinement or transport; do not attempt two-reasoner convergence beyond what B3 lands.
• Do not define the baseline B (item 110); do not touch the deference line's Lean.
• Do not re-derive #129's bankroll theorem; cite it.
• Do not cite any ruling not in DECISIONS.md after the round's first commit; M5 is the only chat-sourced material here and it is marked.
• Register nothing from Part C. Register from Parts A–B only what is lean-proved and listed in the output section.

Lean / formalization target

SeedStatics.lean (one copy, M6); WarrantEntitlement.lean importing it, with A1–A5; ConvergenceMeasure.lean (B3); EndToEndWitness.lean (Part C). Sorry-free, three allowed axioms, nonvacuity witnesses for every structure, #print axioms on every declaration. The report includes lake build output, the axiom audit line, and tests/run.py output — #129's report omitted all three and the registry carried five lean-proved entries on its word; do not repeat that.

Output

In the round directory: REPORT.md with a verification section; REBUTTAL.md (Part A); LANDING.md (Part B, with the ported/not-ported table and the item renumbering map); WITNESS.md (Part C, the run as a dated table: date, event, intervals on Y and Z, enforcer position, reopening, licence status of each certificate); src/ with the fixture and the run; PROVENANCE.md. A wiki page wiki/Seed-Theory.md (the branch rounds never got one), and the Normativity.md and Theorem-Spine.md entries it needs.

Registration candidates, lean-proved only, against the items named: settleForm soundness and Fixture.liability_rebutted (item 113); forcedInterval_spec, forcedInterval_bounds (item 39's geometric half); seed_independence_strict and eventually_const_of_finite (the re-filed seed items); hullMass_anti, discord_persists, discord_iff_pair (the re-filed convergence items). List the rest, do not register.

Final questions the report must answer

1. Does netWorth_ge_neg_odds survive settleForm unchanged? If not, exactly what changed.
2. By how much can one reopening widen a forced interval, and is that bound attained on the fixture?
3. Did the end-to-end run reach n_E with every stage's statement holding, or where did it stop?
4. What did the two branches contain that this round did not land, and which of it does item 35's next instance need?
5. What is reserved to the maintainer.

Report — 2026-10-21-rebuttal-and-end-to-end

Prompt author	the maintainer (prompts/2026-10-21-rebuttal-and-end-to-end/PROMPT.md, verbatim)
Executor	Claude Fable 5.1 (Anthropic), in Claude Code
Base	the branch round/2026-10-20-warrant-enforcement-semantics at b5cc2b1e, shipped in PR #129 (see Corrections)
Lean	SeedStatics.lean (133 declarations), ConvergenceMeasure.lean (55), WarrantEntitlement.lean (273, Part A added), EndToEndWitness.lean (121); all audited to the three allowed axioms, no sorry
Fixture	src/rebuttal.py, src/exhibit.py; tests/run.py (19 checks); the landed branch rounds' runners (28 and 20 checks)
Registrations	nine lean-proved entries in projects/normativity/CLAIMS.md, as the dispatch lists them
Filed	PRIORITIES.md items 117–123; items 35, 39, 112, 113 narrowed
Wiki	wiki/Seed-Theory.md (new); Normativity.md, Theorem-Spine.md, _Sidebar.md (entries)
Date	2026-10-21

Verdict. REBUTTAL-BY-SETTLEMENT-LANDS-THE-ORPHAN-CANNOT-FORM-THE-BANKROLL-ACROSS-ONE-REOPENING-IS-THREE-RHO-TIMES-TWO-PLUS-RHO-NOT-THREE-RHO-THE-SEED-STATICS-AND-THE-INTERVAL-DATA-LAYER-ARE-ON-MAIN-AND-THE-FIRST-END-TO-END-RUN-REACHES-THE-REBUTTAL-WITH-EVERY-STAGE-HOLDING. The gloss is in README.md.

Depends on 2026-10-20-warrant-enforcement-semantics (the odds bankroll, the licence chain, the fixture), 2026-09-16-seed-statics and 2026-09-17-convergence-measure (landed here as sources), 2026-08-16-traderized-enforcement, 2026-09-07-final-pressure-pass.

Corrections to the prompt (AGENTS.md §8)

1. Base deviation. The dispatch requires main after the merge of PR #129 and says to stop if WarrantEntitlement.lean is not on main. At dispatch time PR #129 was open and main was at 2b7a1453; the round stopped and reported. The maintainer then instructed: commit directly on round/2026-10-20-warrant-enforcement-semantics, ship both rounds in PR #129, keep this round's own directory and prompts/ entry, update the warrant round's report where superseded, and record the deviation here. Done as instructed; the warrant round's documents carry dated supersession notes rather than silent edits.
2. **IsForcedInterval.mono and forcedInterval_mono are not false** under M1–M2 in their current form: they are about forcedRegion, the unspecialized-row region with the row set fixed, and remain true and landed. What fails is their transfer to the settled region (Countermodel.settled_not_anti); A4 is proved for that region.
3. **"liability_of_odds applies with the same 3ρ"** is false across the rebuttal. The bound is 3ρ(2 + ρ) (netWorth_ge_neg_odds_reopened); the two-phase cushion exhibit realizes 24 > 12 on the fixture (REBUTTAL.md A2). Before n_E the bound is 3ρ.
4. M5 remained bracketed in the dispatch; the two rulings were landed from PR #102's citation and marked for confirmation (DECISIONS.md, 2026-10-21, second entry; queued).
5. **"The bound on Y"** (C2, C3): C1's fragment has no coherence row tying Y to X∧A∧Y, so Y's interval is [0, 1] throughout; the certificates and intervals reported are on the first warrant's conclusion coordinate X∧A∧Y.
6. **"forcedInterval computed by elimination (not by hand)"**: the kernel cannot evaluate the elimination over ℚ (decide and rfl stall on Rat normalization, probed and recorded). The elimination is run — the #eval lines in EndToEndWitness.lean print its output in the build log — and each interval theorem pins that output by the elimination's correctness theorem (forcedInterval_eq_of_bounds from forcedInterval_spec): valid bounds attained in the real region determine the computed pair. The hand part supplies the candidate and the attaining points, not the value's status as the elimination's output.
7. "One substantive item (the first warrant)" (C1): the first warrant is three forms; the seed's substantive layer carries the three, the second warrant enters as the warrant list W. HumbleItems holds.
8. B3 lists forcedRegionR_anti_warrants; forcedRegionR_anti_defeat and forcedInterval_nest_of_subset (the rest of the branch's §4) are landed with it because they are three lines and the convergence items cite them.
9. Retirement propagation. M2's "every row of that occurrence leaves" is realized one step along cites plus the settlement's closure; without closure a chain of three keeps its last link. Stated in REBUTTAL.md A1, tested, filed as item 121.

Part A — the rule and what it changes

REBUTTAL.md. settleForm with settleForm_eq_some_iff (P1's soundness), the contraposing shape lemmas, M3 as settleForm_strength; Grounds.survivors, settledRegion, region_subset_settledRegion. A2: Fixture.survivors_eq, schedRebutted_eq_survivors, no_strength_after, rebutted_region_nonempty, liability_rebutted at −3ρ(2 + ρ) through the new netWorth_ge_neg_odds_reopened; the harmonic buyer has nothing to buy (nothing_to_buy); the "same 3ρ" refuted (cushion_exhibit, test-supported). A3: Fixture2.old_rule_empty (the countermodel to the warrant round's premise-guard reading), survivors_refuteX, retired_region. A4: settled_not_anti, survivors_anti, settledRegion_anti_of_survivors_eq, settledRegion_subset_kept, reopening_bound; widening 0 on the fixture, attained. A5: the table in REBUTTAL.md.

Part B — the landing

LANDING.md. One SeedStatics.lean (§1–6, 8, 10 of the branch; §7, 9, 11 excluded by the dispatch; the transport's negated-form drop filed as item 122), WarrantEntitlement.lean importing it with its Part 0 removed, ConvergenceMeasure.lean §1–4. The seed subproject with both branch rounds verbatim and ORIGIN.md, their prompts, their runners green in the repository runner, normativity.seed in state/projects.json, their records in state/rounds.json. Items 93–96 of the branches re-filed as 117–120.

Part C — the witness

WITNESS.md. Every stage of C1–C7 is a theorem on the fixture; Run.witness is the conjunction of C8. The run reaches n_E and continues: the strength occurrence is rebutted at n_E by settleForm, X∧A's interval is [0, 1] before and after (the A4(b) bound attained with widening 0; the port-only rule would pin it to 0), Z's interval is [1/2, 1] at every date, the enforcer's bankroll is −3ρ(2 + ρ) = −72 and the conditional Normative Inductor composes, the record is neither injective nor constant and mediates the docket, and the hull mass runs 1/2, 5/12, 5/6, 1/2 with one reopening and is constant from n_E.

The five questions

1. **Does netWorth_ge_neg_odds survive settleForm unchanged?** Yes, verbatim: it is about the rows a schedule holds. What changed is what it is applied to: across a reopening the slack witness changes, and the applicable statement is the two-witness netWorth_ge_neg_odds_reopened with bound 3ρ(2 + ρ); before the reopening the old bound 3ρ applies with the old witness.
2. By how much can one reopening widen a forced interval, and is the bound attained? By at most the width the removed rows had been forcing off the kept rows' pre-step interval: both the pre- and post-step settled regions lie inside regionOn (survivors F') F (settledRegion_subset_kept, reopening_bound). On the fixture the removed strength row forced nothing on X∧A at the pre-step settlement, the allowed widening is 0, the actual widening is 0: attained with equality. The rule's effect on the fixture is to prevent the contraction to [0, 0], not to widen.
3. **Did the run reach n_E with every stage holding?** Yes, and beyond: C1–C7 hold as theorems at every date; C8 is Run.witness. The one place the run differs from the dispatch's picture is the bankroll constant (72, not 12) and the bound on Y (on X∧A∧Y, correction 5).
4. What did the branches contain that was not landed, and what does the next instance of item 35 need? Not landed: confinement (§7), transport (§9), non-dogmatism (§11) of the seed round; the discord certificate (§5), hull-mass convergence (§6) and the pinned fragment (§7) of the convergence round; both rounds' DECISIONS.md entries. A two-reasoner instance needs confinement and the discord certificate; the limit statement of P2 needs §6; a fragment that changes between dates needs transport, with its negated-form drop fixed (item 122). The first instance needed none of them.
5. Reserved to the maintainer. Below.

Verification

Run on 2026-10-21 in the worktree, lean/.lake linked to a populated cache (the memory note on local Lean setup applies).

$ ~/.claude/scripts/safe-lake.sh build          # the whole Workspace library
Build completed successfully (4090 jobs).

Per-file axiom audit (lake env lean on each file, every #print axioms line parsed):

SeedStatics.lean         133 declarations audited, disallowed: {}
ConvergenceMeasure.lean   55 declarations audited, disallowed: {}
WarrantEntitlement.lean  272 declarations audited (273 lines; one name with an apostrophe
                             the parser skips), disallowed: {}
EndToEndWitness.lean     121 declarations audited, disallowed: {}

The repository audit, re-elaborating every file:

$ python3 tests/audit_axioms.py
AXIOM AUDIT: 3017 results across 103 files, all within ['Classical.choice', 'Quot.sound', 'propext']

The repository runner (lean/.lake set aside for the run, as the untracked-pointers gate requires):

$ python3 tests/run.py
WIKI LINKS: clean over 32 page(s) (links resolve; repository links are commit-pinned)
WIKI STATE BINDINGS: clean over 34 page(s); 3 binding(s) verified against the state emission
Ran 68 tests in 5.522s  OK
GATE COVERAGE: 11 gate scripts, all invoked (5 self-test only — no local form)
LEAN SORRY GATE: clean over 103 files
LEAN AXIOM DISCIPLINE: every file carries `#print axioms`
ALL GREEN (78 project(s))
$ python3 -m checkers.run
REGISTRY projects/deference/CLAIMS.md:   registry schema: ok   105 entries, 0 adjudicated here
REGISTRY projects/normativity/CLAIMS.md: registry schema: ok   66 entries, 1 adjudicated here

The elimination, executed (#eval in EndToEndWitness.lean, from the build log):

intervalAt 0 XAY  = (2/5, 1)        intervalAt n₀ XA  = (0, 1)
intervalAt 0 Z    = (1/2, 1)        intervalAt nE XA  = (0, 1)
intervalAt n₁ XAY = (1/2, 1)        intervalAt nE XAY = (0, 0)
intervalAt nE Z   = (1/2, 1)        survivors at nE   = [1, 4]
decideLicensed … XAY certXAY 7 = true;  decideLicensed … Z (certZ 0) 7 = true

Round runners:

$ python3 projects/normativity/rounds/2026-10-21-rebuttal-and-end-to-end/tests/run.py
Ran 19 tests … OK
$ python3 projects/normativity/seed/rounds/2026-09-16-seed-statics/tests/run.py
Ran 28 tests in 12.179s  OK
$ python3 projects/normativity/seed/rounds/2026-09-17-convergence-measure/tests/run.py
Ran 20 tests in 55.916s  OK

What this round does not establish

• The cushion exhibit (24 > 12) is test-supported: two single-coordinate phases with a maker that zeroes the aggregate, not the pinned MarketMaker; the Lean proves the upper bound 3ρ(2 + ρ) and does not prove that 3ρ fails. Item 123.
• Retirement propagation is one step along cites; the fixtures rely on closed settlements. Item 121.
• The witness holds the computable-market and uptake hypotheses as hypotheses, does not run the market maker, and does not evaluate the elimination in the kernel (correction 6).
• Licensed and the record are still the warrant round's objects on the port-only bundle; their settled-bundle form is item 115's.
• The landed branch documents cite declarations not on main (listed in each ORIGIN.md).
• The two reasoners' results of ConvergenceMeasure §1–4 are landed and unused by the witness, which reports ι = Unit.

Items filed

117–120 (the branch items, re-filed, content unchanged), 121 (transitive retirement and the closure requirement), 122 (the transport's negated-form drop), 123 (the reopened bankroll's sharp form and the cushion exploit against the pinned maker). Narrowed: 35 (first instance landed), 39 (geometric half registered), 112 (the orphan cannot form under the rule), 113 (answered by the rule).

Registrations

As the dispatch lists, lean-proved: rebuttal.settleform-sound (settleForm_eq_some_iff), rebuttal.liability-rebutted (Fixture.liability_rebutted) against item 113; seed.forced-interval-spec, seed.forced-interval-bounds against item 39; seed.independence-strict, seed.eventually-const against item 117 (the re-filed seed items); convergence.hull-mass-anti, convergence.discord-persists, convergence.discord-pairwise against item 119. Listed and not registered: every other Part A and Part B theorem named in REBUTTAL.md and LANDING.md, and all of Part C.

Names, provisional

rebutted, vacuous, retired (the three removing outcomes of settleForm), reopening (a settlement step that removes rows), end-to-end witness (P3); and survivors, settled region, reopened mass, cushion exhibit.

Outstanding maintainer actions

1. Confirm or strike the landed 2026-08-08/09 rulings (M5) — DECISIONS.md, Awaiting the author, the 2026-10-21 entry.
2. Close PR #102 and PR #103 with a pointer to LANDING.md (M6).
3. Rule on the reopened bankroll — whether 3ρ(2 + ρ) is accepted as the entitlement across a reopening or the rule is to be tightened so that a rebutted row's counterparty gains do not cushion later selling (e.g. settlement-time accounting of the reopened mass); queued as the second 2026-10-21 entry.
4. Merge PR #129, which now carries both rounds; reserved on the pull request.

Rebuttal by settlement, the seed landing, and the first end-to-end run

Verdict: REBUTTAL-BY-SETTLEMENT-LANDS-THE-ORPHAN-CANNOT-FORM-THE-BANKROLL-ACROSS-ONE-REOPENING-IS-THREE-RHO-TIMES-TWO-PLUS-RHO-NOT-THREE-RHO-THE-SEED-STATICS-AND-THE-INTERVAL-DATA-LAYER-ARE-ON-MAIN-AND-THE-FIRST-END-TO-END-RUN-REACHES-THE-REBUTTAL-WITH-EVERY-STAGE-HOLDING — the rulings M1–M3 are one decidable function on the typed occurrence, settleForm, which keeps exactly the specialized rows of forms whose premise, antecedent and consequent are not pinned false, and the rows it removes are exactly the contraposing ones; under it the warrant round's orphan pin cannot form, the strength row leaves at the refutation, a slack world survives, and the enforcer's assessed net worth is at least −3ρ(2 + ρ) at every live world — the pre-reopening bankroll 3ρ plus ρ times a post-reopening slack mass the market's capital bounds by 3 + 3ρ; the dispatch's "the same 3ρ" is refuted by an exact two-phase exhibit in which a counterparty's gains on the rebutted row cushion its budget and the enforcer loses 24 > 12 on the fixture; retiring a refuted premise leaves the other warrant enforced where the port-only rule emptied the joint region; IsForcedInterval.mono stays true of the unspecialized-row region and fails for the settled region, replaced by nesting without reopening and an exact widening bound through the kept rows' pre-step region, attained with widening 0 on the fixture; one SeedStatics.lean (sections 1–6, 8, 10) and ConvergenceMeasure.lean (sections 1–4) are on main, the two branch rounds landed verbatim under the new seed subproject and their items re-filed as 117–120; and the end-to-end witness runs entry, licence, elimination, settlement, undercut, rebuttal and the record in sequence on one fixture, with every stage a theorem and the elimination's output pinned by its own correctness theorem where the kernel cannot run it.

Read REPORT.md first. The parts: REBUTTAL.md (Part A), LANDING.md (Part B, with the ported/not-ported tables and the item renumbering map), WITNESS.md (Part C, the run as a dated table). Lean: lean/Workspace/Normativity/Contrib/SeedStatics.lean, ConvergenceMeasure.lean, WarrantEntitlement.lean (Part A), EndToEndWitness.lean (Part C). Exact rationals under src/, run by tests/run.py. Wiki: wiki/Seed-Theory.md.

Dispatch: prompts/2026-10-21-rebuttal-and-end-to-end/PROMPT.md. Shipped in pull request #129 together with the warrant-enforcement-semantics round, at the maintainer's instruction.