module module moderate

`IndisputableMonolith.StandardModel.StrongCP`

The StandardModel.StrongCP module introduces the QCD theta parameter inside Recognition Science. It assembles definitions and lemmas on theta bounds, neutron EDM, axion properties, and minimization using the discrete clock. Particle physicists addressing the strong CP problem would cite these objects. The module is a container of definitions and supporting statements with no internal proofs.

claim$θ_{QCD}$ is the QCD theta parameter in the Recognition Science Standard Model, subject to the experimental bound from the neutron electric dipole moment and connected to the 8-tick cycle.

background

The module sits in the StandardModel domain and imports the RS time quantum $τ_0 = 1$ tick together with the 8-tick structure whose phases run through $0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4$. Its single-line doc-comment identifies the core object as the QCD theta parameter. Sibling declarations cover theta experimental bound, neutronEDM, theta finetuning, thetaContributions, AxionSolution, and theta zero selection.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the theta parameter and related statements that prepare the strong sector of the Standard Model. It draws on the eight-tick octave (T7) from the forcing chain and the RS-native constants. No used-by edges are recorded yet.

scope and limits

Does not derive a numerical value for theta from the J-cost or RCL.
Does not prove dynamical selection of theta equals zero.
Does not contain the full axion potential or dark-matter calculation.
Does not address lattice QCD or non-RS ultraviolet completions.

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