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
- held by normativity
Rounds and decisions that touch it
None recorded.