IndisputableMonolith.Verification.NeutrinoReferenceIndexCheck

   1import Mathlib
   2
   3/-!
   4# Neutrino Reference Index: arithmetic check
   5
   6This file mechanically checks the arithmetic shown in the screenshot (Eq. (3.25) of
   7`2601.12194v1.pdf`):
   8
   9`n_ν = 7 * (1 / X_opt) * R_RS = 7 * (1 / 0.515) * 0.583 ≈ 85.5`.
  10
  11Lean reduces the numeric expression **exactly** to a rational number, showing it is
  12approximately `7.924...`, not `85.5`.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Verification
  17namespace NeutrinoReferenceIndexCheck
  18
  19theorem nν_value :
  20    (7 : ℝ) * (1 / (0.515 : ℝ)) * (0.583 : ℝ) = (4081 : ℝ) / 515 := by
  21  norm_num
  22
  23theorem nν_bounds :
  24    (7.92 : ℝ) < (7 : ℝ) * (1 / (0.515 : ℝ)) * (0.583 : ℝ) ∧
  25      (7 : ℝ) * (1 / (0.515 : ℝ)) * (0.583 : ℝ) < 7.93 := by
  26  -- All numerals here are rational; `norm_num` discharges the bounds mechanically.
  27  norm_num
  28
  29theorem nν_ne_85_5 :
  30    (7 : ℝ) * (1 / (0.515 : ℝ)) * (0.583 : ℝ) ≠ (85.5 : ℝ) := by
  31  -- Reduce to rationals; the numbers are far apart.
  32  norm_num
  33
  34end NeutrinoReferenceIndexCheck
  35end Verification
  36end IndisputableMonolith
  37