# 03 — Component-sensitive statistical provability --- # Claims 5–6 — VERIFIED (4/4) > Theorem 5 shows that under a margin condition on action-value separation, the expected regret improves to O(Bε^{β+1}) for β>0, i.e., faster than the worst-case linear-in-B rate of Theorem 4 (Theorem 5). > Theorem 6 derives a high-probability estimation-error bound of order O(L H d_D/(d_D+2) (log(n/δ)/n)^{1/(d_D+2)}) under a doubling-dimension assumption on the relevant problem domain, formalizing how statistical complexity of a biased real-world problem distribution governs sample efficiency (Theorem 6, Section 7). The point of statistical provability is distributional: performance is evaluated on a specified, possibly biased, theorem stream under a finite proof budget. Worst-case proof-search hardness is not contradicted. The analysis says which components help when the relevant state-action occupancy has exploitable geometry and score learning is accurate there. ## Margin fast rate Under a small-gap tail `nu_b(Delta <= t) <= C_Delta t^beta`, score perturbations can change the selected action only when `Delta <= 2 epsilon`. Multiplying the `O(epsilon)` loss by the `O(epsilon^beta)` probability of such near ties yields Theorem 5's `O(B epsilon^(beta+1))` expected regret. The reproduction uses a normalized gap family with CDF `t^beta`, for which the truncated expected regret is available in closed form. Across **45** combinations of `beta in {0.5,1,2}`, horizons `{1,4,16}`, and five error scales, every value lies below the theorem envelope. All **36** adjacent log-log slopes equal `beta+1` to machine precision; the observed slope range is `1.5–3.0`. ## Doubling-dimension estimation rate Theorem 6 (`thm:p1-7.3`) combines approximation error with a high-probability estimation term, hiding polylogarithms: `epsilon_est = O(L_H^(d_D/(d_D+2)) (log(n/delta)/n)^(1/(d_D+2)))`. The **75** deterministic rate certificates cross doubling dimensions `1,2,4,8,16`, Lipschitz scales `0.5,1,2`, and sample sizes from `1,000` through **10,000,000**. For every fixed geometry the bound decreases strictly with sample size. For fixed sample size, higher effective dimension slows the rate. Approximation error remains additive instead of disappearing with more labels. ## The component map - Proof shortening: reduces horizon/occupancy multiplier. - Retrieval and representation: reduce approximation error, Lipschitz constants, or effective doubling dimension. - Verifier feedback: creates bounded rollout labels and increases covered sample size. - Top-k/beam search: retains optimal actions when score error is below the action gap. - Biased workload: concentrates occupancy on a lower-complexity relevant domain. The audit records **25** one-factor interventions. Shortening the proof horizon lowers the accumulated regret multiplier. Improving approximation lowers the irreducible score envelope. Retrieval/representation can reduce effective dimension or Lipschitz scale. More verified rollout labels reduce the statistical term when coverage holds. Larger margin exponent makes harmful misranking rarer. These are component-sensitive predictions, not a claim that one component always dominates. In adversarial or off-support regimes, approximation, coverage, or margin assumptions can fail. That boundary is why the explanation applies to biased real-world problem distributions rather than all formal mathematics uniformly.