THEOREM_AUDIT — proof ledger (status: proved / conditional / numerical / open / false)
Statement ids follow the paper. "source" = prior draft (PD), literature (L) or new (N). Independent checks: theory/symbolic_checks.py
(S1–S8), tests/ (T), Monte Carlo (MC).
| id | statement | status | assumptions | source | independent check | counterexample attempt | paper location | unresolved |
|---|---|---|---|---|---|---|---|---|
| L1 | Influence preservation: Σ_j w_j T_{s_j,k} has influence term U_k = m^{-1}Σ_{i∈D_k}ψ(X_i) exactly (Σ w_j = 1) | proved | A1 | PD (r=2,3) → N (general r) | T: test_combine_levels; S1 | – | App. A.1 | – |
| L2 | Bias cancellation: ‖E J_{r,k} − θ0‖ ≤ C_b m^{-r} Σ_j | w_j | s_j^r; exact exponential biases −2θ0/((m−1)(m−2)), 8θ0/((m−1)(m−2)(m−4)) | proved | A1, A2(r) | PD → N | S3; T: test_exact_bias_of_split_estimators | – |
| L3 | Local remainder: (E‖R^J_k‖²)^{1/2} ≤ √C A_r/m with A_r = Σ | w_j | s_j (= 4, 8, 80/7 for r = 2, 3, 4) | proved | A1 | PD (16C/m²) → N (constant) | S8 | – |
| L4 | Averaged centred remainder: E‖K^{-1}Σ_k(R^J_k − ER^J_k)‖² ≤ C A_r²/(K m²) | proved | A1 (block independence) | PD → N | – | – | App. A.1 | – |
| L5 | Pilot vs centralized MLE: θ^{(0)}_r − θ̂_N = O_p(m^{-r} + (m√K)^{-1} + N^{-1}) | proved | A1, A2(r) | PD → N | MC (exp, logit, pois) | – | App. A.1 | – |
| L6 | Newton contraction ‖N_N(ϑ) − θ̂_N‖ ≤ ½ M_N Λ_N ‖ϑ − θ̂_N‖² when ϑ, θ̂_N ∈ U | proved | A3 | L (standard) / PD | S4 (exact identity in exp model); T: test_newton_identity_on_data | – | App. A.2 | – |
| L7 | q steps: ‖θ^{(q)} − θ̂_N‖ ≤ (½M_NΛ_N)^{2^q−1} ‖θ^{(0)} − θ̂_N‖^{2^q} on the event that all iterates stay in U; iterates stay in U w.p.→1 when θ^{(0)} →p θ0 | proved | A3 | PD (sketch) → N (explicit) | S5 | – | App. A.2 | – |
| T1 | (r, q) frontier: under A1, A2(r), A3, if K = o(N^{α(r,q)}) with α(r,q) = 1 − 1/(2^{q+1}r) and m → ∞ then √N(θ^{(q)}_r − θ̂_N) →p 0 and √N(θ^{(q)}_r − θ0) ⇒ N(0, Σ_ψ) | proved | A1, A2(r), A3 | PD (Thm 4.2, Cor 4.3, Cor 6.1, Prop 6.2) → N (unified, with the stochastic term tracked) | S8 (exponent table); MC rate study | boundary case (Theorem 2) shows the small-o cannot be replaced by O | §5, App. A.2 | constants depend on p through C, M_N, Λ_N (fixed p only) |
| C1 | Inferential validity: Wald intervals with any consistent estimator of Σ_ψ (aggregated observed information, or sandwich from aggregated score outer products) have asymptotically nominal coverage under T1 | proved (Slutsky) | T1 + consistency of the covariance estimator | N | MC coverage tables | misspecified design: Fisher-based intervals under-cover, sandwich does not | §5.3 | – |
| T2 | Exact exponential model: (i) E θ̂_n = θ0 n/(n−1), Var = θ0²n²/((n−1)²(n−2)), E R_n = θ0/(n−1), E R_n² = θ0²(3n+2)/(n(n−1)(n−2)), sup_{n≥3} n²E R_n²/θ0² = 16.5; (ii) E J_{r} − θ0 = θ0 Σ_j w_j s_j/(m − s_j) with leading term β_rθ0m^{-r}; (iii) Var J₂ = θ0² m²(m²−6m+17)/((m−4)(m−2)²(m−1)²); (iv) N(x) − θ̂_N = −(x − θ̂_N)²/θ̂_N and N^q(x) − θ̂_N = −(x−θ̂_N)^{2^q}/θ̂_N^{2^q−1}; (v) boundary: if K/N^{α(r,q)} → c ∈ (0,∞), √N(θ^{(q)}_r − θ̂_N) →p −θ0(β_r c^r)^{2^q} for q ≥ 1 and →p β_rθ0c^r for q = 0; (vi) if K/N^{α(r,q)} → ∞ with m → ∞ then √N‖θ^{(q)}_r − θ̂_N‖ →p ∞ | proved | exact model | PD (r=2, q=1) → N (general r, q; variance; necessity) | S2–S7; T: test_math_identities; MC boundary study | – | §6, App. B | moment existence requires m/s_r > 2 (variance) |
| T3 | Inexact Newton: if the coordinator uses Ĥ with ‖Ĥ − H_N(θ̂_N)‖ = O_p(δ_N), ‖Ĥ^{-1}‖ = O_p(1), and ĝ = g_N(ϑ) + δ_g, then ‖ϑ̃ − θ̂_N‖ = O_p(‖e‖² + δ_N‖e‖ + ‖δ_g‖), e = ϑ − θ̂_N; with q chord steps ‖e_q‖ = O_p(Σ terms) and first-order equivalence iff √N(e_0 δ_N^q + e_0^{2^q} + …) → 0. Cases: (a) Ĥ = average of local Hessians at local MLEs: δ_N = m^{-1} + N^{-1/2} ⇒ α = 1 − 1/(2(r+q)); (b) single-machine Hessian at the iterate: δ_N = m^{-1/2} ⇒ α = 1 − 1/(2r+q) (recovers CEASE's (t+1)/(t+2) for r = 1 and JLY's 2/3); (c) relative quantization of score and Hessian to b bits: extra term O_p(2^{-b}‖e‖) ⇒ b ≥ (½ − r(1−α)) log₂N + ω(1) suffices when K ~ N^α, α ∈ [1 − 1/(2r), α(r,1)) | proved ((a) conditional on A4) | A1–A3 (+A4 for (a)) | L (JLY Thm 3.1, DANE Thm 2 for the factors) → N (frontier form, quantization) | T: test_quantize_relative; MC ablations (stale, single, quantized) | – | §7, App. A.3 | (a) needs the fourth-moment block condition in A4 |
| P4 | Unequal sizes: with weights m_k/N the pilot satisfies θ^{(0)} − θ̂_N = O_p(m_eff^{-r} + √K/N + N^{-1}), m_eff := (N^{-1}Σ_k m_k^{1−r})^{-1/r} ≥ m_min, and T1 holds with m replaced by m_eff; with equal weights 1/K the influence term is not preserved (difference O_p((Σ_i c_i²)^{1/2}), c_i = 1/(K m_{k(i)}) − 1/N) so q = 0 fails unless sizes are asymptotically equal, while q ≥ 1 absorbs the discrepancy. Misspecification: identical statements with Σ_ψ = sandwich | proved | A1–A3, A5 | L (Zhu–Li–Wang, Gu–Chen weights) → restated | MC skewed design | equal-weight counterexample | §8 | – |
| P5 | Cost model: T(r,q) = T_local(r,m,p) + q·T_round(K,p) + overheads; under equal α (D = 2^q r fixed) adding a round is preferable to doubling r iff T_round < Σ_{j=r}^{2r−1} T_level(j); calibrated on measured hardware | conditional (cost model) | none | PD (eqs. 47–48) → N (decision rule) | Phase 8 measurements | – | §9 | empirical, not general |
| P6 | Failure gallery (exponential): (i) Newton converges iff 0 < x < 2θ̂_N; (ii) P(J_r ∉ (0, 2θ̂_N)) > 0 for every finite m and r ≥ 2 (negative weights), so the q ≥ 1 estimator diverges with positive probability; (iii) for moderate m, J₃ has larger variance than J₂ and larger RMSE despite smaller bias; (iv) in exponential families the exact pooled sufficient statistic dominates every approximate protocol | (i),(ii),(iv) proved; (iii) numerical | exact model | PD (remarks) → N | S7; MC | – | §6.4, §10 | – |
| H1 | Adaptive choice of r from the data preserves T1 | open | – | mandate | heuristic evaluated numerically only | – | §10 (open) | no proof attempted; stated as open |