particleMass
plain-language theorem explainer
Particle mass is obtained by multiplying the Yukawa coupling strength by the vacuum expectation value. Researchers deriving Standard Model particle masses from J-cost symmetry breaking would cite this when translating ledger weights into observable masses. The definition is a direct scalar multiplication that follows from the YukawaCoupling structure and the fixed vev constant.
Claim. Let $y$ be a Yukawa coupling with positive strength $y_c > 0$. The particle mass is $m = y_c v$, where $v = phi$ denotes the vacuum expectation value.
background
The module derives the Higgs mechanism from the J-cost functional $J(x) = 1/2(x + 1/x) - 1$, which has a minimum at $x=1$ and $x$ to $1/x$ symmetry. Spontaneous symmetry breaking occurs when the vacuum selects the golden ratio scale, generating masses proportional to the recognition cost at that point. YukawaCoupling is the structure recording a particle's name and its positive dimensionless coupling strength, interpreted as ledger weight in the simplicial ledger. The vev constant is defined as phi, the self-similar fixed point forced by the universal forcing chain.
proof idea
This is a one-line definition that multiplies the coupling field of the YukawaCoupling structure by the vev constant.
why it matters
It supplies the explicit mass formula used by the downstream mass_positive theorem, which proves positivity via mul_pos on the coupling and vev_pos. The declaration fills the mass-generation step in the module's target derivation of the Higgs mechanism from J-cost symmetry breaking, connecting directly to the phi-ladder mass formula and the eight-tick octave scale. It touches the open question of deriving specific Yukawa values from the recognition composition law rather than postulating them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.