bestCabibboFit
plain-language theorem explainer
The definition supplies the numerical value for the leading Cabibbo angle parameter in the CKM matrix as hypothesis6, identified in the module comment with the golden-ratio expression (φ-1)^2/φ ≈ 0.236. Quark-mixing modelers would cite the entry when inserting RS-derived inputs into weak-decay calculations or Wolfenstein parametrizations. The body is a direct one-line assignment with no further reduction steps.
Claim. The best-fit Cabibbo angle is the real number given by hypothesis6, which the module equates to the expression $((φ-1)^2)/φ ≈ 0.236$ where $φ$ is the self-similar fixed point of the forcing chain.
background
The module derives CKM matrix elements from φ-quantized mixing angles that arise inside the eight-tick phase structure. Generations are assigned to adjacent sectors whose phase separations fix the mixing angles; the phase map itself is defined by kπ/4 for k in Fin 8 and is periodic with period 2π. Upstream constants supply the fundamental tick τ₀ = 1 and the ledger factorization that calibrates the J-cost function used to obtain φ itself.
proof idea
The declaration is a one-line definition that binds bestCabibboFit directly to hypothesis6. No tactics or lemmas are applied inside the body; the surrounding comment block supplies the physical reading by linking the value to the three-generation phase sectors.
why it matters
The entry anchors the Cabibbo angle inside the CKM construction that the module presents as SM-012. It realizes the eight-tick octave (T7) and the φ fixed point (T6) at the level of a concrete numerical prediction, feeding the sibling definitions of the Wolfenstein parameters and the individual matrix elements V_us, V_ud. The definition leaves open the discharge of hypothesis6 by a proved theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.