Bounds in ℝ≥0

[MarcIlunga]

Bottom of the proof-technique stack (see the list below). Closes #16.

Security bounds are stated in ℝ≥0 and read in ℝ≥0∞ through the coercion, which is additive and order-preserving, instead of through ENNReal.ofReal, which clamps negatives and is additive only on non-negative arguments.

• ofReal stays only where the distances are defined from real probabilities (transcriptDistance, the advantages, advantageDistance) and in two bridging lemmas:
  • RandomSystem.transcriptDistance_le: a bound on the transcript laws under every environment bounds the transcript distance;
  • RandomSystem.transcriptDistance_le_of_advantage_le: a bound on every advantage does.
• Restated with ε : ℝ≥0: transcriptDistance_visible_le_of_unsetProbability, dist_visible_le, game_dist_le, game_dist_ofSingleFunction_le, and the authenticated-encryption bounds, now ≤ (q_e² / |M| : ℝ≥0).
• AGENTS.md records the convention.

Every later PR in the stack states its bounds this way.

Checks: build with --wfail, source check, whole-library axiom audit (10,363 declarations), Mathlib linter set on the changed files (two pre-existing open Classical lines in files this PR touches are left for the linter cleanup), THEORY.md anchors and 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) ← this PR
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)
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