lemma other other

`G_pos`

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

formal statement (Lean)

  37lemma G_pos : 0 < G := by unfold G; norm_num

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

lambda_rec_dimensionless_id_physical in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
G_pos in IndisputableMonolith.Constants decl_use
kappa_einstein_pos in IndisputableMonolith.Constants decl_use
G_ne_zero in IndisputableMonolith.Constants.Codata decl_use
ell_P_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_over_ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_SI_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_normalized in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
G_pos in IndisputableMonolith.Foundation.ConstantDerivations decl_use
rs_entropy_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
potential_negative in IndisputableMonolith.Gravity.ZeroParameterGravity decl_use
planckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
PlanckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
temperature_from_surface_gravity in IndisputableMonolith.Quantum.BekensteinHawking decl_use
hbar_over_G in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use

Lean names referenced from this declaration's body.