Jmetric_one
plain-language theorem explainer
The lemma shows that the J-metric vanishes at unity. Researchers working with the Recognition Science cost formalism cite it to confirm the zero-distance axiom for the derived metric. The proof is a one-line term simplification that unfolds the square-root definition and applies the unit property of the underlying J-cost.
Claim. Let $J(x) = (x-1)^2/(2x)$. Define the J-metric by $d(x) := sqrt(2 J(x))$. Then $d(1) = 0$.
background
In the Cost module the J-cost is the function $J(x) = (x-1)^2/(2x)$, which satisfies $J(1)=0$ by direct substitution. The J-metric is defined as the square root of twice this cost, producing a quantity that equals the absolute logarithm and therefore functions as a metric. The lemma verifies the zero-distance condition at the identity element, a prerequisite for any distance function in the framework.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of the J-metric as the square root of twice the J-cost and substitutes the already-proved fact that the J-cost vanishes at unity.
why it matters
This result anchors the metric interpretation of the J-cost inside the Recognition Science cost structure. It supplies the zero-distance axiom required by the J-uniqueness property (T5) and the self-similar fixed point (T6) in the forcing chain. Although no immediate downstream uses are recorded, the lemma belongs to the foundational layer supporting later ledger and mechanism-design applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.