Updated: 2026-09-06
Formalized. The checked finite ordinal model covers score separation, convergence, and Theorem 1’s exponential ranking-error rate. Independent human review has not yet been recorded.
The source is Garg and Johari, Designing Informative Rating Systems: Evidence from an Online Labor Market. The governing target is a finite ordinal model with independent rating draws conditional on seller quality and independent seller histories. The source’s quality-only rating law and pairwise-probability factorization support this reading. The public archival source is the published article.
| Result | Comparison with the paper |
|---|---|
| Theorem 1; Appendix Lemmas 1–2 | Source clarifications: adjacent-pair indices and strict tails above the lowest rating; aggregate index. Formalization gap: connection to the population recurrence. |
| Pairwise and uniform-ranking objectives | Exact. |
Theorem 1 uses the declared iid rating model. Its connection to the printed population-state recurrence remains unproved; see the model boundary.
None.
The Appendix transfer uses a finite-support argument in the governing model of Section 3. The variational calculation keeps extended-real intermediate costs and proves finiteness at the final theorem boundary; see the governing-model clarification.
For finite ordinal models, prove score separation by selecting actual support endpoints rather than manufacturing terminal full support. Keep large-deviation objects extended-real through minimization, then prove a finite representative only at the final theorem boundary. Make joint-law completion a visible model field, not an inference from a suggestive recurrence name.
Connecting the declared iid law to the population recurrence is deferred; see Section 5.
The governing-model clarification gives the aggregate and adjacent-pair index fixes and restricts strict cross-quality tail comparisons to ratings above the lowest level. It also states the source’s positive-sampling and independence readings.
Section 10 links the local notation corrections; Section 7 describes the proof deviation.
PaperInterface.lean exposes the finite ordinal model, score formulas, iid bridges, Appendix rate lemmas, convergence claims, and the corrected finite-real Theorem 1 target. ProofInterface.lean contains the paired checked endpoints. The governing iid completion is a visible model input rather than an opaque product-law certificate.
Conditional iid ratings, independent seller histories, and positive sampling rates express the source model and its asymptotic proof conventions. Three paper-local prerequisites and five reused-library prerequisites have current matching judgments in the paper and library ledgers.
The source map records the floor sample count, corrected aggregate score, pairwise and uniform-ranking objectives, uniform normalization, log-mgf, real and extended rate functions, Appendix rates, and Theorem 1. The governing-model memo explains the exact index and codomain corrections.
Reusable finite-probability, ordinal-score, large-deviation, and finite-support lemmas remain separate from the paper’s horizon law and rating-system objectives. The paper namespace retains source numbering and the corrected model assembly.
The dependency DAG connects the finite model and formula definitions through the Appendix rate results to Theorem 1. Its retained 2026-09-04 visual inspection found the legend, labels, and directed edges readable with no clipping or overlap.
The current accepted graph binds three direct corrected-target judgments, three matching paper prerequisites, and five matching library prerequisites. The broader statement ledger records the checked formula and bridge rows. See the accepted graph and closure receipt. No new build or semantic review was run for this document edit.
Checked definitions include floor-counted seller histories, aggregate scores, adjacent-pair and uniform-ranking objectives, the finite ordinal iid state law, log moment-generating functions, and real/extended large-deviation rates.
Direct corrected-target judgments are recorded in the source-to-Spec ledger; the full formula/bridge comparisons are in the statement ledger, and correction provenance is in the source-fidelity ledger.
The source map inventories the model, formulas, Appendix claims, convergence statements, and Theorem 1. The coverage record binds the corrected model and rate items to their reader-visible explanations. The accepted graph is the current credential for the selected corrected surface.