experimentalValues
plain-language theorem explainer
experimentalValues supplies the measured central values and uncertainties for the four CKM matrix elements V_ud, V_us, V_ub, and V_cb. Flavor physicists testing Recognition Science predictions for quark mixing against data would reference this list. The definition is a direct literal enumeration of string-real-real triples with no computation or lemmas applied.
Claim. The experimental values are the list of measured CKM parameters: $V_{ud} = 0.97373(31)$, $V_{us} = 0.2243(8)$, $V_{ub} = 0.00382(20)$, $V_{cb} = 0.0408(14)$.
background
Recognition Science derives the CKM matrix from φ-quantized mixing angles linked to the eight-tick phase structure. The fundamental time quantum is the tick τ₀ = 1. The sibling definitions express the CKM elements in Wolfenstein parametrization: V_ud = 1 - λ²/2, V_us = λ, V_ub = A λ³ (ρ - i η), V_cb = A λ², where λ, A, ρ, η are the standard parameters.
proof idea
This is a direct definition consisting of a literal list of four labeled triples. No lemmas or tactics are invoked; the body enumerates the experimental entries for V_ud, V_us, V_ub, and V_cb exactly as supplied.
why it matters
This definition anchors the CKM module by providing the benchmark data for testing φ-derived angles against observation. It supports the module target of deriving the CKM matrix from RS via φ-quantized mixing and the eight-tick octave, as stated in the module documentation and the associated paper proposition on CKM from golden ratio geometry. The listed hierarchy |V_ub| << |V_cb| << |V_us| supplies the concrete numbers for that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.