lemma proved term proof

`lambda_rec_pos`

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

formal statement (Lean)

 427lemma lambda_rec_pos : 0 < lambda_rec := by

proof body

Term-mode proof.

 428  simp [lambda_rec]
 429
 430/-- Newton's gravitational constant G derived from first principles (RS-native form).
 431    \(G = \lambda_{\text{rec}}^2 c^3 / (\pi \hbar)\). -/

used by (4)

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

lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
G_pos in IndisputableMonolith.Constants decl_use
lambda_rec_is_forced in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
minimal_area_eigenvalue in IndisputableMonolith.Quantum.AreaQuantization decl_use

depends on (13)

Lean names referenced from this declaration's body.

lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
G in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
lambda_rec in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use