gmorPrediction
plain-language theorem explainer
The gmorPrediction definition supplies the numerical value of the Gell-Mann-Oakes-Renner relation for pion masses within the Recognition Science framework. A physicist modeling chiral symmetry breaking in QCD would reference this when checking consistency between the φ-ladder and empirical meson data. The definition is a direct one-line expression that multiplies the light quark mass by the cube of the quark condensate and divides by the square of the pion decay constant.
Claim. The GMOR prediction for the squared pion mass is given by the real number $2 m_q ⟨q̄q⟩ / f_π²$, where $m_q$, ⟨q̄q⟩, and $f_π$ denote the light quark mass, chiral condensate, and pion decay constant in MeV units.
background
In the Pion Masses module, pions are treated as quark-antiquark bound states whose masses arise from explicit chiral symmetry breaking. The GMOR relation connects the pion mass squared to the product of the average light quark mass and the quark condensate, normalized by the square of the pion decay constant. Upstream structures such as the ledger factorization and spectral emergence supply the constants lightQuarkMass_MeV, quarkCondensate_MeV, and pionDecayConstant_MeV that enter the expression.
proof idea
The definition is a direct algebraic expression that substitutes the three empirical constants drawn from upstream modules into the standard GMOR formula. No tactics are required beyond the built-in real arithmetic.
why it matters
This definition supplies the input value for the reasonableness check gmor_reasonable, which verifies that the prediction lies between 100 and 100000. It fills the GMOR check step in the P-013 pion masses derivation, linking the chiral condensate to the φ-ladder placement of the pion. The result supports the broader claim that meson masses follow from the eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.