IndisputableMonolith.Physics.RGTransportCertificate

   1import Mathlib
   2import IndisputableMonolith.RSBridge.Anchor
   3
   4namespace IndisputableMonolith
   5namespace Physics
   6namespace RGTransportCertificate
   7
   8open RSBridge
   9
  10/-- Certified SM RG transport exponent f^RG_i(μ*, μ_end) from canonical policy. -/
  11def f_RG_certified : Fermion → ℚ
  12  | .e   => 494/10000
  13  | .mu  => 288/10000
  14  | .tau => 179/10000
  15  | .u   => 4822/10000
  16  | .d   => 4764/10000
  17  | .s   => 4764/10000
  18  | .c   => 5470/10000
  19  | .b   => 3807/10000
  20  | .t   => 98/10000
  21  | _    => 0
  22
  23/-!
  24NOTE (policy seam):
  25
  26These values are an **external certificate** produced under a declared RG transport policy
  27(loop order, thresholds, scheme, integrator). They are not “fit parameters” of the RS model
  28layer, but they *are* conventions that must be declared whenever used for PDG comparisons.
  29
  30Source-of-truth for the policy snapshot and floating values:
  31- `data/certificates/rg_transport/canonical_2025_q4.json`
  32- `tools/rg_transport_policy.json` + `tools/rg_transport_certify.py`
  33-/
  34
  35/-- Tolerance for the certified transport exponents. -/
  36def f_RG_tolerance : ℚ := 1/10000
  37
  38/-- Hypothesis that the true f^RG lies within the certified range. -/
  39def is_certified (f : Fermion) (val : ℝ) : Prop :=
  40  (f_RG_certified f : ℝ) - (f_RG_tolerance : ℝ) ≤ val ∧
  41  val ≤ (f_RG_certified f : ℝ) + (f_RG_tolerance : ℝ)
  42
  43/-- Lower endpoint of the certified enclosure interval. -/
  44def f_RG_lower (f : Fermion) : ℚ := f_RG_certified f - f_RG_tolerance
  45
  46/-- Upper endpoint of the certified enclosure interval. -/
  47def f_RG_upper (f : Fermion) : ℚ := f_RG_certified f + f_RG_tolerance
  48
  49theorem f_RG_tolerance_nonneg : (0 : ℚ) ≤ f_RG_tolerance := by
  50  norm_num [f_RG_tolerance]
  51
  52theorem f_RG_interval_nonempty (f : Fermion) : f_RG_lower f ≤ f_RG_upper f := by
  53  unfold f_RG_lower f_RG_upper
  54  nlinarith [f_RG_tolerance_nonneg]
  55
  56/-- Equivalent absolute-error enclosure form for certified transport values. -/
  57theorem is_certified_iff_abs_error_le (f : Fermion) (val : ℝ) :
  58    is_certified f val ↔
  59      |val - (f_RG_certified f : ℝ)| ≤ (f_RG_tolerance : ℝ) := by
  60  constructor
  61  · intro h
  62    rcases h with ⟨hlo, hhi⟩
  63    have h1 : -((f_RG_tolerance : ℚ) : ℝ) ≤ val - (f_RG_certified f : ℚ) := by
  64      linarith
  65    have h2 : val - (f_RG_certified f : ℚ) ≤ ((f_RG_tolerance : ℚ) : ℝ) := by
  66      linarith
  67    exact abs_le.mpr ⟨h1, h2⟩
  68  · intro h
  69    have h' := abs_le.mp h
  70    constructor <;> linarith [h'.1, h'.2]
  71
  72/-- The certified center value is enclosed for every fermion. -/
  73theorem certified_center_enclosed (f : Fermion) :
  74    is_certified f (f_RG_certified f) := by
  75  unfold is_certified
  76  have htol_nonneg : (0 : ℝ) ≤ (f_RG_tolerance : ℝ) := by
  77    exact_mod_cast f_RG_tolerance_nonneg
  78  constructor
  79  · exact sub_le_self _ htol_nonneg
  80  · exact le_add_of_nonneg_right htol_nonneg
  81
  82end RGTransportCertificate
  83end Physics
  84end IndisputableMonolith
  85