lemma proved term proof

`actionJ_const_one`

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

formal statement (Lean)

  83lemma actionJ_const_one {a b : ℝ} :
  84    actionJ (AdmissiblePath.const a b 1 one_pos) = 0 := by

proof body

Term-mode proof.

  85  unfold actionJ
  86  simp [AdmissiblePath.const_apply, Jcost_unit0]
  87
  88/-! ## Fixed endpoints -/
  89
  90/-- Two admissible paths share endpoints. -/

depends on (7)

Lean names referenced from this declaration's body.

actionJ in IndisputableMonolith.Action.PathSpace decl_use
AdmissiblePath in IndisputableMonolith.Action.PathSpace decl_use
const in IndisputableMonolith.Action.PathSpace decl_use
const_apply in IndisputableMonolith.Action.PathSpace decl_use
Jcost_unit0 in IndisputableMonolith.Cost decl_use
Jcost_unit0 in IndisputableMonolith.Cost.JcostCore decl_use
admissible in IndisputableMonolith.Information.Thermodynamics decl_use