The H-coefficient bound for random systems

[MarcIlunga]

Proof-technique stack, layer 2 (systems level). Based on the couplings PR, though independent of it. Closes #19.

RandomSystem.transcriptDistance_le_add_of_ratio_on_good, in the new RandomSystems/Distance/HCoefficient.lean. For random systems R (real) and S (ideal) replying at the queried label:

• if (1 - ε₁) · S(h) ≤ R(h) on every transcript outside Bad,
• and Bad has probability at most ε₂ in the transcript law of S under every compatible query-bounded environment,
• then Δ(R, S) ≤ ε₁ + ε₂, with ε₁ ε₂ : ℝ≥0.

A transcript law restricts the system's probability to the transcripts the environment produces, and the restriction is the same for both systems. So the ratio carries over to the transcript laws, and the distribution-level bound statDist_le_probBad_add_of_ratio_on_good (Patarin's H-coefficient technique) applies under each environment. The statement is the case of #20 with nothing revealed and two classes. The original HCTR2 proof (ePrint 2021/1441, §3.3) uses this form.

Checks: build with --wfail, axiom audit, linter set, anchors, math rendering.

The stack

Proof techniques for the HCTR2 port, one technique per PR, ordered by abstraction (merge bottom-up):

1. Bounds in ℝ≥0 #25 Bounds in ℝ≥0 (convention)
2. Couplings of random systems #26 Couplings of random systems (systems)
3. The H-coefficient bound for random systems #27 The H-coefficient bound for random systems (systems) ← this PR
4. Games equivalent as games and the fundamental lemma #28 Games equivalent as games and the fundamental lemma (games)
5. Identical until bad: a common part, per-step costs, and coupled games #29 Identical until bad (games)

🤖 Generated with Claude Code

https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9