AxionSolution
plain-language theorem explainer
The AxionSolution structure packages parameters for the Peccei-Quinn mechanism that dynamically relaxes the QCD theta parameter to zero via a new Goldstone boson. Physicists extending Recognition Science to the strong CP problem cite it when linking 8-tick symmetry to axion dynamics. The declaration is a plain structure with three fields that directly record the PQ scale, axion mass, and coupling targets.
Claim. A structure whose fields are the PQ breaking scale $f_a : ℝ$, the axion mass $m_a : ℝ$, and a list of Standard-Model fields to which the axion couples.
background
The module treats the strong CP problem as the unexplained smallness of the coefficient θ in the QCD term θ(g²/32π²)GμνG̃μν, experimentally bounded by |θ| < 10^{-10}. Recognition Science attributes the selection of θ = 0 to 8-tick symmetry imposing discrete phase constraints that J-cost minimization then drives to the zero minimum. The Peccei-Quinn route introduces a new U(1) symmetry whose breaking produces an axion whose potential relaxes θ dynamically, with mass scaling m_a ~ f_π m_π / f_a.
proof idea
The declaration is a structure definition that introduces the three fields without lemmas, tactics, or computation. It functions as a typed container for the numerical and coupling data of the axion solution.
why it matters
AxionSolution supplies the type instantiated by the downstream definition axionProperties, which hard-codes concrete values (PQ scale 10^{10} GeV, mass 10^{-5} eV). It occupies the axion branch of the module's proposed solutions and connects the theta-zero outcome to the eight-tick octave (T7) and J-cost minimization in the forcing chain. The structure thereby supports later claims about axion dark matter and allowed theta ranges inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.