Updated: 2026-09-04 (terminal-closeout document refresh)
Formalized. Theorems 3.1–3.2 establish the fixed binary rating model’s prior-strength and quality comparisons, with weak variance decrease at Bernoulli endpoints.
10.1609/icwsm.v19i1.35865.cited publication, SHA-256
cad80c0adb745f89aab8324ba42f5570150875885b6074bca6ec5cd9fc128422.cited publication, SHA-256
c5ae8e229ea8033e636af335e5d63f5dd27e098492c9fb013f333e71edd5c1f9.The closeout’s ordinary named-theorem scope is Theorems 3.1–3.2. The fixed-model formula family in Section 2 and Appendix A is a source-mapped semantic prerequisite. Appendix D and Appendix E corrections below are explicit supplementary formula records; they do not inflate the named-result inventory.
The source describes discrete time and one accumulated binary rating
per fixed-model timestep. The formalization therefore uses
t : Nat and 0 < t for these source-facing
fixed-model statements, rather than silently extending time to an
arbitrary positive real. This is a source-supported model reading, not
an extra proof assumption; it is bound to the direct and prerequisite
review targets.
The named results explicitly retain the source’s positive Beta-shape, nonnegative prior-strength, ordered-strength, and Bernoulli-quality-domain conditions. No additional substantive model premise is used.
| Result | Comparison with the paper |
|---|---|
| Beta–Bernoulli model and posterior identities; Theorem 3.2 | Exact. |
| Theorem 3.1 | Source clarification: variance decreases weakly on
the closed Bernoulli interval 0 <= q_v <= 1. |
| Appendix D, Equation (20) | Typo fixed: Beta(C,1-C) replaces
Beta(C,1). |
| Appendix E, Equation (21) | Formula corrected: include prior pseudo-counts in numerator and denominator. |
None.
None.
None.
None.
No generalization is used to prove the source-facing named results.
The underlying real-analytic lemmas are reusable support after the
natural review count is embedded in Real, but they are not
presented as a broadened paper-facing time model.
The source clarifications give the quality-endpoint variance correction and the Beta/Dirichlet formula repairs. They preserve the named comparisons on the stated domains.
None. The three localized source corrections are formalized and disclosed; they are not unresolved caveats or claims of archival equivalence.
PaperInterface.lean exposes the
fixed binary model and transparent targets for Theorems 3.1–3.2; ProofInterface.lean contains their exact
proof endpoints. The proofs cast the natural review count to
Real only inside analytic identities. Appendix D and E
formula repairs are checked supplemental endpoints rather than extra
named results.
No additional assumption is used. The fixed-model prerequisite carries the source’s discrete positive time, Beta-shape, prior-strength, and Bernoulli quality domains and has a current matching judgment in the paper-prerequisite ledger. No material library prerequisite is selected.
The source map binds the
Beta–Bernoulli posterior, bias and variance formulas, Appendix D’s
corrected Beta(C,1-C) identity, and Appendix E’s corrected
prior-inclusive posterior average. Exact repairs are in the source memo.
The proofs reuse general real-analytic identities after embedding the natural count, while the discrete rating model and paper theorem composition remain paper-local. The accepted graph records no material reusable-library review row and no new lift is claimed.
The dependency DAG contains the fixed-model prerequisite, the two named theorems, and the disclosed supplemental formula corrections. Its retained one-page visual inspection found all nodes, arrows, labels, and correction notes legible and unclipped.
The completed closeout records one exact direct judgment, one corrected-target direct judgment, and one matching fixed-model prerequisite. The accepted graph and closure receipt bind the focused build, source review, proof routes, and document checks. No new Lean or semantic review was run for this reorganization.
Checked definitions include the fixed binary rating process, Beta prior and posterior parameters, posterior mean, squared bias, variance, prior strength, and Bernoulli quality domain.
The two direct comparisons are in the source-to-Spec ledger; the model premise is in the paper-prerequisite ledger, and correction provenance is in the source-fidelity ledger.
The coverage ledger records the current source presentations as covered. The source map distinguishes the two named results, the fixed-model prerequisite, and the supplemental Appendix D/E correction records; the latter do not inflate named result coverage.