Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.Higgs_Coupling_RS

show as:
view Lean formalization →

Packages the Recognition Science treatment of Higgs-sector couplings as a domain cost, a positive canonical threshold, and an inhabited certificate. SM-matching work that reads Yukawa or portal data on the phi-ladder would cite the certificate. Structure is definitions plus elementary nonnegativity and evaluation lemmas, not a forcing-chain argument.

claimThe module defines a Higgs-domain cost $C_{\mathrm{dom}}$, proves $C_{\mathrm{dom}}\ge 0$ and an evaluation identity, fixes a canonical threshold $\theta_*>0$, and supplies an inhabited certificate type asserting that the RS Higgs-coupling data meet that threshold under the cost.

background

Recognition Science measures mismatch with the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) forced at T5, with self-similar scale $\varphi$ at T6. Couplings and masses are read on the $\varphi$-ladder (yardstick times $\varphi$ to a rung offset, with gap corrections). The Cost import supplies that cost language; Constants supplies RS-native units (including the tick $\tau_0$).

This StandardModel module specializes that language to the Higgs coupling sector. Sibling objects introduce a domain cost, its nonnegativity and pointwise evaluation, a positive canonical threshold, and a certificate bundle HiggsCouplingCert with a concrete inhabitant. The setting is kinematic matching and threshold bookkeeping, not dynamical EWSB.

proof idea

Definition-and-certificate module, not a deep proof development. The domain cost is declared and given an evaluation identity and a nonnegativity lemma. The canonical threshold is a fixed positive quantity with a one-line positivity fact. The certificate type packages the cost-versus-threshold claim; inhabitance is a constructive witness that the packaged data satisfy it. No multi-step tactic chain or upstream forcing lemmas are required beyond Cost/Constants.

why it matters in Recognition Science

Gives the Standard Model layer a checkable RS object for Higgs couplings: cost above a canonical threshold, packaged so downstream SM-matching can assume an inhabited cert rather than re-open the inequality. No used_by edges are recorded yet, so it is presently a leaf packaging module. It sits beside the mass-ladder and Berry-threshold story (creation scale $\varphi^{-1}$, continuum factor near $\varphi^5$) insofar as Higgs couplings are treated as ladder-aligned data, without claiming a full derivation of $m_H$ or the vev from T0--T8.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)