Item 114: The pinned-region divergence against the pinned market maker

The odds bankroll (WarrantEntitlement.netWorth_ge_neg_odds) is the sufficient half: a live slack world dominating every live deficit at the odds gives −3ρ. The round's converse is test-supported only: against a nonempty region with no slack live world and a live deficit world, a harmonic buyer drives the enforcer's assessed net worth to −∞ under a one-coordinate market maker that zeroes the aggregate. Wanted: the same against the dependency's MarketMaker — that for such a region there is an efficiently computable trader under which (realizedEnforcer L E).netWorth (history L E) v n is unbounded below at a live v. That is item 40's necessity direction restricted to pinned regions, and the one place the round found it true.

Deliverable shape: derived or better: a Lean statement over history L E with the trader exhibited, or the obstruction in the maker's fixed point. Acceptance check: Lean green; the statement's hypotheses inhabited by the round's fixture. Context: .../2026-10-20-warrant-enforcement-semantics/COUNTERMODELS.md §3; src/fixture.py::harmonic_buyer_run; item 40.