axionDarkMatter
plain-language theorem explainer
The declaration states that axions with decay constant around 10^12 GeV can comprise all dark matter. Cosmologists and particle physicists working on axion models in Recognition Science would cite it when linking the strong CP resolution to cosmology. It is implemented as a direct string literal assignment.
Claim. If the axion decay constant satisfies $f_a ~ 10^{12}$ GeV, axions can account for the full dark matter density.
background
The module explains the strong CP problem from the QCD Lagrangian term θ (g²/32π²) G_μν G̃^μν, where experimental bounds require |θ| < 10^{-10} despite no a priori reason for this value. Recognition Science imposes 8-tick symmetry that quantizes θ to multiples of π/4, with J-cost minimization selecting θ = 0. Upstream, the tick definition from Constants sets the fundamental time quantum τ₀ = 1 that generates the eight-tick octave period.
proof idea
This is a one-line definition that directly assigns the string literal describing axion dark matter candidacy.
why it matters
It supports the AxionSolution sibling by noting axions as dark matter candidates, connecting the 8-tick quantization (T7) to cosmological scales. The framework landmarks of phi-ladder mass formulas and RS-native constants (c=1, ħ=phi^{-5}) supply the setting, though the entry stays qualitative. It touches the open question of matching the precise relic density to RS parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.