Updated: 2026-09-07
The incentive-compatibility, renewal-reward, and pricing results are proved on their stated domains, and Theorem 3’s conclusion has a direct proof.
formalized.Scope: the paper’s single-state and dynamic incentive-compatibility definitions, threshold-policy and renewal-reward material, Lemmas 1–10, the unnumbered Proposition in Section 3.1, and Theorems 1–4. Empirical and calibration material outside those named theoretical claims is not part of this formalization.
| Result | Comparison with the paper |
|---|---|
| Driver-surge model and incentive-compatibility definitions | Exact. |
| Lemmas 1–3 | Exact. |
| Theorem 1, the unnumbered Proposition in Section 3.1, and Lemma 4 | Exact. |
| Lemma 5 | Exact. Source clarification. |
| Lemmas 6–8 and 10 | Exact. |
| Lemma 9 | Exact. |
| Theorem 2 | Exact. |
| Theorem 3 | Exact. |
| Theorem 4 | Exact. |
None.
None.
The printed Lemma 9 chooses a feasible price ratio after fixing a non-surge policy. Its conclusion is therefore policy-dependent, whereas the Theorem 3 argument needs one price to work uniformly over deviations. The checked proof instead fixes a structured price before optimizing and handles the target-rate range in two cases. The theorem’s conclusion and source policy domain are unchanged.
None.
No additional generalization is established here.
The Lemma 5 memo records its endpoint reading. The Lemma 9/Theorem 3 memo records the price-policy proof route.
None.
PaperInterface.lean exposes the incentive-compatibility definitions, renewal formulas, Lemmas 1–10, the unnumbered Proposition in Section 3.1, and Theorems 1–4 through eighteen transparent targets. ProofInterface.lean supplies their checked endpoints, including the fixed-price-before-policy Theorem 3 route.
The current paper-prerequisite ledger records thirteen matching graph-selected prerequisites. No material reusable-library prerequisite is selected for this surface.
The source map binds earning rates, switching probability, post-exit time fractions, threshold rewards, structured prices, and derivative/response-shape formulas to their source spans. The clarification memo records the Lemma 5 endpoint reading.
The development separates generic renewal-reward and policy-comparison arguments from paper-specific driver states, prices, and response functions. No additional shared-library extraction is claimed by the accepted graph.
The dependency DAG orders the model, renewal lemmas, policy-shape lemmas, and four theorems. Its retained 2026-09-05 visual inspection found the nodes and directed dependencies legible and consistent with the reviewed surface.
The current graph records sixteen matching direct source-to-Spec judgments and thirteen matching paper prerequisites. The paper-coverage ledger separately records thirty items covered, four as support, and two with recorded boundaries. Section 4 gives the current source-facing interpretation. The accepted graph and closure receipt bind the formalized surface.
Checked definitions include surge states, single-state and dynamic incentive compatibility, threshold policies, measured rewards, earning rates, switching and exit times, structured prices, and the two-state feasible policy domain.
Direct judgments are in the source-to-Spec ledger, row-local comparisons in the statement ledger, and premise judgments in the paper-prerequisite ledger. The source-fidelity ledger records the price/policy proof change and added domains.
The coverage ledger distinguishes thirty covered items, four support-only items, and two source-convention readings across the theoretical inventory. The source map links those items to the current interface; empirical and calibration material remains outside the selected scope.