comparison
plain-language theorem explainer
The declaration supplies a static three-row comparison of the axion mechanism against the Recognition Science 8-tick resolution of the strong CP problem. Researchers examining discrete alternatives to the axion would cite the entry that both routes select theta approximately zero. The definition is a direct list literal with no computation or lemmas.
Claim. A side-by-side summary of solutions to the strong CP problem lists: axion solution via continuous relaxation through a new particle; Recognition Science solution via discrete 8-tick quantization and J-cost selection; both solutions predict θ ≈ 0.
background
The module treats the strong CP problem as the unexplained smallness of the QCD theta term θ (g²/32π²) G_μν G̃^μν, bounded by |θ| < 10^{-10}. Recognition Science resolves it by imposing discrete phase constraints from the eight-tick octave, so θ must be a multiple of π/4 and J-cost minimization forces the zero value. Upstream definitions include tick as the fundamental time quantum τ₀ = 1, the Axion structure carrying mass and decay constant, and cost as the J-cost of a recognition event or multiplicative recognizer.
proof idea
The definition is a direct list literal that enumerates the three string pairs. No tactics or upstream lemmas are invoked.
why it matters
The entry anchors the module's claim that 8-tick symmetry (T7) selects θ = 0 without new particles, contrasting the axion structure from Cosmology.DarkMatter. It supports downstream anchors for mass ratios and the W-mass anomaly explanation. The comparison leaves open whether the discrete minimum fully accounts for axion dark matter dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.