theorem proved term proof

`defectDist_self`

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

formal statement (Lean)

 313theorem defectDist_self (x : ℝ) (hx : 0 < x) : defectDist x x = 0 := by

Term-mode proof.

 314  unfold defectDist
 315  rw [div_self (ne_of_gt hx)]
 316  exact J_at_one
 317
 318/-- **PROVED: Defect distance is symmetric.** -/

Lean names referenced from this declaration's body.

defectDist in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_at_one in IndisputableMonolith.Algebra.CostAlgebra decl_use
Defect in IndisputableMonolith.CPM.LNALBridge decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
J_at_one in IndisputableMonolith.Masses.BaselineDerivation decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
J_at_one in IndisputableMonolith.Modal.Possibility decl_use
J_at_one in IndisputableMonolith.QFT.HiggsMechanism decl_use