def definition def or abbrev

`defectDist`

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

Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput

generate prose now

formal statement (Lean)

 310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)

proof body

Definition body.

 311
 312/-- **PROVED: Defect distance is zero at identity.** -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

defectDist_le_J_of_ratio_bounds in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_no_global_quasi_triangle in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_nonneg in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_quasi_triangle_local in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_self in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_symm in IndisputableMonolith.Algebra.CostAlgebra decl_use

depends on (7)

Lean names referenced from this declaration's body.

Defect in IndisputableMonolith.CPM.LNALBridge decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use