pith. sign in
module module high

IndisputableMonolith.StandardModel.HiggsYukawaBridge

show as:
view Lean formalization →

The module encodes the Standard Model Yukawa extraction rule that converts φ-ladder mass predictions into dimensionless couplings. Physicists tracing the Recognition Science derivation of the Higgs sector cite it when linking the master mass law to effective-field-theory parameters. It supplies a set of definitions and short lemmas that implement the rule y_f = √2 m_f / v using imported mass anchors, without numerical evaluation or experimental fitting.

claimThe Yukawa coupling for a fermion f is defined by $y_f = √2 · m_f / v$, where $m_f$ is the mass obtained from the φ-ladder formula in the appropriate sector and rung, and $v$ is the vacuum expectation value.

background

The module operates inside the Standard Model sector of Recognition Science. It draws the fundamental time quantum τ₀ = 1 tick from Constants, the canonical mass constants from Anchor, and the master mass law from MassLaw. The master mass law states that every stable recognition state occupies a rung on the φ-ladder with mass proportional to coherence energy scaled by sector yardstick and rung position. The supplied doc-comment fixes the extraction convention y_f = √2 m_f / v with m_f taken directly from the φ-ladder prediction.

proof idea

This is a definition module, no proofs. It assembles the Yukawa objects by direct application of the imported mass law and the extraction convention stated in the module doc-comment.

why it matters in Recognition Science

The module supplies the Yukawa bridge required by the Higgs EFT low-energy limit chain and the Higgs observable skeleton. It completes the step that converts φ-ladder masses into the couplings used in the six-module Standard-Model Higgs effective-field-theory sequence cited in the root IndisputableMonolith module. No open scaffolding remains inside the module itself.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)