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

defect_at_one

show as:
view Lean formalization →

The theorem establishes that the defect functional vanishes at the unit value. Researchers formalizing the Law of Existence would cite this when verifying that unity meets the zero-cost existence condition. The proof is a direct simplification that reduces the claim using the definitions of defect and the J-cost functional.

claim$J(1) = 0$, where the canonical cost functional is $J(x) = (x + x^{-1})/2 - 1$ and the defect functional coincides with $J$ for positive real arguments.

background

The defect functional is defined by defect(x) := J(x) for x > 0, with J the canonical cost functional J(x) = (x + x^{-1})/2 - 1. This module supplies a literal formalization of the Law of Existence as the equivalence between existence of x and defect(x) = 0. The upstream definition of defect as equal to J supplies the algebraic content used here.

proof idea

The proof is a one-line wrapper that applies the simp tactic with the definitions of defect and J, reducing the statement directly to the algebraic identity at unity.

why it matters in Recognition Science

This base case feeds the complete Law of Existence theorem, the uniqueness of the existent, and the economic inevitability result that unity is the unique minimizer. It supplies the zero-defect anchor for the equivalence Exists x ↔ defect(x) = 0 ↔ x = 1. The result aligns with the J-uniqueness step in the forcing chain.

scope and limits

formal statement (Lean)

  35@[simp] theorem defect_at_one : defect 1 = 0 := by simp [defect, J]

proof body

Term-mode proof.

  36
  37/-- Defect is non-negative for positive arguments. -/

used by (25)

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

depends on (7)

Lean names referenced from this declaration's body.