ckmlambdaCert
plain-language theorem explainer
The definition constructs a certificate assembling the Wolfenstein A value of exactly 9/11, its membership in the PDG uncertainty interval around 0.826, the identity phi cubed equals 2 phi plus 1, and the Cabibbo proxy angle lying inside the interval (0.225, 0.240). A physicist deriving CKM parameters from the phi ladder would cite it to record that the golden-ratio fixed point reproduces the leading Wolfenstein hierarchy within experimental bounds. The construction is a direct field-by-field record of four prior theorems into the target record
Claim. Let $A$ denote the Wolfenstein parameter and let $c$ denote the Cabibbo proxy. The certificate $C$ satisfies $A = 9/11$, $|A - 0.826| < 0.013$, $phi^3 = 2 phi + 1$, and $0.225 < c < 0.240$.
background
The module formalizes the Wolfenstein parameterization of the CKM matrix inside Recognition Science. The structure CKMLambdaCert packages four statements: the exact value $A = 9/11$ obtained from the cube-derived gauge coupling, the numerical check that this value lies inside the PDG 1-sigma band, the algebraic identity $phi^3 = 2 phi + 1$ that follows from the minimal polynomial of the golden ratio, and the interval membership for the Cabibbo proxy $c = 1/phi^3$ that contains the measured sin(theta_C). Upstream, wolfensteinA_val supplies the equality by reflexivity, wolfensteinA_in_pdg_band performs the norm_num comparison, phi3_eq reduces the cubic via the square identity, and cabibbo_in_band unfolds the proxy and invokes the rational bounds on phi.
proof idea
The definition is a direct record constructor. It assigns the four fields of CKMLambdaCert by naming the sibling theorems wolfensteinA_val, wolfensteinA_in_pdg_band, phi3_eq, and cabibbo_in_band respectively.
why it matters
The certificate records the Recognition Science prediction that the Wolfenstein A parameter equals the rational 9/11 derived from the cube gauge construction and that the Cabibbo angle proxy 1/phi^3 falls inside the PDG window. It therefore supplies a concrete link between the phi-ladder fixed point (T6) and the observed quark mixing hierarchy. No downstream theorems yet consume the certificate, leaving open its integration into a full CKM matrix formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.