YukawaCoupling
plain-language theorem explainer
YukawaCoupling packages a particle string identifier, a positive real coupling strength y, and its positivity witness. Recognition Science modelers of mass generation from J-cost symmetry breaking cite the structure when converting ledger weights into Standard Model Yukawa terms. The declaration is a plain structure with three fields and no computational reduction.
Claim. A Yukawa coupling consists of a particle name (string), a coupling strength $y > 0$, and an explicit witness that $y > 0$.
background
The module derives the Higgs mechanism from the J-cost functional $J(x) = ½(x + x^{-1}) - 1$, which has a minimum of zero at $x = 1$ and is invariant under $x ↔ x^{-1}$. Spontaneous symmetry breaking occurs when the vacuum selects a value such as the golden ratio, after which particle masses arise proportional to the J-cost evaluated at that vacuum expectation value. Upstream results on primitive distinctions supply the axiomatic base from which the J-cost minimum and symmetry are obtained.
proof idea
The declaration is a structure definition that directly assembles the particle identifier, the real coupling, and the positivity constraint. No lemmas or tactics are invoked; it functions as a typed data carrier for the subsequent mass definition.
why it matters
The structure supplies the argument type for particleMass and mass_positive in the same module. It completes the mass-generation step inside the J-cost symmetry-breaking derivation, linking the Recognition Composition Law and the eight-tick octave to concrete particle masses. Downstream theorems then establish positivity of the resulting masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.