StrongCPNumericalCert
plain-language theorem explainer
The StrongCPNumericalCert structure certifies that the Recognition Science prediction sets θ_QCD exactly to zero, places it inside the neutron-EDM bound of 10^{-10}, and establishes that the J-cost function reaches its global minimum at this value. It also records a numerical gap to the nearest non-zero multiple of π/4 and the absolute-value containment. Researchers working on the strong-CP problem cite this certificate when assembling the full 8-tick resolution of the fine-tuning puzzle. The structure is assembled directly from the three named
Claim. The structure asserts that the RS-predicted value satisfies θ = 0, that -θ_max < 0 < θ_max where θ_max = 10^{-10}, that |0| < θ_max, that 1 - cos(π/4) > 0.29, and that the function J(θ) = 1 - cos θ obeys J(0) ≤ J(θ) for all real θ.
background
In the StandardModel.StrongCP module the strong-CP problem is posed as the unexplained smallness of the QCD vacuum angle θ_QCD. Recognition Science resolves it by imposing the eight-tick octave (T7) that restricts allowed phases to multiples of π/4 and then selecting the phase that minimizes the J-cost. The upstream definition thetaJCost supplies J(θ) := 1 - cos θ, whose unique minimum occurs at θ = 0. The companion definitions fix the RS prediction at exactly zero and the experimental ceiling at 10^{-10} from the neutron electric-dipole-moment limit.
proof idea
This is a structure definition that packages five fields. The first three fields are obtained by direct substitution of the constants theta_RS_predicted and theta_experimental_max. The gap_to_next field is a numerical inequality on the cosine at π/4. The final field J_cost_min is the universal minimality statement already proved for thetaJCost at zero.
why it matters
The certificate supplies the numerical closure for the strong-CP resolution inside the eight-tick framework (T7). It is consumed by the downstream definition strongCPNumericalCert that assembles the complete statement. The construction therefore links the discrete phase constraint of the eight-tick octave directly to the experimental bound and to the J-cost selection rule that forces θ = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.