IndisputableMonolith.Physics.AnchorPolicyModel

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.RSBridge.Anchor
   4
   5/-!
   6# AnchorPolicy Model (Lean-native, computable stand-in)
   7
   8`IndisputableMonolith/Physics/AnchorPolicy.lean` intentionally treats the Standard-Model RG residue
   9`f_residue` as an **opaque interface** (axiom), because the repo does not currently implement
  10multi-loop RG kernels + threshold policy + numerical integration inside Lean.
  11
  12This file provides a **Lean-native model** of the residue whose value is *by definition* the closed
  13form display function:
  14
  15  `f_residue_model f μ := gap (ZOf f)`
  16
  17This is useful for:
  18- making downstream algebraic consequences executable / #eval-friendly,
  19- avoiding `axiom` dependencies when you explicitly want to work in the *model* where the anchor
  20  identity holds by construction.
  21
  22Important: this is **not** a proof of the SM RG statement; it is a definitional model.
  23-/
  24
  25namespace IndisputableMonolith.Physics
  26namespace AnchorPolicyModel
  27
  28open IndisputableMonolith.Constants
  29open IndisputableMonolith.RSBridge
  30
  31/-! ## Model residue -/
  32
  33/-- A computable stand-in for the RG residue: constant in scale and equal to the display `gap(Z)`.
  34
  35This encodes the single-anchor closed form as a *definition* rather than a phenomenology axiom. -/
  36noncomputable def f_residue_model (f : Fermion) (_mu : ℝ) : ℝ :=
  37  gap (ZOf f)
  38
  39@[simp] theorem f_residue_model_at (f : Fermion) (mu : ℝ) :
  40    f_residue_model f mu = gap (ZOf f) := rfl
  41
  42/-! ## Consequences (stationarity/robustness become trivial in the model) -/
  43
  44/-- In the model, the residue is constant in `t`, hence stationary at every point. -/
  45theorem stationary_at_any (muStar : ℝ) (f : Fermion) :
  46    deriv (fun t => f_residue_model f (Real.exp t)) (Real.log muStar) = 0 := by
  47  -- `f_residue_model` ignores its scale argument, so the function of `t` is constant.
  48  simp [f_residue_model]
  49
  50/-- In the model, the second derivative is also identically zero, hence bounded. -/
  51theorem stability_bound_at_any (muStar : ℝ) :
  52    ∃ (ε : ℝ), 0 < ε ∧ ∀ (f : Fermion),
  53      |deriv (deriv (fun t => f_residue_model f (Real.exp t))) (Real.log muStar)| < ε := by
  54  refine ⟨1, by norm_num, ?_⟩
  55  intro f
  56  -- Second derivative of a constant is 0.
  57  simp [f_residue_model]
  58
  59/-- Equal-Z degeneracy holds by definition in the model. -/
  60theorem equalZ_at_any {f g : Fermion} (hZ : ZOf f = ZOf g) (mu : ℝ) :
  61    f_residue_model f mu = f_residue_model g mu := by
  62  simp [f_residue_model, hZ]
  63
  64end AnchorPolicyModel
  65end IndisputableMonolith.Physics
  66