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)

 306noncomputable def hbar : ℝ := cLagLock * tau0

proof body

Definition body.

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_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 in IndisputableMonolith.Constants.Codata 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 (7)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
cLagLock in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use