IndisputableMonolith.StandardModel.HiggsObservableSkeleton
The HiggsObservableSkeleton module supplies abstract schemas for Higgs partial widths, total widths, branching ratios and signal strengths. Physicists assembling the RS-to-EFT chain would cite these skeletons to keep kinematic and amplitude factors separate. The module consists entirely of definitions and non-negativity lemmas.
claimThe central schema is $\mathrm{partialWidth}(\mathrm{amp},\mathrm{phaseSpace})=\mathrm{phaseSpace}\cdot|\mathrm{amp}|^2$ with $\mathrm{amp}\ge0$ and $\mathrm{phaseSpace}\ge0$; analogous definitions hold for $\mathrm{totalWidth}$, $\mathrm{branchingRatio}$ and $\mathrm{signalStrength}$.
background
The module lives inside the StandardModel domain and imports the RS time quantum $\tau_0=1$ tick from Constants together with the two bridges that map RS cost geometry to the canonical Higgs EFT. HiggsEFTBridge introduces the dimensionless coordinate $\varepsilon=h/v$ that converts the RS scalar into the effective field of mass dimension one. HiggsYukawaBridge supplies the tree-level Yukawa coupling $y_f=\sqrt{2}\cdot m_f/v$.
These imports set the notational stage for the observable skeletons: amplitudes are taken as real or modulus values and phase-space factors absorb all mass dependence, exactly as required by the downstream low-energy-limit certificate.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module feeds the root IndisputableMonolith umbrella and the HiggsEFTLowEnergyLimit master certificate that bundles the five-module chain from RS cost geometry through the effective scalar coordinate to canonical Higgs EFT. It supplies the observable layer that the low-energy-limit certificate invokes when it assembles partial widths into branching ratios and signal strengths.
scope and limits
- Does not derive numerical amplitudes from the phi-ladder.
- Does not include loop corrections or higher-dimensional operators.
- Does not fix values for $m_H$ or the electroweak scale $v$.
- Does not compute decay rates outside the tree-level skeleton.
used by (2)
depends on (3)
declarations in this module (16)
-
def
partialWidth -
theorem
partialWidth_nonneg -
theorem
partialWidth_match -
def
totalWidth -
theorem
totalWidth_nonneg -
def
branchingRatio -
theorem
branchingRatio_nonneg -
def
signalStrength -
theorem
signalStrength_one_of_match -
theorem
signalStrength_zero_of_RS_zero -
theorem
tree_level_partial_width_match -
theorem
tree_level_total_width_match -
theorem
tree_level_branching_ratio_match -
structure
HiggsObservableSkeletonCert -
def
higgsObservableSkeletonCert -
theorem
higgsObservableSkeletonCert_inhabited