Alignment Workspace

Item 126: The bankroll across repeated reopenings

Deference line — second wave · difficulty substantial · project normativity · open · node item-126

OddsBankroll.Account.netWorth_ge_neg_odds_reopened gives −cap·ρ(2 + ρ) across one reopening from a slack world before and one after. A run with k rebuttals needs k + 1 slack worlds and a bound; iterating the one-step argument suggests −cap·ρ·(2 + ρ)^k or better, and nothing is proved. Wanted: the k-reopening bankroll on the abstract account, and whether a settlement-time accounting of the reopened mass (item 123) makes it linear in k.

Deliverable shape: lean-proved on OddsBankroll.Account. Acceptance check: the Lean audit clean; the one-reopening theorem recovered as k = 1. Context: lean/Workspace/Normativity/Contrib/OddsBankroll.lean; item 123. Consumed by: any run with more than one rebuttal; the asymptotic corollary of .../THEOREM_STORY.md §F beyond one revision.

Deliverable shape: lean-proved on OddsBankroll.Account.

Acceptance check: the Lean audit clean; the one-reopening theorem recovered as k = 1.

Context: lean/Workspace/Normativity/Contrib/OddsBankroll.lean

Registered results bearing on this item

None registered.

Where it hangs

Rounds and decisions that touch it

None recorded.