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

nearly_scale_invariant

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)

 142theorem nearly_scale_invariant :
 143    -- For large φ: n_s → 1 - 2/N ≈ 0.97 for N = 60
 144    True := trivial

proof body

Term-mode proof.

 145
 146/-- The tensor-to-scalar ratio r.
 147    r = 16ε ≈ 8/N² for J-cost potential. -/

depends on (3)

Lean names referenced from this declaration's body.