Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.StrongCP

show as:
view Lean formalization →

Module treating the QCD strong-CP angle θ as a Recognition cost variable on the eight-tick clock. It packages the experimental EDM bound, the fine-tuning problem, axion dynamics, and a J-cost argument that selects θ = 0. Downstream forcing-chain work cites it when closing Standard-Model CP structure from the cost foundation.

claimThe QCD vacuum angle $\theta$ is treated as a real parameter whose physical effects (neutron EDM, fine-tuning) are bounded experimentally. Recognition Science assigns a $J$-cost $J(\theta)$ on the eight-tick phase lattice and proves that $\theta = 0$ uniquely minimizes that cost, thereby selecting a CP-conserving strong sector without an axion as a logical necessity (while still recording the axion solution as the conventional alternative).

background

In QCD the topological term $\theta,G\tilde{G}$ is CP-odd. Experiment (neutron EDM) forces $|\theta|\lesssim 10^{-10}$, the strong-CP problem. The conventional fix is a dynamical axion that relaxes $\theta$ to zero.

Recognition Science instead views $\theta$ as a phase on the fundamental eight-tick clock (phases $k\pi/4$, $k=0,\ldots,7$). The module imports the RS time quantum $\tau_0$ and the EightTick discrete clock, then defines a $J$-cost on admissible $\theta$ values. Sibling declarations cover the experimental bound, neutron EDM, fine-tuning measure, axion properties and dark-matter role, the allowed set, the cost functional, and the uniqueness of the zero minimum.

The local claim is that cost minimization, not a new particle, forces $\theta=0$.

proof idea

Definition-and-selection module rather than a single theorem. It introduces $\Theta_{\mathrm{QCD}}$ and the experimental window, records the axion solution as background, then builds a $J$-cost on allowed $\theta$. Two core lemmas show that $\theta=0$ minimizes the cost and is therefore selected. Supporting material packages EDM, fine-tuning, and axion dark-matter facts used by later forcing arguments. No deep tactic scripts at module level; the work is the cost identification plus the zero-minimum theorems.

why it matters in Recognition Science

Feeds IndisputableMonolith.Foundation.UnifiedForcingChain, whose doc-comment states that all of T0–T8 are forced from the cost foundation (Recognition Composition Law). Strong-CP closure is part of making the Standard Model’s discrete CP structure inevitable once $J$ and the eight-tick octave (T7) are fixed. The module supplies the RS-native reason $\theta=0$ is preferred, so the forcing chain need not treat strong CP as an extra postulate. It also keeps the axion route visible for comparison with conventional phenomenology.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (26)