theta_experimental_bound
plain-language theorem explainer
The declaration supplies the numerical upper bound |θ_QCD| < 10^{-10} taken from neutron electric dipole moment data. Particle physicists comparing Recognition Science predictions to the strong CP problem would cite this constant when quantifying the required fine-tuning. It is introduced as a direct noncomputable real constant with no lemmas or computation steps.
Claim. The experimental upper bound on the QCD vacuum angle satisfies $|θ| < 10^{-10}$.
background
The module addresses the strong CP problem in QCD, where the Lagrangian term L_θ = θ (g²/32π²) G_μν G̃^μν allows any θ ∈ [0, 2π) yet experiment requires |θ| extremely small. Recognition Science invokes eight-tick symmetry to impose discrete phase constraints, forcing θ to multiples of π/4 with J-cost minimization selecting θ = 0. This definition supplies the numerical threshold drawn from the neutron EDM limit d_n < 10^{-26} e·cm.
proof idea
Direct definition that assigns the real constant 1e-10 with no tactics or lemmas applied.
why it matters
The constant anchors the fine-tuning discussion in SM-008 by providing the target precision that eight-tick symmetry (T7) must satisfy through J-cost minimization. It supplies the experimental input against which the module's later results on theta zero selection and axion properties are judged, linking to the broader Recognition framework landmarks of the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.