ThetaQCD
plain-language theorem explainer
The QCD theta parameter is formalized as a real number in the half-open interval from zero to 2 pi. Researchers modeling the strong CP problem inside Recognition Science cite this structure when imposing 8-tick phase constraints on the QCD Lagrangian term. The declaration is a plain structure definition that packages the value with its range predicate and requires no proof steps.
Claim. The QCD theta parameter satisfies $0 ≤ θ < 2π$.
background
The module sets the strong CP problem inside Recognition Science by writing the QCD Lagrangian term as $L_θ = θ (g²/32π²) G_μν G̃^μν$ with θ ranging over [0, 2π). Eight-tick symmetry (T7) forces discrete phase values that are multiples of π/4, after which J-cost minimization selects the zero solution. The single upstream dependency supplies the real-valued spin from the twice-spin definition in the SpinStatistics module.
proof idea
The declaration is a direct structure definition. It introduces a field for the real value together with a predicate enforcing the closed-open interval [0, 2π) and contains no tactics or lemmas.
why it matters
This structure supplies the formal carrier for the theta parameter that later siblings use to prove theta zero minimizes J-cost and that the eight-tick octave selects the CP-preserving point. It directly implements the RS mechanism stated in the module header: discrete phase constraints from T7 plus J-cost selection. No downstream theorems are recorded yet, leaving the link to the full strong-CP resolution open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.