ihMB4kA2SQ / README.md
DineshAI's picture
Add source-complete theorem proof replay
5cd7fd3 verified
|
Raw
History Blame Contribute Delete
4.02 kB
---
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.