lemma proved term proof

`planck_time_inner_nonneg`

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

formal statement (Lean)

 166lemma planck_time_inner_nonneg : 0 ≤ hbar_codata * G_codata / c_codata ^ 5 :=

proof body

Term-mode proof.

 167  le_of_lt (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5))
 168
 169/-- **Theorem**: τ₀ = t_P / √π
 170
 171This relation shows τ₀ is the Planck time divided by √π. -/

depends on (10)

Lean names referenced from this declaration's body.

c_codata in IndisputableMonolith.Constants.Derivation decl_use
c_codata_pos in IndisputableMonolith.Constants.Derivation decl_use
G_codata in IndisputableMonolith.Constants.Derivation decl_use
G_codata_pos in IndisputableMonolith.Constants.Derivation decl_use
hbar_codata in IndisputableMonolith.Constants.Derivation decl_use
hbar_codata_pos in IndisputableMonolith.Constants.Derivation decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use