def definition def or abbrev

`hbar`

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

formal statement (Lean)

  30@[simp] noncomputable def hbar : ℝ := 1.054571817e-34

proof body

Definition body.

  31
  32/-- Gravitational constant (CODATA 2018). -/

used by (40)

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

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
Physical in IndisputableMonolith.Bridge.DataCore decl_use
G in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
hbar_action_identity in IndisputableMonolith.Constants decl_use
hbar_bounds in IndisputableMonolith.Constants decl_use
hbar_eq_phi_inv_fifth in IndisputableMonolith.Constants decl_use
hbar_lt_one in IndisputableMonolith.Constants decl_use
hbar_pos in IndisputableMonolith.Constants decl_use
hbar_positive in IndisputableMonolith.Constants decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
lambda_rec_pos in IndisputableMonolith.Constants decl_use
hbar_ne_zero in IndisputableMonolith.Constants.Codata decl_use
hbar_pos in IndisputableMonolith.Constants.Codata decl_use
GDerivationChain in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_over_ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_SI in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_identity in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_normalized in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
standardInflation in IndisputableMonolith.Cosmology.HorizonProblem decl_use
gaussian_approx_at_eq in IndisputableMonolith.Foundation.PathIntegralDeep decl_use
pathIntegralDeepCert in IndisputableMonolith.Foundation.PathIntegralDeep decl_use
PathIntegralDeepCert in IndisputableMonolith.Foundation.PathIntegralDeep decl_use
path_weight in IndisputableMonolith.Foundation.PathIntegralDeep decl_use
path_weight_max_at_eq in IndisputableMonolith.Foundation.PathIntegralDeep decl_use
path_weight_pos in IndisputableMonolith.Foundation.PathIntegralDeep decl_use

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.

hbar in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use