No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
154theorem mixingAngles_geometric_origin :
155 (1 : ℕ) / edgeDualCount = 1 / 24 ∧
156 cabibboProjection = -3 := by
proof body
Term-mode proof.
157 constructor <;> rfl
158
159/-!
160### Numeric Approximations
161
1621. **V_cb ≈ 0.0417**: (1/24) matches the V_cb observation.
1632. **φ⁻³ ≈ 0.236**: Golden projection part of the Cabibbo angle.
164-/
165
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
V_cb
in IndisputableMonolith.Physics.CKM
decl_use
-
cabibboProjection
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
edgeDualCount
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
V_cb
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use