ckm_hierarchy
plain-language theorem explainer
Recognition Science derives the strict ordering of CKM matrix elements |V_ub| < |V_cb| < |V_us| from the phi-ladder and the torsion schedule on the Q3 cube. Flavor physicists comparing RS predictions to PDG mixing data would cite the result. The proof unfolds the three RS element definitions, invokes cabibbo_parameter_pos, bounds the parameter in (0,1) via one_lt_phi and power rewriting, then closes both inequalities with nlinarith.
Claim. The RS-derived CKM matrix elements satisfy $ |V_{ub}| < |V_{cb}| < |V_{us}| $, where each element is obtained from the torsion differences on the Q_3 cube via powers of the golden ratio.
background
The module derives CKM elements from torsion mismatch between up-type and down-type sectors on the Q3 cube. The Cabibbo angle satisfies sin(θ_C) ≈ φ^{-11} with the generation torsion schedule {0,11,17}. Upstream, one_lt_phi supplies the lemma 1 < φ that bounds the Cabibbo parameter below unity. Related definitions include the inflaton potential V(φ_inf) = Jcost(1 + φ_inf) and the binary-cube vertex count V(D) = 2^D from SpectralEmergence.
proof idea
The tactic proof first unfolds rs_V_ub, rs_V_cb and rs_V_us. It obtains hc := cabibbo_parameter_pos, then proves cabibbo_parameter < 1 by rewriting zpow_neg and zpow_natCast and applying inv_lt_one_of_one_lt with nlinarith on one_lt_phi together with the identity phi^11 = phi^8 * phi^3. The constructor splits the conjunction; each conjunct is discharged by nlinarith using sq_nonneg cabibbo_parameter.
why it matters
The theorem supplies the hierarchy field to ckm_cert_exists, which constructs a nonempty CKMCert containing hierarchy, unitarity_bound and torsion_structure. It directly answers the module question of deriving the CKM matrix from φ-geometry and the {0,11,17} torsion schedule. In the broader framework the result rests on the phi fixed point (T6) and the eight-tick octave (T7) that generate the rung ladder used for the mass and mixing formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.