theorem proved term proof

`gammaMassQCD1L_zero`

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

formal statement (Lean)

 143theorem gammaMassQCD1L_zero : gammaMassQCD1L 0 = 0 := by

proof body

Term-mode proof.

 144  simp [gammaMassQCD1L]
 145
 146/-! ## RK4 integrator scaffold with enclosure bounds -/
 147
 148/-- RK4 increment from stage values `(k1,k2,k3,k4)`. -/

depends on (2)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
gammaMassQCD1L in IndisputableMonolith.Physics.RGTransport decl_use