pith. machine review for the scientific record. sign in
theorem proved tactic proof high

defect_nonneg

show as:
view Lean formalization →

Defect(x) is non-negative for every positive real x. Researchers citing the discreteness forcing principle or economic inevitability theorems in Recognition Science invoke this result to establish the cost lower bound. The proof unfolds the defect definition, rewrites the expression as a scaled square term via field simplification, and concludes non-negativity by direct positivity.

claim$J(x) = J(x) = 0$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.

background

Defect is the J-cost functional restricted to positive reals, with upstream definition defect x := J x where J(x) = (x + x^{-1})/2 - 1. The module formalizes the Law of Existence as the equivalence between existence and zero defect, with key results including defect zero iff x equals one and the unique minimizer at unity. The and theorem from CirclePhaseLift supplies angular bounds in related contexts but is not required for this non-negativity step.

proof idea

The tactic proof first simplifies defect and J by definition, introduces the auxiliary fact that x is nonzero, establishes non-negativity of (x-1)^2 / x by positivity, then applies a calc block to equate the original expression to half that term and finishes with positivity.

why it matters in Recognition Science

This supplies the non-negativity clause required by the discreteness forcing principle, which uses it to show J forces discrete ontology through its unique minimum at x=1. It is also invoked directly in economic_inevitability, total_defect_nonneg, zero_defect_iff_unity, and nonunity_positive_entropy. The result anchors the J-uniqueness step (T5) in the forcing chain and the cost non-negativity that drives the eight-tick octave and D=3 emergence.

scope and limits

Lean usage

exact LawOfExistence.defect_nonneg (c.entries_pos i)

formal statement (Lean)

  38theorem defect_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ defect x := by

proof body

Tactic-mode proof.

  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. -/

used by (26)

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

depends on (2)

Lean names referenced from this declaration's body.