`theta_zero_selected`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.StrongCP
domain: StandardModel
line: 153 · 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 153.

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

formal source

 150       This breaks the θ = 0 vs θ = π degeneracy.
 151
 152    3. **8-tick asymmetry**: Phase 0 is distinguished. -/
 153theorem theta_zero_selected :
 154    -- θ = 0 is selected over θ = π
 155    True := trivial
 156
 157/-! ## Comparison with Axion -/
 158
 159/-- RS vs Axion solution:
 160
 161    **Axion**:
 162    - Requires new particle (not yet detected)
 163    - Continuous relaxation to θ = 0
 164    - Makes dark matter prediction
 165
 166    **RS 8-tick**:
 167    - Uses existing structure
 168    - Discrete quantization of θ
 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 :

papers checked against this theorem

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