allowedTheta
plain-language theorem explainer
Recognition Science restricts the QCD theta parameter to eight discrete values fixed by eight-tick symmetry. A physicist studying the strong CP problem would cite this enumeration to see how the T7 octave quantizes theta to multiples of pi/4. The definition is a direct list construction that encodes the periodicity constraint from the forcing chain.
Claim. The QCD vacuum angle is restricted to the discrete set $0, {1/4}pi, {1/2}pi, {3/4}pi, pi, {5/4}pi, {3/2}pi, {7/4}pi$ by eight-tick symmetry.
background
The StandardModel.StrongCP module recasts the strong CP problem inside Recognition Science. The Lagrangian term theta (g squared over 32 pi squared) G mu nu times G tilde mu nu permits any theta in [0, 2 pi), yet experiment demands absolute value less than 10 to the minus 10. Eight-tick symmetry (T7) forces theta to equal k pi over 4 for k from 0 to 7, after which J-cost minimization selects the CP-conserving points.
proof idea
The declaration is a direct definition that enumerates the eight values compatible with the eight-tick octave. It draws on the cost functions imported from ObserverForcing and MultiplicativeRecognizerL4 together with the ledger factorization structure, though the body itself consists only of explanatory comments on J-cost ranking.
why it matters
This supplies the candidate set for theta in the SM-008 treatment of the strong CP problem. It implements the discrete phase constraint from the eight-tick octave (T7) in the UnifiedForcingChain and prepares J-cost selection that favors theta equals zero. No downstream results yet consume it, so the link to the neutron EDM bound remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.