experimentalTests
plain-language theorem explainer
The declaration enumerates three experimental routes to test the Recognition Science resolution of the strong CP problem. A QCD phenomenologist or axion experimentalist would cite the list when planning neutron EDM upgrades or lattice runs. The definition simply assembles a fixed list of strings following the same pattern used in the ThreeGenerations and quantum modules.
Claim. The experimental tests for the eight-tick resolution of the strong CP problem consist of axion searches (ADMX, HAYSTAC and similar), improvements to the neutron electric dipole moment bound, and lattice QCD evaluations of the theta parameter.
background
The module sets the strong CP problem in the Recognition Science setting: the QCD Lagrangian term theta times the topological density is restricted by eight-tick symmetry to discrete values pi k /4, after which the J-cost function selects theta exactly zero. The upstream tick definition supplies the fundamental time quantum tau_0 = 1 in RS-native units, while the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost that performs the selection. The Axion structure records the alternative dynamical solution with mass in the 10^{-6} to 10^{-3} eV window.
proof idea
The declaration is a direct list construction. It mirrors the experimentalTests definitions in ThreeGenerations, EntanglementEntropy and NonlocalityNoSignaling, each of which returns a List String of test descriptions without further computation.
why it matters
The list supplies the concrete observational consequences of the eight-tick mechanism (T7) that solves the strong CP problem without new particles. It is referenced by the corresponding experimentalTests declarations in the ThreeGenerations, EntanglementEntropy and NonlocalityNoSignaling modules. The module doc-comment states that RS predicts theta = 0 exactly and remains compatible with axions, with neutron EDM improvement beyond 10^{-10} serving as the decisive discriminator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.