pith. machine review for the scientific record. sign in
def definition def or abbrev high

higgsObservableSkeletonCert

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

Lean usage

  observable   := higgsObservableSkeletonCert

formal statement (Lean)

 215def higgsObservableSkeletonCert : HiggsObservableSkeletonCert where
 216  pw_nonneg     := partialWidth_nonneg

proof body

Definition body.

 217  tw_nonneg     := totalWidth_nonneg
 218  br_nonneg     := branchingRatio_nonneg
 219  signal_unity  := signalStrength_one_of_match
 220  tree_pw_match := partialWidth_match
 221  tree_br_match := tree_level_branching_ratio_match
 222

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.