symmetry_at_equilibrium
plain-language theorem explainer
Symmetry of J-cost under inversion holds for every positive real argument. Workers extending Recognition Science to turbulence, disease dynamics, or arbitrage would cite the result to equate paired deviations. The argument is a direct invocation of the underlying Jcost_symm identity from the Cost module.
Claim. For every positive real number $r$, the J-cost satisfies $J(r) = J(r^{-1})$.
background
J-cost quantifies deviation from equilibrium via the Recognition Science functional form $J(x) = (x + x^{-1})/2 - 1$. The module C16 establishes universality of positivity and symmetry for this cost across domains, treating it as the off-equilibrium counterpart to the equilibrium fact Jcost(1) = 0. The upstream lemma Jcost_symm states: for $x > 0$, Jcost x = Jcost x^{-1}, proved by unfolding the definition and applying field simplification and ring normalization.
proof idea
The proof is a one-line wrapper that applies the Jcost_symm lemma from IndisputableMonolith.Cost to the hypothesis hr.
why it matters
This theorem supplies the symmetry half of the C16 universality claim and feeds directly into the jPositivityUniversalityCert definition that aggregates domain-specific costs (turbulent, disease, arbitrage). It rests on the Recognition Composition Law and the phi-forcing chain (T5 J-uniqueness) while remaining agnostic about explicit positivity proofs. The result closes the symmetry component needed before domain specializations can be certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.