pith. sign in
module module high

IndisputableMonolith.Physics.HiggsVEVFromJCost

show as:
view Lean formalization →

This module certifies that a top Yukawa coupling near unity sets the top-loop recognition ratio exactly to one, allowing the Higgs vacuum expectation value to be read off from the J-cost. Researchers deriving electroweak parameters from the phi-ladder and recognition composition law would cite it. The module consists of targeted definitions and a certification object that links the imported time quantum to the Higgs VEV under the stated Yukawa condition.

claimWith top Yukawa $y_t$ satisfying $y_t = 1$, the top-loop recognition ratio equals unity and the Higgs vacuum expectation value is obtained directly from the J-cost function on the phi-ladder.

background

The module imports Constants, whose sole documented object is the fundamental RS time quantum defined as τ₀ = 1 tick. It introduces the HiggsVEVFromJCost construction together with the sibling objects EWBREAKINGChannel, topYukawa, and HiggsVEVCert. The local theoretical setting is the Recognition Science derivation of particle masses and couplings from the J-cost and the recognition composition law, with the top quark loop singled out because its Yukawa is taken to be order one.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the HiggsVEVCert object that feeds the EWBREAKINGChannel and topYukawa_eq_one siblings. It fills the explicit step in which the top-loop recognition ratio is normalized to unity when y_t ~ 1, thereby closing the link between the J-cost and the Higgs vacuum expectation value inside the physics layer of the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)