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

Reproduce

The command is fixed across the experiment tree:

uv sync --frozen && uv run python repro/src/run_publication_gate.py

Python 3.12; exact dependencies are pinned in pyproject.toml and uv.lock. Every scientific gate and negative control is fail-closed: a mismatch exits nonzero.

Download the three-route result, route matrix, d=2/d=3 raw cells, complete scaled result, raw CSVs, independent checker, and negative controls. The source-complete proof generator, independent replay source, visibility matrix and release audit remain directly reachable.

The immutable Historical rejected baseline is preserved additively and is not the current verification.