jcost_reciprocal
plain-language theorem explainer
The declaration establishes that the J-cost satisfies J(x) = J(1/x) for every positive real x. Workers on the F1 foundation paper or on geometric-mean optimality in Recognition Science cite this reciprocity when analyzing inversion-invariant costs in descent or bond problems. The proof is a one-line wrapper that invokes the core symmetry lemma Jcost_symm already proved in the Cost module.
Claim. Let $J(y) := ½(y + y^{-1}) - 1$. Then for every real $x > 0$, $J(x) = J(x^{-1})$.
background
The module F1 — Log-Domain J-Cost Geometry collects identities for the canonical cost $J(x) = ½(x + x^{-1}) - 1$ and its log-domain geometry. This setting is required by the foundation paper for geometric-mean optimality and the distinction between simultaneous and sequential descent. The upstream lemma Jcost_symm states: lemma Jcost_symm {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹, proved by unfolding the definition and applying field_simp and ring.
proof idea
One-line wrapper that applies the symmetry lemma Jcost_symm from the Cost module (and its duplicate in JcostCore) directly to the hypothesis hx : 0 < x.
why it matters
Labeled F1.1.4 in the foundation paper, the identity anchors the log-domain symmetry used by the module's main results on geometric-mean minimization and simultaneous versus sequential descent. It is cited by the NS, P vs NP, Yang-Mills, and RH (frustrated phase) arguments listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.