Updated: 2026-09-06
The selected results are formalized across the finite-market, single-genre, two-user, profit, and infinite-producer parts of the paper. Local formula clarifications are reflected in the checked statements, and the source-faithful results are identified below by paper number.
Formalization gap: Theorem 2 uses a specific two-dimensional user model; Theorems 3–4 cover user vectors at angles below 90°; Lemma 2 proves a restricted equilibrium characterization.
| Paper results | Comparison with the paper |
|---|---|
| Propositions 1–3 | Exact. |
| Corollary 1 and Lemma 3 | Typo. The CDF exponent is corrected, and the resulting distribution and equilibrium are proved. |
| Example 1 | Formalization gap. The equilibrium construction is proved; the separate uniqueness sentence is not asserted. |
| Theorem 1 | Typo. The product characterization and its multi-genre alternative are proved with genre normalized only at nonzero support points. |
| Lemma 4 | Formalization gap. The paper’s span conclusion remains unproved. |
| Lemmas 1 and 5–8 | Formalization gap. The checked optimization route uses positive denominators and an attained product maximizer; it does not assert the unrestricted printed minimax identities. |
| Corollaries 2, 3, and 5 | Formalization gap. These are fixed-exponent existence and exclusion results; they do not assert the paper’s full supremal-threshold package. |
| Corollaries 4 and 6 | Typo. The two-user genre threshold and welfare conclusion are proved after the local formula and zero-normalization corrections. |
| Claim 1 and Proposition 4 | Exact. |
| Theorem 2 and Propositions 9–10 | Formalization gap. The selected phase results use the canonical two-dimensional realization of the two-user model. |
| Propositions 5–6, Corollary 7, and Lemma 13 | Exact. |
| Lemma 2 | Additional premise; formalization gap. Score-tie nullness is sufficient for the checked strict-CDF best-response equivalence; its necessity for a general tie-aware characterization is unresolved. The paper’s C1–C3 equivalence is not proved. |
| Lemma 9 | Formalization gap. The checked identity is the minimum cost over a feasible score fibre in the canonical two-dimensional model, rather than the cost of every content vector in arbitrary dimension. |
| Lemma 10 | Formalization gap. The displayed cost derivatives are proved; their identification with equilibrium density derivatives is not asserted. |
| Lemma 11 | Exact. |
| Lemma 12 | Additional premise; formalization gap. The support-slope inequality is proved from differentiated first-order identities and a negative-semidefinite payoff Hessian. Deriving them from equilibrium and C1 remains unproved; their necessity is unresolved. |
| Propositions 7–8 | Formalization gap. The checked conclusions concern every support action; Proposition 7 uses the Euclidean route. Passing to the paper’s expected-profit wording requires the corresponding population-law and integrability bridge. |
| Definition 1 and Theorems 3–4 | Typo fixed; formalization gap. Genre weights, the CDF quality cap, and the feasible angle domain are corrected; the construction proves the strictly acute two-user case above threshold. |
Except for the explicit Lemma 8 and Lemma 9 counterexamples, these omissions do not establish that the omitted source claims are false or that the stated restrictions are necessary.
The clarification memo gives the exact original-to-formalized comparison for both results.
Theorem 1’s product characterization is proved using an attained positive product maximizer and its supporting inequality, bypassing the unrestricted minimax step. See the optimization clarification.
None.
The source clarification memo is the single substantive account of the corrected CDF, nonzero genre convention, positive optimization domain, fixed-exponent thresholds, tie-aware characterization, canonical score-cost calculation, profit interpretation, and infinite-producer construction.
None.
PaperInterface.lean exposes 36 source-facing result specifications, and ProofInterface.lean supplies their checked endpoints. Selected expanded targets were compared directly for Example 1, Lemma 1, Theorem 2, Proposition 7, and Theorem 4. The result and prerequisite ledgers bind the remaining interface statements to the same source inventory.
status.json lists no standalone paper assumption declaration. Result-level hypotheses are visible in the interface specifications. The prerequisite ledger records six source matches and five corrected-target matches for the paper-local models and definitions. The finite-dimensional norm regularity convention is omitted from the public context summary because it follows from the paper’s norm model.
The statement map binds each selected result to its source presentation. The source-fidelity ledger records the CDF, genre, optimization, score-cost, derivative, profit, and infinite-producer corrections summarized in the public memo.
The library semantic ledger selects no paper prerequisite for a separate reusable-library review. The selected results rely on repository probability, fixed-point, compactness, and optimization foundations while retaining the paper-specific market and equilibrium definitions in this paper.
DependencyDAG.tex now presents the numbered paper models and results, their mathematical dependencies, and the three relevant reader statuses: exact, corrected source text, and formalization gaps. The compiled diagram was visually checked for readable labels, arrow direction, and node overlap.
The extended-valued threshold definition compiles and passes bounded independent source comparison. Its current closeout evidence is being synchronized; the retained receipt describes its pinned prior tree.
The retained focused-build receipt records a passing build for its pinned tree. The import-closure receipt records the refreshed checked import surface. The review packet was regenerated from the authenticated review graph, compiled, and visually inspected. Report structure, memo coverage, and rendered links pass. The retained final closure receipt describes the most recently completed terminal transaction.
The checked definitions cover the finite market, symmetric mixed equilibrium, quality and nonzero genre, single- and multi-genre regimes, the powered-score image, product condition and extended-valued threshold, the two-population and reparameterized equilibrium models, producer payoff, and Definition 1’s finite-genre formulation of the infinite-producer limit. Exact source routes appear in the statement map and prerequisite ledger.
The 36 selected results are Propositions 1–10; Theorems 1–4; Lemmas 1–13; Corollaries 1–7; Claim 1; and Example 1. Section 4 gives the comparison label for every group, and the clarification memo states every material difference.
The source-to-Spec ledger contains 36 recorded machine comparisons: eight source matches and 28 corrected-target matches. None of these rows carries a human-review judgment; this report gives the reader-facing interpretation of those machine comparisons.
The statement map inventories 47 source items: 36 selected results and 11 prerequisite model or definition items. The 36 result comparisons and 11 prerequisite comparisons account for the full inventory. Coverage is composed from those source-bound result and prerequisite reviews.