theorem proved wrapper

`nsRS_lt_one`

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

formal statement (Lean)

  40theorem nsRS_lt_one : nsRS < 1 := by

One-line wrapper that applies unfold.

  41  unfold nsRS gap45; norm_num
  42

Lean names referenced from this declaration's body.

nsRS in IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost decl_use