Pith. sign in
module module high

IndisputableMonolith.StandardModel.HiggsObservableSkeleton

show as:
view Lean formalization →

Abstract schema for Higgs decay observables: partial width equals phase-space times squared tree amplitude, then total width, branching ratios, and signal strengths. Non-negativity and RS–SM matching lemmas sit beside the definitions. The low-energy Higgs EFT master certificate imports this layer. Structure is definitional with elementary algebraic identities, not deep analysis.

claimFor a Higgs channel with tree amplitude modulus $|A|$ and kinematic factor $\Phi\ge 0$, the partial width is $\Gamma=\Phi\,|A|^2$. Total width is $\Gamma_{\mathrm{tot}}=\sum\Gamma_i$; branching ratio $\mathrm{BR}_i=\Gamma_i/\Gamma_{\mathrm{tot}}$ (when $\Gamma_{\mathrm{tot}}>0$); signal strength $\mu$ compares RS and SM rates. Matching lemmas assert $\Gamma^{\mathrm{RS}}=\Gamma^{\mathrm{SM}}$ (and $\mu=1$) when amplitudes and phase space agree; $\mu=0$ if the RS amplitude vanishes.

background

Recognition Science links cost geometry to a canonical Higgs EFT through an effective scalar coordinate $\varepsilon=h/v$, with $h$ the collider-normalized field and $v>0$ the electroweak scale (HiggsEFTBridge). Fermion Yukawas enter as $y_f=\sqrt{2},m_f/v$ from RS-derived masses over $v$ (HiggsYukawaBridge).

Collider observables need widths and rates, not only the Lagrangian. This module supplies the standard kinematic skeleton: a partial width is phase space times squared tree amplitude, with both factors required non-negative for a physical channel. Masses of the Higgs and final states are absorbed into the phase-space factor.

Constants (including the RS tick) are imported only as ambient infrastructure. No new forcing-chain step is proved here; the layer is the observable interface between the EFT/Yukawa bridges and low-energy certificates.

proof idea

Definition module plus elementary lemmas. partialWidth is the product $\Phi,|A|^2$; non-negativity follows from non-negative factors. Total width sums partial widths; branching ratios are normalized partial widths. Signal-strength lemmas are one-line algebraic consequences: identical RS and SM inputs give $\mu=1$; vanishing RS amplitude gives $\mu=0$. Tree-level match lemmas restate equality of partial and total widths under amplitude and phase-space agreement. No analytic continuation, loop integrals, or PDF convolution.

why it matters in Recognition Science

Feeds HiggsEFTLowEnergyLimit, the master certificate that bundles the chain Anil requested: RS cost geometry → effective scalar coordinate → canonical Higgs EFT, then through Yukawa and observable layers to low-energy limits. Without a shared width/BR/$\mu$ schema, EFT matching cannot be stated as equal collider rates.

Sits downstream of HiggsEFTBridge and HiggsYukawaBridge: those modules supply the field coordinate and $y_f$; this module turns amplitudes into $\Gamma$, BR, and $\mu$. It does not itself derive $m_H$, $\alpha$, or rung masses from T5–T8; it only packages how tree amplitudes become observables once those inputs exist.

Closes a scaffolding gap between Lagrangian-level bridges and certificate-level equality of RS versus SM signals.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)