lemma other other

`hbar_pos`

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

formal statement (Lean)

  36lemma hbar_pos : 0 < hbar := by unfold hbar; norm_num

used by (24)

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
hbar_pos in IndisputableMonolith.Constants decl_use
hbar_positive in IndisputableMonolith.Constants decl_use
hbar_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
alphaG_pred_closed in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
alphaG_pred_eq in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
G_div_hbar in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
planckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
PlanckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
casimir_is_attractive in IndisputableMonolith.QFT.VacuumFluctuations decl_use
vacuum_has_energy in IndisputableMonolith.QFT.VacuumFluctuations decl_use
temperature_from_surface_gravity in IndisputableMonolith.Quantum.BekensteinHawking decl_use
G_hbar_gauss_bonnet in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use
G_over_hbar_phi_tenth in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use
kappa_eq_eight_div_hbar in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use
kappa_per_octave_eq_inv_hbar in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use
octave_duality_witness in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use

depends on (5)

Lean names referenced from this declaration's body.

hbar in IndisputableMonolith.Constants decl_use
hbar_pos in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use