predict: certify pricing error and apply NAV bid/ask

.claude/rules/predict-contracts.md

@@ -135,17 +135,17 @@ Predict-specific Move rules: package architecture, config and capability shapes,
 - Terminology: docs use options/structured-product vocabulary (canonical glossary: `packages/predict/docs/glossary.md`). Mint-economics identifiers are `entry_value`, `net_premium`, `financed_amount`, `min_net_premium` (and the `OrderMinted.net_premium` event field). The `floor_*` family (`floor_shares` = the static floor `F`, and `floor_amount`) is the payoff primitive — never rename it to financing/debt vocabulary; the glossary bridges the two. The EWMA congestion surcharge keeps core's `penalty` vocabulary in code.
 - For Predict mint slippage, spell out what the bound controls. `mint_exact_quantity`'s `max_cost` caps the all-in account withdrawal (`net_premium + trader-paid fee + builder_fee + EWMA penalty`), while `max_probability` caps the quoted per-contract probability before fees. `mint_exact_amount` caps only the `net_premium` budget and uses `min_quantity` as the slippage guard; fees and penalties are paid on top. `OrderMinted` emits payment components separately, not a total. If the check is just summing local payment components, keep the sum in the assert instead of adding a one-use helper.
 - Leveraged Predict economics are part of the contract terms. Leverage sets a static deterministic floor `F` frozen at mint (`floor_shares = F`); pricing, NAV, payout, settlement, and liquidation model one contract with a static floor and a knock-out level, deriving value from the packed order terms rather than bolting on separate leverage-specific scans. A winner redeems `quantity - floor_shares`; the order knocks out when its gross value reaches `floor_amount / liquidation_ltv`.
-- Contract floors should track only the atomic values needed by each index. NAV is the exact per-expiry recoverable value (payout-tree `walk_linear` minus the leveraged `correction`, floored) — economically `Σ qty·P - Σ min(qty·P, F)`. Payout backing uses the exact terminal payout `quantity - floor_shares` plus the aggregate disjoint-backing λ buffer, so live backing can be read without scanning or passing a clock.
+- Contract floors should track only the atomic values needed by each index. NAV carries the approximate per-expiry recoverable value (payout-tree `walk_linear` minus the leveraged `correction`, floored) as one signed center-plus-error certificate — economically `Σ qty·P - Σ min(qty·P, F)`. Payout backing uses the exact terminal payout `quantity - floor_shares` plus the aggregate disjoint-backing λ buffer, so live backing can be read without scanning or passing a clock.
 - An index may aggregate raw order atoms or derived terms. If it aggregates derived terms, removal must subtract bit-equal what insertion added, so the term derivation must be a single owned function (the canonical evaluator, `strike_payout_tree::payout_terms`) called by mint insert, remove, reinsert, and any settlement recompute — never re-implemented per call site. The evaluator must stay pure (snapshotted config plus caller atoms only; no clock, no oracle, no policy asserts — mint admission stays in the mint-only wrapper), every atom it reads must round-trip losslessly through the packed order ID — the id packs boundary ticks, `quantity`, `floor_shares`, and `sequence`, so a lossy repack of `quantity` or `floor_shares` is an accounting bug, not a precision nit (`opened_at_ms` is no longer packed) — and the snapshotted config fields it reads (e.g. `backing_buffer_lambda`) must never gain live-expiry setters. Re-calling the evaluator or one of its sub-primitives is free and safe; re-expressing its formula anywhere is the violation. Flow policy (e.g. mint admission) validates its bounds *before* evaluating terms, so the evaluator's own aborts always mean a broken atom round-trip, never bad flow input.
 - Payout backing for a winning order is the exact `quantity - floor_shares` (equal to the settled payout under the static floor); the only conservatism is the aggregate disjoint-backing λ buffer (D030). Do not reintroduce a clock-dependent or rising-floor max-live backing term — the static floor makes the terminal payout exact.
 - NAV may use aggregate floor accounting only under an explicit precondition that every active leveraged order is individually above its floor before valuation. If that invariant is not maintained by the surrounding health/liquidation flow, aggregate subtraction can overstate recoverable value and the implementation must fall back to exact per-order recoverability or another exact representation.
 - For leveraged Predict economics, the contract floor is limited-recourse to the order that created it. A floor can offset only that order's live value or settled payout, capped at that value/payout. Do not treat aggregate floor value that exceeds aggregate position liability as positive NAV unless the implementation explicitly models exact per-order recoverability.
-- **NAV-mark directional invariant — never undercount the SUPPLY mark.** The NAV mark that prices PLP **supply** must be an *upper bound* on true recoverable value (`supply_NAV >= TRUE_NAV`): a supplier priced `>= TRUE` mints `<=` fair shares, so it can never over-mint and dilute incumbents. The flush prices supply AND withdraw at **one mark** — `pool_nav = idle + Σ active-expiry current_nav` (net of the pending-protocol-profit exclusion), computed once in `finish_flush` and passed to both queues in `drain_lp_requests` — so that single mark must equal TRUE in both directions. It does: each `expiry_market::current_nav` is the **EXACT** per-expiry recoverable value (free cash minus the exact per-order live liability = payout-tree `walk_linear` minus the leveraged-book `correction_value`, floored at zero), so `supply_NAV = TRUE` at the valuation boundary — never an under- or over-count. There is **no conservative band** (the bucket/band decomposition belonged to the deleted approximate-NAV world); NAV manipulation is closed by the **privileged** cron flush (audit L8), and dilution by the fair FIFO drain at the frozen mark. A liveness clamp inside `current_nav` (the degenerate-underwater `saturating_sub` cash floor) must *maximize* NAV when it fires. A settlement-dependent mark — a **past-expiry-but-unsettled** market — has no well-defined TRUE, so it cannot be valued until settlement-v2: do NOT substitute an approximate mark (contribute-0 dilutes incumbents on supply; free-cash over-pays withdrawals — both break the single-mark dual-use). This is the documented flush-liveness precondition on `expiry_market::current_nav` / `plp::value_expiry`.
+- **Numerical-certificate policy — fail closed where uncertainty transfers economic value.** Pricing creates an `Approx` as soon as numerical error exists and carries that center-plus-error fact intact until the policy owner deconstructs it. Mint admission aborts before creating an order when the contract-price certificate exceeds 0.1%, because an uncertain entry price transfers real value between the trader and pool. Full-pool valuation aborts before draining queues when the pool-NAV certificate exceeds 1%; within that bound, `finish_flush` freezes one paired mark over the same pre-drain PLP supply: supplies price at `center + error` (`supply_NAV >= TRUE_NAV`, preventing over-mint dilution) and withdrawals at `center - error` (`withdraw_NAV <= TRUE_NAV`, preventing overpayment). A zero center produces two zero, non-executable marks so the flush can complete without moving value. This certified bid/ask is not the deleted heuristic NAV band or a withdrawal fee: it is the terminal interpretation of one propagated error certificate. Live close and liquidation continue to use the canonical scalar center with no certificate-dependent branch; liquidation's protocol-chosen LTV threshold already carries a materially larger economic buffer, so numerical error does not create a second liquidation boundary. The privileged flush still closes oracle-timing manipulation. A settlement-dependent **past-expiry-but-unsettled** market has neither a well-defined center nor a certifiable error bound and therefore still blocks valuation; do not substitute a synthetic mark.
 - Leveraged Predict orders must satisfy `floor_shares <= quantity` (`F <= Q`) at creation — the static floor cannot exceed the max payout. Trading fees and builder fees are transaction costs, not floor value, and should not be included in this invariant.
 
 ## Predict Gas & Capacity
 
 Measured localnet capacity findings live in `packages/predict/predeploy/evidence/` (consolidated model: open-items C-1). Respect them when touching the flush / NAV / liquidation paths.
 - **The full-pool flush is ONE mandatory PTB** (`PoolValuation` is a hot potato) that values EVERY active market. The landed NAV price memo made the single-market 5,000 leveraged-order cap safe in the measured cheap branch (~2.36-2.68B MIST, ~47-54% of the wall), but the independent caps (24 markets / 1,000 nodes / 5,000 leveraged) still do not compose: the pool-total case OOGed around 8.6k leveraged orders across ~9 markets before a clean gas-only boundary was isolated. Any new growth-sensitive cap must be checked against `Σ_markets` under the ~5M computation wall, not in isolation.
 - **A batched leveraged mint/redeem amplifies the per-op cost vs standalone (measured ~15-20× at a saturated book, replicated across 2 runs; a PTB of ~110-150 leveraged mints OOGs the 5e9 cap — data-dependent on book, and a 100-mint PTB is ~3.4B = 68% of the cap).** The mechanism is per-TRANSACTION metering / command-position accumulation, NOT liq-book dirtying: a leveraged mint appended after 20 *1x* mints — which never touch the liquidation book (`insert_order` is a no-op for 1x) — is amplified just as much (more, by position), so the cost scales with command POSITION / accumulated tx state, not with prior `insert_order` writes to `book.pages` (harness `mint-batch` experiment, `packages/predict/predeploy/evidence/c3-mint-batch-2026-07-01.md`; this REFUTES the earlier "dirtied dynamic fields" claim). `range_price` (`select_liquidation_candidates`) is pure math. Don't assume an op's standalone cost holds when batched — and the ceiling binds ANY large multi-command PTB, not just scan-heavy ops.
-- **`lp_pool_value` floors at 0** (`gross.saturating_sub(exclusion + pending_protocol_profit)`); when the sticky profit basis exceeds a collapsed gross it returns 0, and `supply_shares`/`withdraw_dusdc` then abort `EInvalidDrainMark` — a supply/withdraw brick. Treat NAV==0 as a real reachable state, not just an underflow guard.
+- **`lp_pool_value_approx` floors its center at 0** after subtracting the exact exclusion and pending protocol profit; when the sticky profit basis exceeds a collapsed gross it returns a zero-center certificate, and `finish_flush` creates two zero, non-executable marks so queued supplies and withdrawals are refunded rather than bricking the flush. Treat NAV==0 as a real reachable state, not just an underflow guard.