signalStrength_one_of_match
plain-language theorem explainer
When the input rate parameter equals itself and is nonzero, the signal strength modifier evaluates to unity. Collider phenomenologists checking Recognition Science against Higgs data would cite this to confirm tree-level reproduction of Standard Model expectations. The proof is a one-line wrapper that unfolds the signalStrength definition and simplifies directly under the nonzero hypothesis.
Claim. For any real number $x$ with $x ≠ 0$, the signal strength modifier satisfies $μ(x,x)=1$, where $μ$ is the ratio of the computed partial width to the reference width when numerator and denominator amplitudes agree.
background
The Higgs Observable Skeleton module defines abstract structural objects for partial widths, branching ratios, and signal-strength modifiers parametrized by amplitudes and phase-space factors. The signal strength modifier is the ratio that quantifies agreement between an RS-derived amplitude and its Standard Model reference. Upstream structures include PhiForcingDerived.of for J-cost calibration and SpectralEmergence.of for the forced SU(3)×SU(2)×U(1) gauge content and three-generation structure.
proof idea
The proof is a one-line wrapper that unfolds the definition of signalStrength and applies the simp tactic with the hypothesis that the input parameter is nonzero, yielding the identity immediately.
why it matters
This supplies the signal_unity field inside higgsObservableSkeletonCert, which collects the nonnegativity and matching properties required to certify that the skeleton reproduces SM observables at tree level when couplings agree. It fills the structural identity step in the module's tree-level matching program and touches the open question of loop-level partial widths tagged LOOP_LEVEL_OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.