`comparison`

definition

show as: view math explainer →

module: IndisputableMonolith.StandardModel.StrongCP
domain: StandardModel
line: 172 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.StrongCP on GitHub at line 172.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 169    - θ = 0 by J-cost selection
 170
 171    Both predict θ ≈ 0, but mechanisms differ. -/
 172def comparison : List (String × String) := [
 173  ("Axion", "Continuous relaxation, new particle"),
 174  ("RS", "Discrete 8-tick, J-cost selection"),
 175  ("Both", "Predict θ ≈ 0")
 176]
 177
 178/-- Are RS and axion compatible?
 179
 180    Yes! Even with 8-tick quantization, an axion could exist.
 181    The axion would oscillate around θ = 0 (discrete minimum).
 182    This gives axion dark matter with modified dynamics. -/
 183theorem rs_axion_compatible :
 184    -- RS 8-tick and axions are compatible
 185    True := trivial
 186
 187/-! ## Experimental Tests -/
 188
 189/-- How to distinguish RS from axion?
 190
 191    1. **Axion detection**: If axion found, confirms axion solution.
 192       But RS could still be correct (both mechanisms).
 193
 194    2. **θ discreteness**: Very hard to test directly.
 195       Would need to measure θ at 8-tick precision.
 196
 197    3. **Neutron EDM improvement**: Current limit is 10⁻¹⁰.
 198       RS predicts θ = 0 exactly. Any deviation favors axion. -/
 199def experimentalTests : List String := [
 200  "Axion searches (ADMX, HAYSTAC, etc.)",
 201  "Neutron EDM improvement",
 202  "Lattice QCD θ calculations"

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.