pith. machine review for the scientific record. sign in
theorem proved term proof

rar_power_law_emergence

show as:
view Lean formalization →

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)

 101theorem rar_power_law_emergence
 102    (a₀ a_baryon α : ℝ) (ha0 : 0 < a₀) (ha : 0 < a_baryon) :
 103    (a₀ / a_baryon) ^ (α / 2) * a_baryon = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by

proof body

Term-mode proof.

 104  simpa [a_obs_ilg, w_accel] using (rar_power_law a₀ a_baryon α ha0 ha)
 105
 106/-- Alias for the main RAR emergence statement, kept for stable downstream references. -/

depends on (7)

Lean names referenced from this declaration's body.