theorem proved term proof

`omega_lambda_bounds`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 132theorem omega_lambda_bounds : 0 < 11/16 - (alpha / Real.pi) ∧ 11/16 - (alpha / Real.pi) < 11/16 :=

proof body

Term-mode proof.

 133  ⟨omega_lambda_positive, omega_lambda_lt_11_16⟩
 134
 135/-! ## Section P-002: Fermion Mass Hierarchy -/
 136
 137/-- **CALCULATED**: φ^6 bounds: 17 < φ^6 < 18.
 138    Uses φ^6 = (φ^3)^2 = (2φ+1)^2. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

Omega_Lambda_bounds in IndisputableMonolith.Cosmology.CosmologicalConstantDerivation decl_use

depends on (7)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
omega_lambda_lt_11_16 in IndisputableMonolith.Unification.RegistryPredictionsProved decl_use
omega_lambda_positive in IndisputableMonolith.Unification.RegistryPredictionsProved decl_use