axionProperties
plain-language theorem explainer
axionProperties supplies concrete parameter values for the Peccei-Quinn axion solution inside the Recognition Science account of the strong CP problem. A physicist comparing axion dark matter candidates or neutron EDM bounds to RS predictions would reference these numbers. The definition is a direct record that populates the three fields of the AxionSolution structure with a PQ scale, mass, and coupling list.
Claim. The axion solution is instantiated with Peccei-Quinn scale $f_a = 10^{10}$ GeV, axion mass $m_a = 10^{-5}$ eV, and couplings to photons, nucleons, and electrons.
background
The module treats the strong CP problem arising from the QCD theta term $L_θ = θ (g²/32π²) G_μν G̃^μν$ with θ ∈ [0, 2π). Recognition Science invokes 8-tick symmetry to force discrete phase constraints, after which J-cost minimization selects θ = 0. The AxionSolution structure encodes the Peccei-Quinn mechanism: a new U(1)_PQ symmetry is broken, yielding a Goldstone boson whose vacuum expectation value dynamically relaxes θ to zero, with mass scaling $m_a ~ f_π m_π / f_a$.
proof idea
This is a direct definition that instantiates the AxionSolution structure by assigning literal values to its three fields.
why it matters
The definition supplies explicit numbers that can be inserted into J-cost or theta-minimization calculations within the SM-008 target. It sits inside the 8-tick framework (T7) that imposes the discrete phase constraints leading to θ = 0. No downstream theorems are recorded yet, leaving open how these parameters will be linked to the phi-ladder mass formula or Berry creation threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.