higgsObservableSkeletonCert
plain-language theorem explainer
The declaration constructs the master certificate for the Higgs observable skeleton by instantiating its record fields with six lemmas on non-negativity and matching. A physicist checking Recognition Science reproduction of Standard Model Higgs phenomenology at tree level would cite it to bundle partial-width non-negativity, total-width non-negativity, branching-ratio non-negativity, signal-strength unity, and amplitude-phase-space agreement. The construction is a direct record instantiation that assembles the lemmas without additional proof.
Claim. Let $C$ be the Higgs observable skeleton certificate. Then $C$ satisfies: for all amplitudes $a$ and phase spaces $p_s$, $0 ≤ p_s$ implies $0 ≤ Γ_{partial}(a, p_s)$; for any list of channels, if every channel phase space is non-negative then the total width is non-negative; branching ratios are likewise non-negative; the signal-strength modifier equals 1 whenever numerator and denominator agree; and tree-level partial widths match when both amplitudes and phase spaces agree.
background
The module formalises the target surface of Higgs collider observables—partial widths, branching ratios, and signal-strength modifiers—as abstract structural objects parametrised by amplitudes and phase-space factors. Its purpose is to expose, in Lean-checkable form, the precise content of tree-level matching between Recognition Science and the Standard Model: when RS-derived Higgs mass, Yukawa couplings, and gauge couplings equal their SM values, the tree-level partial widths computed from the same amplitude formula must be identical. Loop-level channels such as $h→γγ$ remain tagged LOOP_LEVEL_OPEN.
proof idea
This is a definition that directly constructs the HiggsObservableSkeletonCert record. It assigns the six fields to the corresponding upstream lemmas: partialWidth_nonneg supplies pw_nonneg, totalWidth_nonneg supplies tw_nonneg, branchingRatio_nonneg supplies br_nonneg, signalStrength_one_of_match supplies signal_unity, partialWidth_match supplies tree_pw_match, and tree_level_branching_ratio_match supplies tree_br_match.
why it matters
The certificate is consumed by higgsEFTLowEnergyLimitCert, which bundles it together with the EFT bridge, electroweak mass bridge, Yukawa bridge, and longitudinal scattering certificate. It realises the structural identities required for tree-level RS–SM matching of Higgs observables, as described in the module status section. The downstream theorem higgsObservableSkeletonCert_inhabited immediately follows by exhibiting this explicit inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.