Pith. sign in
module module moderate

IndisputableMonolith.StandardModel.StrongCP

show as:
view Lean formalization →

Module on the QCD vacuum angle θ in Recognition Science: it packages experimental bounds, the neutron EDM link, axion alternatives, and a J-cost argument that forces θ = 0. Particle theorists and anyone tracing the strong-CP resolution in the RS forcing chain would cite it. Structure is definitional scaffolding plus cost-minimization lemmas tied to the eight-tick clock and Constants.

claimThe module introduces the QCD angle $\theta_{\mathrm{QCD}}$, the experimental bound from the neutron EDM, the fine-tuning measure of a nonzero $\theta$, and a Recognition cost $J(\theta)$. It records axion-based escapes, then asserts that $\theta = 0$ uniquely minimizes the cost on the eight-tick structure and is therefore selected.

background

In ordinary QCD the topological term $\theta G\tilde{G}$ is CP-odd. Experiment (neutron EDM) forces $|\theta|\lesssim 10^{-10}$, which is unnatural unless a dynamical mechanism (axion) or a selection principle sets $\theta=0$. Recognition Science supplies the latter via the unique cost $J$ fixed by the Recognition Composition Law.

The module sits on RS Constants (native units, $\tau_0$ tick) and the Foundation.EightTick discrete clock: phases $0,\pi/4,\ldots,7\pi/4$. Sibling declarations name $\Theta_{\mathrm{QCD}}$, the experimental bound, neutron EDM, fine-tuning, axion properties, an allowed-$\theta$ set, the $\theta$-dependent $J$-cost, and the claims that $\theta=0$ minimizes and is selected.

Local setting is Standard Model phenomenology inside the RS ledger: $\theta$ is treated as a cost parameter on the eight-tick octave rather than a free continuous coupling.

proof idea

Definition-heavy module, not a single theorem. It introduces $\Theta_{\mathrm{QCD}}$ and related quantities (bounds, EDM, axion data), defines a $J$-cost of nonzero $\theta$, then proves minimization and selection lemmas: $\theta=0$ is the unique cost minimum and is therefore forced. Upstream material is only Constants and EightTick; the cost comparison is the working engine. No deep tactic scripts are implied by the module surface.

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 (RCL). A clean $\theta=0$ selection removes an open Standard-Model fine-tuning from the RS ledger and aligns the strong sector with CP-even eight-tick structure (T7) and $J$-uniqueness (T5). Downstream forcing can therefore treat strong CP as settled by cost rather than by an extra axion field. The module also keeps the conventional axion story as a named alternative for comparison.

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)