module module

`IndisputableMonolith.StandardModel.StrongCP`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (26)

structure ThetaQCD L48
def theta_experimental_bound L55
def neutronEDM L62
theorem theta_finetuning L72
def thetaContributions L83
structure AxionSolution L99
def axionProperties L104
def axionDarkMatter L111
def allowedTheta L122
def thetaJCost L130
theorem theta_zero_minimizes L133
theorem theta_zero_selected L153
def comparison L172
theorem rs_axion_compatible L183
def experimentalTests L199
def summary L214
structure StrongCPCert L227
def strongCPCert L232
def theta_RS_predicted L254
def theta_experimental_max L257
theorem theta_RS_inside_experimental L260
theorem abs_theta_RS_lt_bound L267
theorem strong_cp_gap L277
structure StrongCPNumericalCert L291
def strongCPNumericalCert L300
structure StrongCPFalsifier L313