pith. machine review for the scientific record. sign in
theorem proved term proof

rs_axion_compatible

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 183theorem rs_axion_compatible :
 184    -- RS 8-tick and axions are compatible
 185    True := trivial

proof body

Term-mode proof.

 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. -/

depends on (11)

Lean names referenced from this declaration's body.