strong_cp_gap
plain-language theorem explainer
The theorem quantifies the J-cost gap for nonzero phases in the 8-tick lattice, establishing that any allowed θ ≠ 0 satisfies J-cost at least 0.29 above the θ = 0 minimum. Researchers addressing the strong CP problem through Recognition Science would cite this to show the selection of θ = 0 is separated by a macroscopic interval rather than a flat minimum. The proof substitutes the exact cosine value, bounds sqrt(2) numerically, and closes with linear arithmetic.
Claim. In the 8-tick phase lattice the J-cost gap satisfies $1 - cos(π/4) > 0.29$.
background
The module treats the strong CP problem as the unexplained smallness of the QCD θ term, which in Recognition Science is forced to discrete multiples of π/4 by the eight-tick octave. The J-cost function J(x) = (x + x^{-1})/2 - 1 measures recognition cost of a phase; its minimum at θ = 0 is separated from the next lattice point θ = π/4 by the gap proved here. Upstream, Constants.tick supplies the fundamental time quantum τ₀ = 1 with one octave equal to eight ticks, while PrimitiveDistinction.from encodes the structural conditions that produce the discrete lattice.
proof idea
The tactic proof first rewrites cos(π/4) to sqrt(2)/2 via the library identity Real.cos_pi_div_four. It then proves sqrt(2) < 1.42 by showing 1.42² > 2 and applying sqrt_lt_sqrt, after which linarith finishes the target inequality.
why it matters
The result supplies the gap_to_next field of strongCPNumericalCert, which certifies that the RS-predicted θ lies inside experimental bounds while remaining separated from the next allowed value. It completes the T7 eight-tick octave step of the forcing chain by turning the structural minimum into a numerically robust gap, as noted in the module doc-comment that J-cost minimization selects θ = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.