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

J_defect_form

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  79theorem J_defect_form (x : ℝ) (hx : x ≠ 0) : J x = (x - 1) ^ 2 / (2 * x) :=

proof body

Term-mode proof.

  80  Jcost_eq_sq hx
  81
  82/-! ## §2. The Recognition Composition Law (RCL) -/
  83
  84/-- The **Recognition Composition Law**: the ONE primitive of Recognition Science.
  85
  86    J(xy) + J(x/y) = 2·J(x)·J(y) + 2·J(x) + 2·J(y)
  87
  88    In the log-coordinate form (t = ln x, u = ln y), this becomes:
  89    G(t+u) + G(t−u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
  90
  91    which is a calibrated multiplicative form of the d'Alembert functional equation. -/

depends on (17)

Lean names referenced from this declaration's body.