triangle_sum
plain-language theorem explainer
The three unitarity angles of the CKM matrix sum to 180 degrees by direct arithmetic on their constant definitions. A particle physicist checking geometric closure of the RS-derived mixing triangle would cite this when confirming consistency with the complex-plane unitarity condition. The proof is a one-line wrapper that unfolds the three angle constants and applies norm_num.
Claim. Let $α$, $β$, and $γ$ be the unitarity angles of the CKM matrix. Then $α + β + γ = 180^°$.
background
The module derives CKM matrix elements from φ-quantized mixing angles tied to the 8-tick phase structure. The unitarity condition on the first row and third column produces a triangle in the complex plane whose interior angles are labeled α, β, γ. The three angle definitions supply the concrete values 85°, 22°, and 73° respectively; the theorem asserts their sum closes the triangle. Upstream results supply the active-edge count A and the actualization operator A, both used to anchor the underlying φ-ladder that motivates the angle choices.
proof idea
The term proof unfolds unitarityAngle_alpha, unitarityAngle_beta, and unitarityAngle_gamma, then invokes norm_num to evaluate the arithmetic sum.
why it matters
The declaration supplies the elementary geometric closure required by any CKM construction inside Recognition Science. It supports the module's target of obtaining the full mixing matrix from φ-angles and the paper proposition on CKM from golden-ratio geometry. It touches the T7 eight-tick octave that supplies the phase quantization but leaves open the derivation of the specific numerical values from the J-cost or defectDist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.