IndisputableMonolith.StandardModel.HiggsObservableSkeleton
The module encodes an abstract schema for Higgs partial widths as phaseSpace times the squared amplitude, with non-negativity enforced for physical channels. It supplies the observable layer that closes the RS cost geometry to canonical Higgs EFT chain. Collider physicists building low-energy SM predictions from the forcing chain would cite these definitions. The module consists of definitions plus elementary non-negativity and matching lemmas.
claimThe partial width into a channel is given by $w = s |a|^2$, where $a$ is the tree amplitude and $s$ the kinematic phase-space factor (with $m_H$ and final-state masses absorbed), both required non-negative.
background
The module operates inside the Standard Model section of the Recognition Science framework. It rests on the Higgs EFT Bridge, which maps the dimensionless RS coordinate ε = h/v to the canonical Higgs EFT, and the Higgs Yukawa Bridge, which writes fermion couplings as y_f = √2 m_f / v. Constants supplies the base time quantum τ₀ = 1 tick. The local setting is the final step that converts the effective scalar coordinate into collider observables.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the observable layer that completes the RS-to-SM chain inside the Higgs EFT Low Energy Limit master certificate. It is imported by the root IndisputableMonolith module and by HiggsEFTLowEnergyLimit, which bundles the five-module sequence that formalises the path from RS cost geometry through the effective scalar coordinate to canonical Higgs EFT and its low-energy consequences.
scope and limits
- Does not derive amplitudes from the phi-ladder or J-cost geometry.
- Does not include loop corrections or higher-order EFT operators.
- Does not assign numerical values to masses or couplings.
- Does not treat production cross sections or initial-state kinematics.
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