def definition def or abbrev

`G`

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

formal statement (Lean)

  33@[simp] noncomputable def G : ℝ := 6.67430e-11

proof body

Definition body.

used by (40)

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

cost_algebra_unique in IndisputableMonolith.Algebra.CostAlgebra decl_use
cost_algebra_unique_aczel in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_defect_form in IndisputableMonolith.Algebra.CostAlgebra decl_use
H_RSZeroParameterStatus in IndisputableMonolith.Astrophysics.MassToLight decl_use
E_coh in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
ml_zero_parameter_certificate in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
BridgeData in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id in IndisputableMonolith.Bridge.DataCore decl_use
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
duhamelRemainderOfGalerkin_integratingFactor in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
AllReachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
IsolationInvariant in IndisputableMonolith.Complexity.SAT.Completeness decl_use
Reachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
G in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
kappa_einstein in IndisputableMonolith.Constants decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
lambda_rec_pos in IndisputableMonolith.Constants decl_use
alpha_seed_structural in IndisputableMonolith.Constants.AlphaDerivation decl_use
G_ne_zero in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
inner_nonneg in IndisputableMonolith.Constants.Derivation decl_use
tau0_planck_relation in IndisputableMonolith.Constants.Derivation decl_use
dimensions_status in IndisputableMonolith.Constants.Dimensions decl_use
dim_G in IndisputableMonolith.Constants.Dimensions decl_use
NA_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use
proton_mass_MeV_pos in IndisputableMonolith.Constants.ExternalAnchors decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use