`comparison`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.StandardModel.StrongCP on GitHub at line 172.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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.