| 1 |
Delete out/results.json and out/counterexample.csv, re-run analysis.py; results.json byte-identical, counterexample.csv same SHA-256 |
PASS |
| 2 |
rows of counterexample.csv = counterexample_values.n = n_analysed = design n (100000); columns x,y |
PASS |
| 3 |
Recomputing means/sds (ddof=1) and KS from counterexample.csv reproduces results.json (diffs <= 2e-18) |
PASS |
| 4 |
Seed in results = design seed 20261029 |
PASS |
| 5 |
|
y |
| 6 |
Share of x+y exactly 0 = 0.50047 (theory 0.5) |
PASS |
| 7 |
sd_sum = 1.4059 vs theoretical sqrt(2)=1.4142; sd_x, sd_y ≈ 1; means ≈ 0 |
PASS (within sampling error, se of sd ≈ 0.003-0.005) |
| 8 |
KS(x+y) = 0.2508 >= theoretical lower bound 0.25 (atom of mass ~1/2 forces sup-gap >= half the jump against any continuous CDF) |
PASS |
| 9 |
Marginal KS (x: 0.0021, y: 0.0020) and independent-sum baseline KS (0.0018) are of order 1/sqrt(n) ≈ 0.003, i.e. ~100x smaller than counterexample KS |
PASS |
| 10 |
Sum is non-degenerate (sd_sum > 0) so the "constant counts as normal" clause does not rescue A |
PASS |
| 11 |
Verdicts hard-coded from proofs in argument.md, not derived from simulation |
PASS |