jcost_log_symmetric
plain-language theorem explainer
The theorem establishes that J-cost satisfies J(x) = J(1/x) for every positive real x. Researchers proving uniqueness of the cost minimum or convexity properties in Recognition Science cite this log-ratio symmetry. The proof is a direct one-line term application of the Jcost_symm algebraic identity.
Claim. For every positive real number $x$, $J(x) = J(x^{-1})$, where $J$ denotes the J-cost function on positive ratios.
background
The module ExistenceUniquenessFromCost establishes that the zero set of J-cost on positive reals is exactly the singleton {1}, addressing the pre-Big-Bang claim that existence is not plural. J-cost is the cost of a recognition event, induced either by a multiplicative recognizer comparator or by an observer forcing event, and functions as a semi-metric on the log-ratio scale. The upstream Jcost_symm lemma states: Jcost x = Jcost x⁻¹ by unfolding the squared form, applying field_simp, and closing with ring.
proof idea
The proof is a one-line term wrapper that applies the Jcost_symm lemma from the Cost module directly to the hypothesis 0 < x.
why it matters
This supplies the log_symmetric field inside existenceUniquenessCert, which together with zero_iff_one and isolated certifies a unique cost minimum. It also populates the corresponding field in jConvexityUniversalityCert. The result supports the Recognition Science claim that J acts as a distance on the log-ratio scale and is consistent with the Recognition Composition Law symmetry requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.