feat(LatticeCrypto): discrete Gaussian mass bounds (mode, sum, guessing probability)

[alik-eth]

Quantitative pointwise-mass theory for the 1-D discrete Gaussian, closing the gap noted in the Falcon min-entropy discussion on #466 (self-contained off main; no Falcon/GPV imports).

What this adds (all in LatticeCrypto/DiscreteGaussian.lean, +251 lines)

• Mode-mass bound: discreteGaussianWeight σ μ z ≤ discreteGaussianWeight σ μ (round μ) (the weight is maximized at the rounding of the center — no positivity hypothesis needed), hence discreteGaussianPMF σ μ z ≤ weight(round μ) / discreteGaussianSum σ μ.
• Quantitative sum lower bound: σ·√(2π) − 1 ≤ discreteGaussianSum σ μ — the full constant, via two new reusable infinite-tail comparison lemmas (integral_Ioi_le_tsum_of_antitoneOn, integral_Iic_le_tsum_of_monotoneOn — Mathlib currently has only the finite-interval SumIntegralComparisons; these take limits along intervalIntegral_tendsto_integral_Ioi/Iic), splitting at ⌊μ⌋ with the middle unit interval charged ≤ 1.
• Guessing-probability bound: for 1 < σ·√(2π), discreteGaussianDist σ μ hσ z ≤ ENNReal.ofReal (1 / (σ·√(2π) − 1)) — the per-sample min-entropy bound (2^(−H∞) form) that a coset-Gaussian trapdoor sampler's guessing probability ultimately reduces to. The 2n-dimensional NTRU coset lift (GPV08 Lemma 2.10) remains future work; this is its 1-D building block.

Verification

All 8 new declarations #print axioms at exactly [propext, Classical.choice, Quot.sound]; zero sorries; file clean under the CI linter set; lake build LatticeCrypto HashSig Examples green.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

This PR adds a formalization of quantitative pointwise mass bounds for the 1-D discrete Gaussian distribution, providing mode-mass, sum, and guessing probability bounds without any sorries or admits. The core changes are concentrated in LatticeCrypto/DiscreteGaussian.lean (+251 lines). It is self-contained and closes a gap noted in an earlier Falcon min-entropy discussion. The work supports future coset-Gaussian trapdoor sampler analysis (e.g., GPV08 Lemma 2.10) by providing the 1-D building block for GuessingProbability and min-entropy conditions. No protocols, infrastructure, or documentation changes are included.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	251
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 8 declaration(s)

LatticeCrypto/DiscreteGaussian.lean (8)

• theorem discreteGaussianDist_apply_le (σ μ : ℝ) (hσ : 0 < σ)
• theorem discreteGaussianPMF_le_one_div_sub_one (σ μ : ℝ) (hσ : 0 < σ)
• theorem discreteGaussianPMF_le_weight_round_div_sum (σ μ : ℝ) (hσ : 0 < σ) (z : ℤ) :
• theorem discreteGaussianWeight_le_one (σ μ : ℝ) (z : ℤ) :
• theorem discreteGaussianWeight_le_weight_round (σ μ : ℝ) (z : ℤ) :
• theorem integral_Iic_le_tsum_of_monotoneOn {f : ℝ → ℝ} {c : ℝ}
• theorem integral_Ioi_le_tsum_of_antitoneOn {f : ℝ → ℝ} {c : ℝ}
• theorem le_discreteGaussianSum (σ μ : ℝ) (hσ : 0 < σ) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a substantial extension to LatticeCrypto/DiscreteGaussian.lean, adding pointwise mass bounds, sum–integral comparison lemmas, a quantitative lower bound for the normalizing constant, and a guessing-probability bound. The diff generally follows the project's guidelines, but several violations and concerns are noted below.

---

📄 **Per-File Summaries**

• LatticeCrypto/DiscreteGaussian.lean: This diff introduces three major additions to DiscreteGaussian.lean. First, it adds two import lines (Mathlib.Analysis.SumIntegralComparisons and Mathlib.MeasureTheory.Integral.IntegralEqImproper). Second, it defines three new theorems—discreteGaussianWeight_le_one, discreteGaussianWeight_le_weight_round, and discreteGaussianPMF_le_weight_round_div_sum—that provide pointwise mass bounds for the discrete Gaussian weight and PMF, culminating in the result that every point mass is at most the mass at round μ. Third, the diff adds a SumIntegralComparison section containing two new general lemmas (integral_Ioi_le_tsum_of_antitoneOn and integral_Iic_le_tsum_of_monotoneOn) that bound improper integrals by sums over unit-spaced grids, which are then used in the new LowerBound section to prove le_discreteGaussianSum, a quantitative lower bound σ√(2π) - 1 ≤ discreteGaussianSum σ μ. Finally, the Guessing-Probability-Bound section adds two theorems (discreteGaussianPMF_le_one_div_sub_one and discreteGaussianDist_apply_le) that combine the mode-mass bound with the normalizing-constant lower bound to obtain a concrete per-point guessing bound for the one-dimensional discrete Gaussian, expressed in both ℝ and ENNReal forms. No sorry or admit appear in the added code.

---

Last updated: 2026-07-13 16:01 UTC.