IndisputableMonolith.Verification.CPMBridge.Constants.Probability

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5namespace CPMBridge
   6namespace Constants
   7
   8/-- Probability that `n_domains` independent selections from a range of size `range_size`
   9    all land within a window of radius `tolerance`. -/
  10noncomputable def coincidenceProbability (n_domains : ℕ)
  11    (range_size : ℝ) (tolerance : ℝ) : ℝ :=
  12  (tolerance / range_size) ^ n_domains
  13
  14lemma coincidenceProbability_net_radius :
  15    coincidenceProbability 4 1 0.04 = (0.04 : ℝ) ^ 4 := by
  16  simp [coincidenceProbability]
  17
  18lemma net_radius_probability_small :
  19    coincidenceProbability 4 1 0.04 < (1 : ℝ) / 100000 := by
  20  -- (0.04)^4 = 1 / 390625 < 1 / 100000
  21  have hcalc : coincidenceProbability 4 1 0.04 = (1 : ℝ) / 390625 := by
  22    norm_num [coincidenceProbability]
  23  have : (1 : ℝ) / 390625 < 1 / 100000 := by
  24    norm_num
  25  simpa [hcalc] using this
  26
  27/-- Conservative combined coincidence probability using auxiliary bounds for
  28    projection constants and dyadic schedules. -/
  29lemma combined_probability_small :
  30    let pNet := coincidenceProbability 4 1 0.04
  31    let pProj : ℝ := 1 / 100
  32    let pDyadic : ℝ := 1 / 1000
  33    pNet * pProj * pDyadic < (1 : ℝ) / 1000000000 := by
  34  intro pNet pProj pDyadic
  35  have : (0.04 : ℝ) ^ 4 / 100 / 1000 < (1 : ℝ) / 1000000000 := by
  36    norm_num
  37  simpa [pNet, pProj, pDyadic, coincidenceProbability] using this
  38
  39end Constants
  40end CPMBridge
  41end Verification
  42end IndisputableMonolith
  43