No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
33theorem nuclear_efficiency_valid :
34 0 < nuclear_efficiency ∧ nuclear_efficiency < 1 := by
proof body
Term-mode proof.
35 norm_num [nuclear_efficiency]
36
37/-- **GAMOW ENERGY**: peak of energy window for nuclear reactions.
38 E_Gamow = (π η_G k_B T)^{2/3} / E_keV
39 The pp chain dominates at T ~ 10⁷ K (solar core temperature). -/
depends on (17)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
K
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
peak
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
k_B
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
nuclear_efficiency
in IndisputableMonolith.Physics.StellarEvolution
decl_use
-
k_B
in IndisputableMonolith.Quantum.BekensteinHawking
decl_use
-
k_B
in IndisputableMonolith.Quantum.PageCurve
decl_use
-
temperature
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
k_B
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use