rs_V_cb
plain-language theorem explainer
rs_V_cb sets the RS value of the CKM element V_cb to the square of the Cabibbo parameter. Flavor physicists working in the Recognition Science framework cite this when verifying the predicted CKM hierarchy and unitarity. The definition performs a direct algebraic squaring on the upstream cabibbo_parameter.
Claim. The RS-derived CKM matrix element satisfies $V_{cb} := (phi^{-11})^2$, where $phi$ is the golden ratio fixed point and the exponent encodes the torsion difference of 11 between the first two generations.
background
The CKMDerivation module examines whether CKM matrix elements follow from φ-geometry together with the generation torsion schedule {0, 11, 17}. Mixing is attributed to torsion mismatch between up-type and down-type sectors on the Q3 cube. The upstream cabibbo_parameter is defined directly as phi raised to the power negative eleven, matching the torsion difference τ₁ − τ₀ = 11.
proof idea
The declaration is a one-line definition that squares the cabibbo_parameter. It relies only on the upstream definition of cabibbo_parameter as phi to the power negative eleven; no additional lemmas or tactics are required.
why it matters
rs_V_cb feeds the values into CKMCert, which certifies the hierarchy rs_V_ub < rs_V_cb < rs_V_us and the unitarity bound. It advances the module's goal of deriving CKM elements from torsion geometry. The construction uses the self-similar fixed point φ from the T5 J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.