pith. machine review for the scientific record. sign in
def definition def or abbrev high

gmorPrediction

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 173def gmorPrediction : ℝ :=

proof body

Definition body.

 174  2 * lightQuarkMass_MeV * (quarkCondensate_MeV^3) / (pionDecayConstant_MeV^2)
 175
 176/-- GMOR prediction is in the right ballpark (within order of magnitude). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.