HiggsObservableSkeletonCert
plain-language theorem explainer
HiggsObservableSkeletonCert packages non-negativity of partial and total widths, branching ratios, signal-strength unity under matching inputs, and tree-level equality conditions into one auditable structure for Higgs observables. Collider model builders would cite it to confirm that RS-derived amplitudes reproduce SM tree-level phenomenology when masses and couplings agree. The structure is assembled by direct field assignment from the module's non-negativity and matching lemmas.
Claim. A structure asserting: for amplitude $a$ and phase space $ps$ with $ps ≥ 0$, partial width $Γ(a,ps) ≥ 0$; for non-negative channel weights, total width $Γ_{tot} ≥ 0$; branching ratio $BR ≥ 0$; signal strength $μ(x,x) = 1$ whenever $x ≠ 0$; and conditional equality $Γ(a_1,p_1) = Γ(a_2,p_2)$ and $BR(a_1,p_1,c_{rs}) = BR(a_2,p_2,c_{sm})$ when the respective amplitudes, phase spaces, and channel lists agree.
background
The module treats partial width as the decay rate into one channel computed from an amplitude and a phase-space factor, total width as the sum over channels, and branching ratio as their ratio. Signal strength is the ratio of RS to SM rates. These objects are kept abstract so that agreement of RS mass, Yukawa, and gauge couplings with SM values forces tree-level observable agreement. The setting is therefore the target surface of collider phenomenology rather than a first-principles computation of SM widths.
proof idea
The declaration is a structure definition. Each field is populated by a direct reference to a sibling lemma: pw_nonneg from partialWidth_nonneg, tw_nonneg from totalWidth_nonneg, br_nonneg from branchingRatio_nonneg, signal_unity from signalStrength_one_of_match, tree_pw_match from partialWidth_match, and tree_br_match from the corresponding branching-ratio match lemma.
why it matters
The certificate supplies the observable-level interface required by HiggsEFTLowEnergyLimitCert and by the inhabited-instance theorem in the same module. It records the precise content of tree-level RS-SM matching for the Higgs sector, as stated in the module documentation. Loop-induced channels remain tagged LOOP_LEVEL_OPEN and are excluded from the present structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.