recognition /
Physics /
Physics.CMBTemperature /
explainer
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)
34 def rs_eta : ℝ := 6.1e-10
proof body
Definition body.
35
36 /-! ## Recombination Temperature -/
37
38 /-- **RECOMBINATION TEMPERATURE** from Saha equation.
39 At x_e = 0.5 (50% ionization), the Saha equation gives:
40 k_B T* ≈ E_ion / ln(η⁻¹ × factor) ≈ 0.3 eV ≈ 3500 K
41
42 More precisely, T* ≈ 3000 K (accounting for detailed balance). -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
rs_eta
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_00
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_11
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_22
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_33
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_eq_im_eta
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_offdiag
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
rs_eta_symm
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
depends on (11)
Lean names referenced from this declaration's body.
K
in IndisputableMonolith.Constants
decl_use
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
k_B
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
k_B
in IndisputableMonolith.Quantum.BekensteinHawking
decl_use
k_B
in IndisputableMonolith.Quantum.PageCurve
decl_use
rs_eta
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use
k_B
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use