IndisputableMonolith.StandardModel.HiggsObservableSkeleton

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.StandardModel.HiggsEFTBridge
   4import IndisputableMonolith.StandardModel.HiggsYukawaBridge
   5
   6/-!
   7# Higgs Observable Skeleton
   8
   9This module formalises the *target* surface of Higgs collider observables —
  10partial widths, branching ratios, and signal-strength modifiers — as
  11abstract structural objects parametrised by amplitudes and phase-space
  12factors.
  13
  14The point of the module is **not** to compute the SM partial widths from
  15scratch.  It is to expose, in a Lean-checkable form, what it would mean
  16for the RS theory to "match the SM Higgs phenomenology".  Concretely:
  17
  18* If the RS-derived Higgs mass equals the SM value,
  19* If the RS-derived Yukawa coupling for a fermion equals the SM Yukawa,
  20* If the RS-derived gauge coupling equals the SM gauge coupling,
  21
  22then the *tree-level* partial width into that channel, computed from the
  23same amplitude formula in both theories, must be numerically identical.
  24That is the precise content of "RS reproduces SM observables" at tree
  25level.
  26
  27Loop-level corrections (e.g. h → γγ, h → gg) require explicit RS-derived
  28loop amplitudes; those are *not* yet in Lean and are tagged `LOOP_LEVEL_OPEN`.
  29
  30## Status
  31
  32* `THEOREM`: structural identities for total width, branching ratios,
  33  signal strength.
  34* `CONDITIONAL_THEOREM`: tree-level matching of an RS partial width to the
  35  SM partial width when the input couplings agree.
  36* `OPEN`: loop-level partial widths for `h → γγ`, `h → Zγ`, `h → gg`.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace StandardModel
  41namespace HiggsObservableSkeleton
  42
  43open Real
  44open Constants
  45
  46noncomputable section
  47
  48/-! ## §1. Partial Width Schema -/
  49
  50/-- Abstract schema for a Higgs partial width into a channel.
  51
  52    `partialWidth amp phaseSpace = phaseSpace * |amp|²`.
  53
  54    Here `amp` is the (real or modulus) tree amplitude into the channel
  55    and `phaseSpace` is the kinematic factor (with the `m_H` and final-state
  56    masses absorbed into it).  Both must be non-negative for a physical
  57    channel. -/
  58def partialWidth (amp phaseSpace : ℝ) : ℝ := phaseSpace * amp ^ 2
  59
  60/-- Partial widths are non-negative for non-negative phase space. -/
  61theorem partialWidth_nonneg (amp phaseSpace : ℝ) (hps : 0 ≤ phaseSpace) :
  62    0 ≤ partialWidth amp phaseSpace := by
  63  unfold partialWidth
  64  have hamp2 : 0 ≤ amp ^ 2 := sq_nonneg _
  65  exact mul_nonneg hps hamp2
  66
  67/-- Two partial widths matched when both amplitudes and phase-space factors
  68    agree. -/
  69theorem partialWidth_match
  70    (amp1 amp2 phaseSpace1 phaseSpace2 : ℝ)
  71    (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2) :
  72    partialWidth amp1 phaseSpace1 = partialWidth amp2 phaseSpace2 := by
  73  rw [hamp, hps]
  74
  75/-! ## §2. Total Width and Branching Ratios -/
  76
  77/-- The total Higgs width is the sum of partial widths over all channels.
  78    We model "all channels" as a finite list of `(amp, phaseSpace)` pairs. -/
  79def totalWidth (channels : List (ℝ × ℝ)) : ℝ :=
  80  (channels.map (fun p => partialWidth p.fst p.snd)).sum
  81
  82/-- The total width is non-negative when each channel's phase space is. -/
  83theorem totalWidth_nonneg (channels : List (ℝ × ℝ))
  84    (hps : ∀ p ∈ channels, 0 ≤ p.snd) :
  85    0 ≤ totalWidth channels := by
  86  unfold totalWidth
  87  induction channels with
  88  | nil => simp
  89  | cons head tail ih =>
  90      simp only [List.map_cons, List.sum_cons]
  91      have hhead_mem : head ∈ head :: tail := by simp
  92      have hhead : 0 ≤ partialWidth head.fst head.snd :=
  93        partialWidth_nonneg head.fst head.snd (hps head hhead_mem)
  94      have htail : 0 ≤ (tail.map (fun p => partialWidth p.fst p.snd)).sum := by
  95        apply ih
  96        intro p hp
  97        exact hps p (by simp [hp])
  98      linarith
  99
 100/-- The branching ratio of a single channel is its partial width over the
 101    total width.  Defined to be zero if the total width is zero (a
 102    degenerate, unphysical case). -/
 103def branchingRatio (amp phaseSpace : ℝ) (channels : List (ℝ × ℝ)) : ℝ :=
 104  if totalWidth channels = 0 then 0
 105  else partialWidth amp phaseSpace / totalWidth channels
 106
 107/-- Branching ratios are non-negative when phase spaces are. -/
 108theorem branchingRatio_nonneg
 109    (amp phaseSpace : ℝ) (channels : List (ℝ × ℝ))
 110    (hps_amp : 0 ≤ phaseSpace)
 111    (hps : ∀ p ∈ channels, 0 ≤ p.snd) :
 112    0 ≤ branchingRatio amp phaseSpace channels := by
 113  unfold branchingRatio
 114  by_cases h : totalWidth channels = 0
 115  · simp [h]
 116  · simp [h]
 117    have hpw : 0 ≤ partialWidth amp phaseSpace := partialWidth_nonneg amp phaseSpace hps_amp
 118    have htot : 0 ≤ totalWidth channels := totalWidth_nonneg channels hps
 119    exact div_nonneg hpw htot
 120
 121/-! ## §3. Signal-Strength Modifier -/
 122
 123/-- The signal strength `μ_i = (σ · BR)_RS / (σ · BR)_SM` for a channel.
 124
 125    By construction, `μ = 1` when both the cross-section and the branching
 126    ratio match the SM. -/
 127def signalStrength (sigma_BR_RS sigma_BR_SM : ℝ) : ℝ :=
 128  if sigma_BR_SM = 0 then 0 else sigma_BR_RS / sigma_BR_SM
 129
 130/-- The signal-strength modifier equals 1 when both numerator and
 131    denominator agree. -/
 132theorem signalStrength_one_of_match
 133    (x : ℝ) (hx : x ≠ 0) :
 134    signalStrength x x = 1 := by
 135  unfold signalStrength
 136  simp [hx]
 137
 138/-- Signal strength of zero RS rate is zero. -/
 139theorem signalStrength_zero_of_RS_zero
 140    (y : ℝ) (hy : y ≠ 0) :
 141    signalStrength 0 y = 0 := by
 142  unfold signalStrength
 143  simp [hy]
 144
 145/-! ## §4. Tree-Level Matching Theorem -/
 146
 147/-- The decisive structural matching theorem: if the RS amplitude and
 148    phase space for a channel equal their SM counterparts, then the RS
 149    partial width equals the SM partial width.
 150
 151    The hypothesis is exactly the content of "RS reproduces the SM tree
 152    amplitude in this channel."  In practice this hypothesis is satisfied
 153    once the canonical-normalisation map of `HiggsEFTBridge` and the
 154    Yukawa map of `HiggsYukawaBridge` are closed for the channel of
 155    interest. -/
 156theorem tree_level_partial_width_match
 157    (amp_RS amp_SM phaseSpace_RS phaseSpace_SM : ℝ)
 158    (hamp : amp_RS = amp_SM)
 159    (hps : phaseSpace_RS = phaseSpace_SM) :
 160    partialWidth amp_RS phaseSpace_RS = partialWidth amp_SM phaseSpace_SM :=
 161  partialWidth_match amp_RS amp_SM phaseSpace_RS phaseSpace_SM hamp hps
 162
 163/-- If every channel's RS amplitude and phase space match the SM
 164    counterparts, then the total widths are equal channel by channel and
 165    therefore equal in sum. -/
 166theorem tree_level_total_width_match
 167    (rsChannels smChannels : List (ℝ × ℝ))
 168    (h : rsChannels = smChannels) :
 169    totalWidth rsChannels = totalWidth smChannels := by
 170  rw [h]
 171
 172/-- Branching ratios match channel-wise when the underlying channel
 173    structures match. -/
 174theorem tree_level_branching_ratio_match
 175    (amp1 phaseSpace1 amp2 phaseSpace2 : ℝ)
 176    (rsChannels smChannels : List (ℝ × ℝ))
 177    (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2)
 178    (hch : rsChannels = smChannels) :
 179    branchingRatio amp1 phaseSpace1 rsChannels
 180      = branchingRatio amp2 phaseSpace2 smChannels := by
 181  rw [hamp, hps, hch]
 182
 183/-! ## §5. Master Skeleton Certificate -/
 184
 185/-- Master certificate for the Higgs observable skeleton.
 186
 187    Tags:
 188    - `THEOREM`: structural identities for partial widths, total widths,
 189      branching ratios, and signal strengths.
 190    - `TREE_LEVEL_CONDITIONAL`: the matching theorems are conditional on
 191      the underlying amplitude/phase-space agreement between RS and SM.
 192    - `LOOP_LEVEL_OPEN`: loop-induced channels (`h → γγ`, `h → Zγ`,
 193      `h → gg`) are not formalised here. -/
 194structure HiggsObservableSkeletonCert where
 195  /-- THEOREM: partial widths are non-negative on physical phase space. -/
 196  pw_nonneg     : ∀ amp ps, 0 ≤ ps → 0 ≤ partialWidth amp ps
 197  /-- THEOREM: total widths are non-negative. -/
 198  tw_nonneg     : ∀ channels, (∀ p ∈ channels, 0 ≤ p.snd) →
 199                   0 ≤ totalWidth channels
 200  /-- THEOREM: branching ratios are non-negative. -/
 201  br_nonneg     : ∀ amp ps channels, 0 ≤ ps →
 202                   (∀ p ∈ channels, 0 ≤ p.snd) →
 203                   0 ≤ branchingRatio amp ps channels
 204  /-- THEOREM: signal strength equals one when RS and SM rates match. -/
 205  signal_unity  : ∀ x : ℝ, x ≠ 0 → signalStrength x x = 1
 206  /-- TREE_LEVEL_CONDITIONAL: partial-width match from amplitude and
 207      phase-space match. -/
 208  tree_pw_match : ∀ a1 a2 p1 p2 : ℝ, a1 = a2 → p1 = p2 →
 209                   partialWidth a1 p1 = partialWidth a2 p2
 210  /-- TREE_LEVEL_CONDITIONAL: branching-ratio match from channel-wise match. -/
 211  tree_br_match : ∀ a1 p1 a2 p2 c_rs c_sm,
 212                   a1 = a2 → p1 = p2 → c_rs = c_sm →
 213                   branchingRatio a1 p1 c_rs = branchingRatio a2 p2 c_sm
 214
 215def higgsObservableSkeletonCert : HiggsObservableSkeletonCert where
 216  pw_nonneg     := partialWidth_nonneg
 217  tw_nonneg     := totalWidth_nonneg
 218  br_nonneg     := branchingRatio_nonneg
 219  signal_unity  := signalStrength_one_of_match
 220  tree_pw_match := partialWidth_match
 221  tree_br_match := tree_level_branching_ratio_match
 222
 223theorem higgsObservableSkeletonCert_inhabited : Nonempty HiggsObservableSkeletonCert :=
 224  ⟨higgsObservableSkeletonCert⟩
 225
 226end
 227
 228end HiggsObservableSkeleton
 229end StandardModel
 230end IndisputableMonolith
 231