thetaJCost
plain-language theorem explainer
The J-cost of an angle θ is given by 1 minus its cosine, which vanishes at θ = 0 and reaches its maximum at θ = π. Researchers addressing the strong CP problem cite this definition to quantify how 8-tick symmetry plus cost minimization forces the QCD vacuum angle to zero. The definition is a direct one-line expression using the standard cosine function.
Claim. The J-cost function for the strong CP angle is defined by $J(θ) := 1 - cos θ$.
background
In the Recognition Science treatment of the strong CP problem, the 8-tick structure restricts possible values of the QCD vacuum angle θ to multiples of π/4. The J-cost is introduced to select among these discrete values by assigning a non-negative real number that is zero precisely when CP is conserved. This module imports the eight-tick foundation and constants to embed the strong CP term within the larger RS framework.
proof idea
This is a one-line definition that directly encodes the J-cost expression 1 - cos θ without any additional lemmas or reductions.
why it matters
This definition supplies the cost function used by the StrongCPCert structure to certify that θ = 0 is the unique global minimum among allowed 8-tick values. It thereby closes the RS mechanism for the strong CP problem without introducing new particles, as summarized in the module's summary list. The construction relies on the eight-tick octave (T7) and J-uniqueness (T5) from the foundational chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.