pith. machine review for the scientific record. sign in
def definition def or abbrev high

comparison

show as:
view Lean formalization →

This definition tabulates the mechanistic contrast between the axion solution and the Recognition Science 8-tick resolution of the strong CP problem. A physicist modeling axion dark matter or testing discrete symmetry constraints would reference the list when comparing continuous relaxation against J-cost selection on the phi-ladder. The body is a direct three-entry list construction that records the shared prediction θ ≈ 0 while distinguishing the underlying structures.

claimThe comparison list is $[(``Axion'', ``Continuous relaxation, new particle''), (``RS'', ``Discrete 8-tick, J-cost selection''), (``Both'', ``Predict θ ≈ 0'')]$, where RS denotes the Recognition Science framework, J-cost is the recognition-event cost derived from the multiplicative recognizer comparator, and θ is the QCD vacuum angle.

background

The module SM-008 derives the strong CP problem from 8-tick symmetry. QCD Lagrangian term θ (g²/32π²) G_μν G̃^μν allows any θ ∈ [0, 2π), yet experiment requires |θ| < 10^{-10}. Recognition Science imposes discrete phase constraints via the eight-tick octave (T7), forcing θ to multiples of π/4 and selecting θ = 0 by J-cost minimization. J-cost is defined as the derived cost of a recognition event (ObserverForcing.cost) or the comparator cost on positive ratios (MultiplicativeRecognizerL4.cost). The tick is the fundamental RS time quantum τ₀ = 1. The Axion structure records a light pseudoscalar with mass ~10^{-6}–10^{-3} eV and decay constant in GeV, produced by misalignment.

proof idea

Direct list definition. The body enumerates the three string pairs without further computation or tactic steps.

why it matters in Recognition Science

The definition anchors the StrongCP module inside the Recognition framework by contrasting the axion mechanism (new particle, continuous relaxation) with the 8-tick J-cost selection that uses only existing structure. It feeds downstream results including w_mass_anomaly_explained, mass_ratio_bounds, proton_electron_ratio_uncertainty, and circuit_lower_bound_topological. It realizes the T7 eight-tick octave landmark for phase quantization and supplies the discrete alternative to the axion solution while preserving the shared prediction θ ≈ 0.

scope and limits

formal statement (Lean)

 172def comparison : List (String × String) := [

proof body

Definition body.

 173  ("Axion", "Continuous relaxation, new particle"),
 174  ("RS", "Discrete 8-tick, J-cost selection"),
 175  ("Both", "Predict θ ≈ 0")
 176]
 177
 178/-- Are RS and axion compatible?
 179
 180    Yes! Even with 8-tick quantization, an axion could exist.
 181    The axion would oscillate around θ = 0 (discrete minimum).
 182    This gives axion dark matter with modified dynamics. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.