axionProperties
axionProperties records a concrete Peccei-Quinn axion instance with PQ scale 10^{10} GeV, mass 10^{-5} eV, and couplings to photons, nucleons, and electrons. Researchers testing axion dark matter or strong CP solutions would cite these parameter choices when comparing Recognition Science predictions to bounds. The definition is a direct record construction of the AxionSolution structure using the supplied numerical fields.
claimThe Peccei-Quinn axion solution is realized by the record with PQ breaking 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 as the unexplained smallness of the QCD theta term, experimentally bounded by |theta| < 10^{-10}. Recognition Science attributes theta = 0 to 8-tick symmetry, which restricts theta to multiples of pi/4 and selects the zero value by J-cost minimization on the phi-ladder.
proof idea
The definition directly constructs an AxionSolution record by assigning the three fields to the listed constants. No lemmas or tactics are invoked; it is a plain record literal.
why it matters in Recognition Science
The definition supplies a working numerical example inside the AxionSolution structure for the module's target of explaining theta_QCD ≈ 0 from 8-tick symmetry. It aligns with the eight-tick octave and J-cost selection of theta = 0, providing a concrete instance that can be referenced by sibling declarations on axion dark matter.
scope and limits
- Does not derive the chosen numerical values from the forcing chain or phi-ladder.
- Does not prove dynamical relaxation of theta to zero.
- Does not connect the parameters to the mass formula or Berry threshold.
- Does not address experimental constraints beyond the listed couplings.
formal statement (Lean)
104def axionProperties : AxionSolution := {
proof body
Definition body.
105 pq_scale := 1e10, -- GeV
106 axion_mass := 1e-5, -- eV
107 couples_to := ["photons", "nucleons", "electrons"]
108}
109
110/-- Axions are also a dark matter candidate! -/