higgsObservableSkeletonCert_inhabited
plain-language theorem explainer
The theorem proves that the certificate type collecting non-negativity of partial widths, total widths, and branching ratios for Higgs observables is inhabited. Researchers formalizing Recognition Science predictions for collider phenomenology would reference it to establish that the abstract observable structure is well-defined. The proof consists of a single term supplying the explicit certificate construction as witness.
Claim. The type of certificates for the Higgs observable skeleton is non-empty, where each certificate comprises the statements that partial widths are non-negative whenever the phase-space factor is non-negative, total widths are non-negative when all channel contributions are non-negative, and branching ratios are non-negative under the same conditions.
background
This module formalizes the target surface of Higgs collider observables as abstract structural objects parametrized by amplitudes and phase-space factors. The certificate structure assembles theorems asserting non-negativity of partial widths on physical phase space, non-negativity of total widths, and non-negativity of branching ratios. The upstream definition constructs the certificate by bundling the non-negativity lemmas for each component.
proof idea
The proof is a one-line term that directly supplies the explicit construction of the certificate as the witness for non-emptiness.
why it matters
It establishes the basic existence of the master certificate for Higgs observables in the Recognition Science framework, enabling statements about tree-level matching to the Standard Model when couplings agree. The module notes that loop-level channels such as h to gamma gamma remain open. This step precedes any conditional matching theorems for specific RS parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.