--- title: "Repro - Sharp Inequalities between Total Variation and Hellinger Distances for Gaussian Mixtures" emoji: 🎯 colorFrom: yellow colorTo: red sdk: static pinned: false tags: - trackio - trackio-logbook - open-experiment - icml2026-repro - paper-ihMB4kA2SQ --- # Claim-by-claim reproduction This bundle evaluates the five headline claims of *Sharp Inequalities between Total Variation and Hellinger Distances for Gaussian Mixtures*. Each claim has three materially different executable routes, including a direct route and a source-pinned universal or asymptotic certificate. The current theorem layer expands every internal paper dependency, pins every external theorem to a primary source hash, and requires zero unresolved internal nodes; a separate program independently replays the saved proof transcript. | Claim | Three-route outcome | | --- | --- | | C1 | `0/420` 1D violations; `0/14` d=2/d=3 violations; all-d certificate passes | | C2 | `0/420` 1D violations; `0/14` d=2/d=3 violations; universal pointwise reduction passes | | C3 | `11/11` explicit orders pass; independent integration and infinite-sequence certificate pass | | C4 | sample upper `n^-0.474`; Le Cam lower `n^-0.497`; 21 log-correction calibrations pass | | C5 | finite upper `H²~epsilon^1.688`; lower `H²~epsilon^1.920`; exact exponents converge to 2 | The C1/C2 doubled-grid checker agrees to `2.14e-6`, the C3 independent high-precision checker agrees to `1.759e-4`, and all intended negative controls are rejected. The source-complete replay reports `SOURCE_COMPLETE_PROOF_REPLAY_PASS`, verifies all five conclusions, and rejects five mutated proof objects: the wrong C1 exponent, a missing C2 square, coefficient `0.34` in C3, the invalid same-`delta` inversion in C4, and the weakened C5 contamination boundary. It is a machine-checked proof transcript, not a Lean/Coq formalization. ## Start here - [Claim-by-claim overview](pages/current-overview/page.md) - [Current formal proof replay](pages/current-formal-proof-replay/page.md) - [C1 — chi-square/TV theorem](pages/current-claim-c1/page.md) - [C2 — Hellinger/TV corollary](pages/current-claim-c2/page.md) - [C3 — sharp Chebyshev construction](pages/current-claim-c3/page.md) - [C4 — minimax TV characterization](pages/current-claim-c4/page.md) - [C5 — robust Hellinger upper/lower rates](pages/current-claim-c5/page.md) - [Exact methods, command, environment, and compute](pages/current-methods/page.md) - [Source-complete proof transcript](evidence/raw/source_complete_proof_replay/proof_transcript.md) - [Independent source-complete replay](evidence/raw/source_complete_proof_replay/independent_checker.json) ## Reproduce The command is fixed across the experiment tree: ```bash uv sync --frozen && uv run python repro/src/run_publication_gate.py ``` Python `3.12`; exact dependencies are pinned in [`pyproject.toml`](evidence/src/pyproject.toml) and [`uv.lock`](evidence/src/uv.lock). Every scientific gate and negative control is fail-closed: a mismatch exits nonzero. Download the [three-route result](evidence/raw/three_route/result.json), [route matrix](evidence/raw/three_route/route_matrix.json), [d=2/d=3 raw cells](evidence/raw/three_route/multidimensional_direct.csv), [complete scaled result](evidence/raw/scaled_direct/result.json), [raw CSVs](evidence/raw/scaled_direct/claim_1_2_raw.csv), [independent checker](evidence/raw/scaled_direct/independent_checker.json), and [negative controls](evidence/raw/scaled_direct/negative_control.json). The [source-complete proof generator](evidence/src/repro/src/verify_source_complete_proof_replay.py), [independent replay source](evidence/src/repro/src/check_source_complete_proof_replay.py), [visibility matrix](pages/current-visibility/page.md) and [release audit](pages/current-release-audit/page.md) remain directly reachable. The immutable [Historical rejected baseline](pages/historical-rejected-baseline/page.md) is preserved additively and is not the current verification.