| Assumptions (eq:primitive-prices, eq:main-domain, eq:adoption-domain) | no issue found | sympy: identities B-D=qm, C=mu-c+B, 2B-C=c(1-q); numeric check of illustration | high | The illustration (0.5,1,0.1,0.55,0.15) satisfies every stated restriction, so the admissible set is nonempty. n_A>1/2 is equivalent to qp>c. The g_*<h threshold reproduces 0.0915 < h. |
| Lem consumer (L298) | no issue found | line check of each demand piece, consistency and uniqueness, plus the p_1=mu convention | high | I checked each interval's consistency, why n cannot exceed min{H,h/D} at p_1=mu, and the no-sale case for p_1>mu. |
| Prop pricing (L356) | no issue found | line check plus sympy: capped root, Phi(n_A), Phi' bound via h/D<n_H | high | Checked: the branch profits; price-floor feasibility; the partial-exit dominance; that Phi is strictly increasing on [0,n_H] (A-2qmh/D>h); uniqueness of H_* in (0,n_A); the price-jump formula. Illustration H_*=0.4068 reproduced. |
| Prop share-welfare (L408) | no issue found | sympy: endpoint difference and peak gap; line check of regime slopes | high | Eq. (endpoint-welfare) and (peak-gap) match symbolically; R'(n_H)=D-h>0 supports the global maximum at alpha=1-n_H. Welfare values 0.3774/0.3983/0.2713/0.3733 reproduced. |
| Prop adoption (L507) incl. eq:adoption-gain, eq:explicit-switch | no issue found | sympy: W_f=Phi(f/D), dW_f/df, mixed-branch welfare identity, capped smaller root; line check of uniqueness by regime | high | Checked: uniqueness of H=f/D on (g_*,h) and of H=H_* with rho=f/g_* below g_*; the boundary correspondences; equivalence H_*<h/D iff (adoption-domain). The mixed welfare identity holds for g_*=DH_* and for g_*=h. |
| Prop postoffer (L599) | no issue found | sympy: profit form, W=R-t(1-n), all four f-derivatives; line check of demand and globality | high | dW/df=(f-K)/(2B), dCS/df=D/(2B)-1, and dPi/df=n_f all match. n_t-t/D is decreasing in t, so the interior claim holds. Numbers at f=0.10 (0.8056, 0.4188, 0.0813) reproduced. |
| Prop known-tastes (L679) and its exact certificate | no issue found | sympy: P_eps, F_eps, CS (by integration), physical welfare, welfare-slope and dCS/df via implicit differentiation, gap identity B(n_f-f/D)^2; exact rational check of line 1904 polynomial and Bernstein coefficients | high | All closed forms match after imposing the FOC. The line 1904 polynomial equals F_eps(n_f,f)-Q_eps(N_eps(f)) exactly, with Bernstein coefficients 0.034076, 0.020316, 0.009275, 0.000955. Fig. 3 values 0.84398/0.79956 and 0.37539/0.37238 reproduced. |
| Lem known-taste-preconfiguration (L740) | no issue found | close reading of interval structure and the price-raising deviation | medium | Checked: the activated set is an interval; E(t)=L(t)-f>0 and early-vs-manual slack h-f at the cutoff; feasibility of the price increase; the deviation leaves early mass and later revenue unchanged. |
| Prop positive-rents (L779) | no issue found | sympy: welfare identity and slope, price-slope at p_0; line check of low-, high- and exit-price deviation bounds | high | Each of (eps-human-slack) to (eps-welfare-slope) delivers the step it is cited for. The agent-early bound Pi_A(n_A)+eps < Phi(H)-eps H and the high-price bound (A+eps)n are correct. |
| Prop fixed-info-dispersion (L840) | no issue found | line check of switching-interval profits and derivatives; hand and sympy check of welfare via physical accounting | high | Prices, H^fix, g_eps, U^fix and W^fix follow. Physical-surplus accounting gives the same W. Illustration values 0.0737, 0.3057, 0.4557, -1.0038 reproduced. |
| Prop fixed-info (L1132) | no issue found | line check of candidate profits, H_s, adoption lottery and welfare | high | Pi_E=qsm+delta and Pi_C=qsm+H(delta+g_s) follow. Expected welfare mu-c-f also matches physical accounting with rho=f/g_s. |
| Cor coordination (L1101) | no issue found | line check against Prop share-welfare and Prop adoption | high | The objective on [0,1-n_H] is linear with slope h-f. Shares beyond 1-n_H have W<R(n_H) and larger setup expenditure. Every private equilibrium has H<n_H. |
| Cor postoffer-fixed-information (L1182) | no issue found | line check | high | Checked threshold feasibility, the all-wait profit qsm, and the advantage delta+f>0. |
| Prop general-report (L906), its curved certificates and the saturation reversal | no issue found | sympy: welfare identity C_a+eps(1-H), slope; F_a'' for the saturated case; dense-grid numerics for the beta table and saturation bounds | medium | The proof steps and the M>qm sign claim follow. Saturated bounds reproduce: max F_a about 0.09997 < 0.10391; C_a(0.52) about 0.10690; slope -7.3244 at H=0.5. The four beta-table gaps reproduce to six digits. The C^1-neighbourhood claim (line 931) is only sketched at lines 2468-2477; I found no counterexample. |
| Prop consumption-network (L1251) and noisy-report mapping (L1272) | issue found | sympy: P_k, F_k, E[T^2]; line check of the limit argument; hand check of noisy coefficients | medium | The closed forms and the noisy-coefficient mapping hold. The compactness step that excludes far-away maximizers is terse about zero-surplus ties in the k=0 limit (F19). |
| Prop anticipated-regular-price (L1317) | no issue found | sympy: closed-form Pi_eps at line 2697, T_eps at line 1343, g_* derivative polynomial; hand check of welfare-derivative limit and the 0.008540 error bound | medium | Pi_eps, T_eps=4(5eps+10f+2)/9 and g_*(0.525)=0.0936192 match. The x-derivative polynomial matches up to a positive factor. The total error bound evaluates to about 0.008539 at lambda=3000. The four box-wide derivative bounds were not rechecked. |
| Prop flexible-price (L1373) | no issue found | sympy: R_max=C^2/(4B), W^FB(n)=M+Kn(1-n); line check of upper bound | high | Profit is R(n)-Dn under full delegation. The upper bounds for p<=mu and p>mu and the planner comparison K/4>K^2/(4B) hold. |
| Prop postoffer-joint-price (L1403) | no issue found | sympy: value at n^J and n^J identity; line check of surplus upper bound | high | The bound derivative C+t-2Bn >= t-K settles case 1. Bn^J>t_f holds because 2B-K>t_f. The t_f=0 supremum sequence gives (C-D)^2/(4B). |