theta_RS_inside_experimental
plain-language theorem explainer
The theorem confirms that the Recognition Science prediction of exactly zero for the QCD theta angle lies strictly inside the experimental bound of 10^{-10} from neutron EDM measurements. Particle physicists studying the strong CP problem would cite it to show that eight-tick symmetry resolves the fine-tuning issue without axions or other extensions. The proof reduces the claim to numerical inequalities by unfolding the constant definitions and applies norm_num to confirm both sides of the conjunction.
Claim. $-10^{-10} < 0 < 10^{-10}$, where the left and right bounds are the experimental limit on $|θ_{QCD}|$ and the Recognition Science prediction is $θ_{RS} = 0$ selected by J-cost minimization.
background
The module SM-008 addresses the strong CP problem by deriving $θ_{QCD} ≈ 0$ from eight-tick symmetry. The QCD Lagrangian contains the term $θ (g²/32π²) G_{μν} G̃^{μν}$, which violates CP unless $θ$ is tiny; the eight-tick structure forces $θ$ to multiples of $π/4$, after which J-cost minimization selects exactly zero. Upstream definitions set $θ_{RS predicted} = 0$ and $θ_{experimental max} = 10^{-10}$ from neutron EDM constraints.
proof idea
The term-mode proof unfolds the two constant definitions, reducing the statement to the numerical claim $-1e-10 < 0 ∧ 0 < 1e-10$. It then uses refine to split the conjunction and norm_num to discharge both inequalities.
why it matters
This supplies the inside_experimental field of the strongCPNumericalCert record, which bundles all numerical checks that the RS mechanism satisfies the strong CP bound. It directly implements the module claim that eight-tick symmetry selects $θ = 0$, consistent with the T7 eight-tick octave and T5 J-uniqueness in the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.