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)
250theorem rho_bar_interval : (0.10 : ℝ) < wolfenstein_rho ∧ wolfenstein_rho < 0.20 := by
proof body
Term-mode proof.
251 unfold wolfenstein_rho; constructor <;> norm_num
252
253/-- The unitarity constraint ρ̄² + η̄² < 1 holds (required for V unitary). -/
depends on (6)
Lean names referenced from this declaration's body.
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
required
in IndisputableMonolith.Foundation.DomainBootstrap
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use
-
wolfenstein_rho
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use