lemma other other

`c_pos`

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

formal statement (Lean)

  35lemma c_pos : 0 < c := by unfold c; norm_num

used by (22)

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
c_pos in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
kappa_einstein_pos in IndisputableMonolith.Constants decl_use
c_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
c_pos in IndisputableMonolith.Foundation.ConstantDerivations decl_use
Triangle in IndisputableMonolith.Gravity.ReggeCalculus decl_use
DeLaValleePoussinZeroFreeRegion in IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion decl_use
logZeroFreeStrip_of_deLaValleePoussin in IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion decl_use
LogZeroFreeStrip in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use
riemannZeta_ne_zero_in_log_strip in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use
generated_phase_hit_gives_HitsBalancedPhase in IndisputableMonolith.NumberTheory.SubsetProductPhase decl_use
SubsetProductPhaseHit in IndisputableMonolith.NumberTheory.SubsetProductPhase decl_use
casimir_is_attractive in IndisputableMonolith.QFT.VacuumFluctuations decl_use
temperature_from_surface_gravity in IndisputableMonolith.Quantum.BekensteinHawking decl_use
bh_entropy_positive in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
ConstantsPredictionsCert in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use

depends on (2)

Lean names referenced from this declaration's body.

c_pos in IndisputableMonolith.Constants decl_use
c_pos in IndisputableMonolith.Foundation.ConstantDerivations decl_use