pith. machine review for the scientific record. sign in
theorem proved term proof high

triangle_sum

show as:
view Lean formalization →

Unitarity triangle angles α, β, γ in the CKM matrix sum to exactly 180 degrees from their assigned numerical values. Flavor physicists checking CP-violation consistency would cite this when validating Recognition Science quark-mixing derivations. The proof is a direct term reduction that unfolds the three constant definitions and applies numerical normalization to the arithmetic sum.

claim$α + β + γ = 180^∘$, where α, β, γ are the angles of the unitarity triangle formed by the rows of the CKM matrix.

background

The module constructs the CKM matrix from φ-quantized mixing angles that arise from the eight-tick phase structure. Unitarity of the 3×3 matrix produces a closed triangle in the complex plane whose interior angles must sum to 180°. Upstream results supply the active-edge count A (IntegrationGap and Masses.Anchor) and the actualization operator A (Modal.Actualization) that underwrite the coherence assumptions used to assign the angle values.

proof idea

The term proof unfolds unitarityAngle_alpha, unitarityAngle_beta, and unitarityAngle_gamma, then applies norm_num to verify the numerical identity 85 + 22 + 73 = 180.

why it matters in Recognition Science

The declaration confirms geometric closure of the CKM unitarity triangle inside the Recognition Science treatment of quark flavor mixing. It directly supports the module target of deriving the matrix from golden-ratio geometry and aligns with the T7 eight-tick octave in the unified forcing chain. The embedded comment sketches φ-based predictions for λ, A, and η/ρ, marking an open verification path against measured CKM parameters.

scope and limits

formal statement (Lean)

 196theorem triangle_sum :
 197    unitarityAngle_alpha + unitarityAngle_beta + unitarityAngle_gamma = 180 := by

proof body

Term-mode proof.

 198  unfold unitarityAngle_alpha unitarityAngle_beta unitarityAngle_gamma
 199  norm_num
 200
 201/-! ## φ-Predictions for CKM -/
 202
 203/-- RS predictions for CKM parameters:
 204
 205    1. λ ≈ (φ - 1)² / φ ≈ 0.236 (vs observed 0.227)
 206    2. A ≈ related to φ
 207    3. η/ρ ≈ φ (possible?)
 208    4. Unitarity triangle angles ≈ φ-related
 209
 210    These would be profound if verified! -/

depends on (7)

Lean names referenced from this declaration's body.