# Verification Status for the Discrete Draft

The current `paper_v2` draft uses a discrete-time dynamic game as the main model.
Continuous time is retained only as a small-period appendix approximation.

## Modeling choice

Use the discrete model for the paper's main claims. It keeps the timing, kinked Bertrand
payoffs, mixed equilibria, and finite-state Bellman-Nash object explicit. Use the
continuous-time HJB only for local first-order intuition and smooth comparative statics.
Do not cite the continuous-time thresholds as global equilibrium results for the corrected
paper.

## Current checks

Run these from the repository root:

```bash
python3 verification/discrete_dynamic_game.py --s 1 --output verification/discrete_dynamic_game_output.json
python3 verification/current_paper_symbolic_check.py
```

`discrete_dynamic_game.py` computes a finite-horizon grid version of the model by
backward induction. At each date and state it solves the finite continuation bimatrix
game and records the selected equilibrium. The default website artifact uses the pure
one-shot benchmark (`--s 1`) so parity has a symmetric selected equilibrium in the
reported diagnostic.

`current_paper_symbolic_check.py` is retained as an algebra regression test for the
underlying payoff, compute-market, access-pricing, and continuous-time approximation
identities. It is no longer the main equilibrium check.

## Scope

The current draft establishes:

- the two faces of task reliability;
- one-period no-inactive-settlement mechanics;
- finite-horizon Markov-perfect equilibrium by backward induction on finite games;
- stationary Markov equilibrium existence for the finite discounted stochastic game;
- compute-market scarcity accounting;
- composition/kink and access-pricing implications.

It does not claim uniqueness, global continuous-state equilibrium existence, convergence
of grid equilibria to a continuous-state equilibrium, or empirical magnitudes.
