signalStrength_zero_of_RS_zero
plain-language theorem explainer
The theorem states that the Higgs signal strength modifier vanishes whenever the RS rate contribution is set to zero, for any nonzero phase-space factor y. Collider phenomenologists matching Recognition Science amplitudes to LHC data would cite this when confirming that a null RS tree-level rate produces a null observable. The proof is a one-line term reduction that unfolds the signalStrength definition and simplifies using the nonzero hypothesis on y.
Claim. Let rs denote the RS-derived rate contribution and y the phase-space factor. Then the signal strength modifier satisfies $mu(0,y)=0$ for all $yneq 0$.
background
The Higgs Observable Skeleton module defines abstract structural objects for collider observables: partial widths, total widths, branching ratios, and signal-strength modifiers, each parametrised by an amplitude and a phase-space factor. These objects are introduced precisely to make the statement 'RS reproduces SM tree-level phenomenology' Lean-checkable once the canonical normalisation map and Yukawa map are closed. Upstream foundations supply the arithmetic and forcing machinery (canonical arithmetic objects, J-cost structures, eight-tick phases) that underwrite the rate definitions, but the present theorem uses only the local unfolding of signalStrength.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of signalStrength and applies simp with the hypothesis hy : y ≠ 0, which immediately yields the zero result.
why it matters
This identity belongs to the family of structural theorems that close the tree-level matching surface in the Higgs Observable Skeleton. It guarantees consistency of the signal-strength modifier when the RS amplitude vanishes, thereby supporting the broader claim that RS reproduces SM observables once the EFT and Yukawa bridges are satisfied. The module flags loop-level channels (h → γγ, h → gg) as still open; the present result is unaffected by those gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.