pith. machine review for the scientific record. sign in
def

defect

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LawOfExistence
domain
Foundation
line
32 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LawOfExistence on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  29noncomputable def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  30
  31/-- The defect functional. Equals J for positive x. -/
  32noncomputable def defect (x : ℝ) : ℝ := J x
  33
  34/-- Defect at unity is zero. -/
  35@[simp] theorem defect_at_one : defect 1 = 0 := by simp [defect, J]
  36
  37/-- Defect is non-negative for positive arguments. -/
  38theorem defect_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ defect x := by
  39  simp only [defect, J]
  40  have hx0 : x ≠ 0 := hx.ne'
  41  have h : 0 ≤ (x - 1)^2 / x := by positivity
  42  calc (x + x⁻¹) / 2 - 1 = ((x - 1)^2 / x) / 2 := by field_simp; ring
  43    _ ≥ 0 := by positivity
  44
  45/-! ## The Existence Predicate -/
  46
  47/-- **Existence Predicate**: x exists in the RS framework iff x > 0 and defect(x) = 0. -/
  48structure Exists (x : ℝ) : Prop where
  49  pos : 0 < x
  50  defect_zero : defect x = 0
  51
  52/-- **Defect Collapse Predicate**: Equivalent formulation. -/
  53def DefectCollapse (x : ℝ) : Prop := 0 < x ∧ defect x = 0
  54
  55/-! ## Core Equivalence Theorems -/
  56
  57/-- **Defect Zero Characterization**: defect(x) = 0 ⟺ x = 1 (for x > 0). -/
  58theorem defect_zero_iff_one {x : ℝ} (hx : 0 < x) : defect x = 0 ↔ x = 1 := by
  59  simp only [defect, J]
  60  constructor
  61  · intro h
  62    have hx0 : x ≠ 0 := hx.ne'

papers checked against this theorem (showing 1 of 1)