theorem proved term proof

`phi_inv3_upper_bound`

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

formal statement (Lean)

 153theorem phi_inv3_upper_bound : phi ^ (-3 : ℤ) < (0.2361 : ℝ) :=

proof body

Term-mode proof.

 154  Numerics.phi_inv3_zpow_bounds.2
 155
 156/-- V_us matches within 1 sigma.
 157
 158    V_us_pred = φ^(-3) - (3/2)*α
 159              ≈ 0.2360679 - 0.01095
 160              ≈ 0.2251
 161    V_us_exp = 0.22500
 162    |V_us_pred - V_us_exp| ≈ 0.0001 < 0.00067 ✓
 163
 164    Proof: From bounds on φ^(-3) and α, we establish the match. -/

used by (2)

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

V_us_match in IndisputableMonolith.Physics.CKMGeometry decl_use
jarlskog_match in IndisputableMonolith.Physics.MixingDerivation decl_use

depends on (8)

Lean names referenced from this declaration's body.

sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
sigma in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
phi_inv3_zpow_bounds in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
V_us in IndisputableMonolith.Physics.CKM decl_use
V_us_exp in IndisputableMonolith.Physics.CKMGeometry decl_use
V_us_pred in IndisputableMonolith.Physics.CKMGeometry decl_use
V_us in IndisputableMonolith.StandardModel.CKMMatrix decl_use