Updated: 2026-09-09
The finite-rating model’s convergence and exponential ranking-error rate are formalized.
Garg and Johari, Designing Informative Rating Systems: Evidence from an Online Labor Market. The checked model has finitely many ordered seller types and rating levels. Ratings are independent conditional on seller quality, and sellers’ rating histories are independent. The scope covers ranking objectives, convergence, and Theorem 1.
| Result | Comparison with the paper |
|---|---|
| Theorem 1; Appendix Lemmas 1–2 | Exact with source clarification. Indices, probability calculation, population model. |
| Pairwise and uniform-ranking objectives | Exact. |
None for the stated independent-rating model.
None.
The probability proof works directly with finite rating histories; see the Appendix calculation.
Assign infinite cost to impossible scores before minimizing the rate function. Use actual support endpoints to prove score separation without requiring every rating to occur with positive probability.
None recorded.
The memo explains the positive rating-arrival rates and independence conventions. It also gives the index and endpoint clarifications and clarifies the time indices in the population update.
None beyond the source clarifications in Section 10.
PaperInterface.lean states the model and selected results; ProofInterface.lean connects them to their proofs.
The model review covers independent rating histories and positive rating-arrival rates. The library review checks the definitions used from the shared library.
The source map links rating counts, average scores, ranking measures, and rate formulas to their paper passages and formal statements.
Reusable results cover probability on finite sets, averages of ordered ratings, and exponential probability bounds.
The dependency diagram traces the model and Appendix lemmas to Theorem 1.
Build and mathematical-review evidence is recorded in the closeout record and its linked records. Independent human sign-off has not yet been recorded.
Checked definitions include rating counts, average scores, pairwise and overall ranking measures, the joint distribution of seller types and scores, and the rate functions used in Theorem 1.
The statement review compares the selected results with the source. Further formula comparisons appear in the formula review, with source clarifications in the source-fidelity record.
The source inventory lists the model, formulas, Appendix claims, convergence statements, and Theorem 1. The coverage review records how these are covered by the formalization.