theorem proved term proof

`gr_limit_on`

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

formal statement (Lean)

 149theorem gr_limit_on (inp : ActionInputs) :
 150  S_on inp { alpha := 0, cLag := 0 } = S_EH inp.fst := by

Term-mode proof.

 151  unfold S_on S_total
 152  exact gr_limit_reduces inp.fst inp.snd
 153
 154end ILG
 155end Relativity
 156end IndisputableMonolith

Lean names referenced from this declaration's body.