pith. machine review for the scientific record. sign in
def definition def or abbrev

experimentalTests

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)

 199def experimentalTests : List String := [

proof body

Definition body.

 200  "Axion searches (ADMX, HAYSTAC, etc.)",
 201  "Neutron EDM improvement",
 202  "Lattice QCD θ calculations"
 203]
 204
 205/-! ## Summary -/
 206
 207/-- RS solution to strong CP:
 208
 209    1. **8-tick quantizes θ**: Only πk/4 allowed
 210    2. **J-cost selects θ = 0**: Minimum J-cost
 211    3. **No new particles needed**: Uses existing structure
 212    4. **Compatible with axion**: Both could be true
 213    5. **Predicts θ = 0 exactly**: Testable -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.