Jcost_zero_iff_one
The equivalence establishes that J-cost vanishes exactly at unity for positive reals. Modelers of energy-processing bridges in recognition gravity cite it to locate equilibrium states. The proof reduces J(x)=0 to the quadratic (x-1)^2=0 via field simplification followed by linear arithmetic.
claimFor all real $x>0$, let $J(x)=½(x+x^{-1})-1$. Then $J(x)=0$ if and only if $x=1$.
background
J-cost is defined by $J(x)=½(x+x^{-1})-1$ for $x>0$. This functional is the unique cost induced by the Recognition Composition Law. In the EnergyProcessingBridge module the theorem identifies the zero-cost point that equates energy distributions to processing gradients.
proof idea
Constructor splits the biconditional. Forward direction unfolds Jcost to obtain $x+x^{-1}=2$, applies field_simp and nlinarith to reach $(x-1)^2=0$, then concludes $x=1$ by nlinarith. Reverse direction substitutes $x=1$ and simplifies.
why it matters in Recognition Science
The result anchors the zero-cost condition inside the energy_processing_bridge theorem and supplies the key step for ratio_rigidity on connected graphs. It realizes J-uniqueness from the forcing chain (T5) and ensures the identity event is the sole minimum in observer forcing.
scope and limits
- Does not apply for non-positive x.
- Does not bound Jcost away from the minimum.
- Does not treat complex or vector arguments.
- Does not derive non-negativity of Jcost.
Lean usage
example (x : ℝ) (hx : 0 < x) (h : Jcost x = 0) : x = 1 := (Jcost_zero_iff_one x hx).mp hformal statement (Lean)
45theorem Jcost_zero_iff_one (x : ℝ) (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
proof body
Tactic-mode proof.
46 constructor
47 · intro h
48 unfold Jcost at h
49 have : x + x⁻¹ = 2 := by linarith
50 have hx_ne : x ≠ 0 := ne_of_gt hx
51 have : x ^ 2 - 2 * x + 1 = 0 := by
52 field_simp at this ⊢; nlinarith
53 have : (x - 1) ^ 2 = 0 := by nlinarith
54 have : x - 1 = 0 := by nlinarith [sq_nonneg (x - 1)]
55 linarith
56 · intro h; subst h; unfold Jcost; simp
57
58/-- J-cost exact identity: J(1 + ε) = ε²/(2(1+ε)) for ε > -1.
59 This is the bridge between J-cost and the Hamiltonian (kinetic energy ≈ ε²/2). -/