lightQuarkMass_MeV
plain-language theorem explainer
Average light quark mass supplies the explicit breaking scale in the GMOR relation for pion masses. Modelers of chiral symmetry breaking cite this value to check consistency with the 140 MeV pion mass. The definition is a direct arithmetic average of the conventional inputs 2.2 MeV and 4.7 MeV.
Claim. The average light quark mass in MeV is given by $m_q = (2.2 + 4.7)/2$.
background
The Pion Masses module derives the masses of the charged and neutral pions from Recognition Science via the GMOR relation, which states that $m_π^2$ is proportional to $(m_u + m_d)$ times the quark condensate. Standard values are adopted for the light quarks with $m_u ≈ 2.2$ MeV and $m_d ≈ 4.7$ MeV. This definition computes their average for insertion into the mass formula. The upstream scalar constant defines a field that is constant across spacetime and serves as a basic building block for field constructions.
proof idea
This definition evaluates the arithmetic mean of the two quark mass parameters in a single expression. No external lemmas are invoked.
why it matters
This definition feeds the quark mass input into gmorPrediction, which computes the GMOR estimate and is verified for order-of-magnitude agreement in gmor_reasonable. It realizes the explicit chiral symmetry breaking term in the RS pion mass derivation as described in the module documentation. The construction aligns with the phi-ladder patterns for hadron masses and supports predictions such as the pion to electron mass ratio near 273.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.