Standard Model Higgs Observable Skeleton

The observable skeleton

The standard model of particle physics describes the Higgs boson through a set of measurable quantities: how often it decays into each possible final state, and how strongly it is produced. Experimenters report these as partial widths, branching ratios, and signal-strength modifiers. A partial width is the rate for one decay channel, such as Higgs to two photons. A branching ratio is that channel's share of the total decay rate. A signal-strength modifier compares a measured rate against the standard model's prediction, with 1 meaning perfect agreement.

The Higgs Observable Skeleton module in the Recognition Science library does not compute these quantities from first principles. Its purpose is narrower and more precise: it formalizes the structure of these observables so that a specific claim can be checked. The claim is conditional. If the framework's derived Higgs mass equals the standard model value, if its derived Yukawa coupling for a fermion equals the standard model's, and if its gauge coupling matches, then the tree-level partial width into that channel, computed from the same amplitude formula, must be numerically identical. The module proves this as a conditional theorem: equal inputs give equal outputs, by the definition of the width as phase space times the square of the amplitude.

The module also proves structural facts that hold regardless of the physics. Total width is nonnegative when every channel's phase-space factor is nonnegative. Branching ratios stay between zero and one. A signal-strength modifier equals 1 when the framework's rate matches the standard model's, and equals 0 when the framework predicts no rate at all. These are not empirical claims; they are identities that follow from the definitions, checked by the machine.

What the module does not do is just as important. Loop-level corrections, such as the Higgs-to-two-photons decay that proceeds through a virtual top-quark loop, require explicit loop amplitudes. Those are not yet in the library, and the module tags them as open. The skeleton is the target surface: it says what a match would look like, and it proves the tree-level part of that match, while leaving the loop-level part as a defined goal.

/-- The decisive structural matching theorem: if the RS amplitude and
    phase space for a channel equal their SM counterparts, then the RS
    partial width equals the SM partial width.

    The hypothesis is exactly the content of "RS reproduces the SM tree
    amplitude in this channel."  In practice this hypothesis is satisfied
    once the canonical-normalisation map of `HiggsEFTBridge` and the
    Yukawa map of `HiggsYukawaBridge` are closed for the channel of
    interest. -/
theorem tree_level_partial_width_match
    (amp_RS amp_SM phaseSpace_RS phaseSpace_SM : ℝ)
    (hamp : amp_RS = amp_SM)
    (hps : phaseSpace_RS = phaseSpace_SM) :
    partialWidth amp_RS phaseSpace_RS = partialWidth amp_SM phaseSpace_SM :=
  partialWidth_match amp_RS amp_SM phaseSpace_RS phaseSpace_SM hamp hps

/-- The signal-strength modifier equals 1 when both numerator and
    denominator agree. -/
theorem signalStrength_one_of_match
    (x : ℝ) (hx : x ≠ 0) :
    signalStrength x x = 1 := by
  unfold signalStrength
  simp [hx]

What this page does not claim

This module does not compute any standard model partial width from scratch. This module does not prove that the framework's couplings actually equal the standard model values. Loop-level Higgs decays are not covered by any theorem in this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/HiggsObservableSkeleton.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: