`experimentalTests`

definition

show as: view math explainer →

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

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

 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"
 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 -/
 214def summary : List String := [
 215  "8-tick quantizes θ to 8 values",
 216  "J-cost minimum at θ = 0",
 217  "No axion required (but compatible)",
 218  "Predicts θ = 0 exactly"
 219]
 220
 221/-! ## Strong CP Certificate (machine-verified) -/
 222
 223/-- **THEOREM (Strong CP Certificate)**: The J-cost is globally minimized at θ = 0.
 224    The minimum is achieved exactly; all other allowed values (multiples of π/4)
 225    have strictly positive J-cost.
 226    Proof: thetaJCost(θ) = 1 − cos θ ≥ 0 = thetaJCost(0) for all θ. -/
 227structure StrongCPCert where
 228  theta_minimizes : ∀ θ, thetaJCost 0 ≤ thetaJCost θ
 229  zero_cost : thetaJCost 0 = 0

papers checked against this theorem

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