Jcost_zero_iff_one
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.