def definition def or abbrev

`tensor_to_scalar`

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

formal statement (Lean)

  52noncomputable def tensor_to_scalar (N : ℝ) : ℝ := 12 * alpha_attractor / N ^ 2

Definition body.

  53
  54/-- For N = 55 e-foldings: r ≈ 12 * 2.618 / 3025 ≈ 0.0104. -/

From the project-wide theorem graph. These declarations reference this one in their body.

tensor_to_scalar in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
r_at_55_bounds in IndisputableMonolith.Gravity.Inflation decl_use
r_in_detectable_range in IndisputableMonolith.Gravity.Inflation decl_use
r_from_jcost in IndisputableMonolith.Gravity.JCostInflaton decl_use

Lean names referenced from this declaration's body.

tensor_to_scalar in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
alpha_attractor in IndisputableMonolith.Gravity.Inflation decl_use