thetaContributions
plain-language theorem explainer
The declaration enumerates the three sources that sum to the effective QCD theta parameter under Recognition Science. A physicist modeling axion dynamics or discrete symmetry constraints on the strong CP problem would cite this list when decomposing theta_eff. It is assembled by direct enumeration of the bare topological term, the quark-mass phase contribution, and their total.
Claim. The effective strong-CP phase is the sum of the bare topological angle and the phase of the quark-mass determinant: $theta_eff = theta_QCD + arg det M_q$.
background
The module treats the strong CP problem as arising from the topological term $L_theta = theta (g^2/32 pi^2) G_mu nu tilde G^mu nu$ whose angle theta can lie anywhere in [0,2pi) yet satisfies the experimental bound |theta|<10^{-10}. Recognition Science replaces the fine-tuning puzzle with 8-tick symmetry: phases are restricted to multiples of pi/4 and J-cost minimization on the phi-ladder selects theta=0. Upstream, the EightTick.phase definition supplies the discrete phases k pi/4 for k in Fin 8, while the Axion structure encodes the dynamical relaxation mechanism with mass ~10^{-6} to 10^{-3} eV.
proof idea
One-line definition that directly constructs the three-element list of string descriptions for the theta contributions.
why it matters
This definition supplies the decomposition required by the 8-tick resolution of the strong CP problem (SM-008). It precedes the axion solution and the theta_zero_selected claim that J-cost minimization forces theta=0. The relevant framework landmark is the eight-tick octave (T7) that imposes discrete phase constraints, converting the continuous fine-tuning issue into a symmetry selection on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.