log_space_symmetry
plain-language theorem explainer
The declaration shows that the J-cost remains unchanged when its argument is replaced by its reciprocal for any positive real. Cosmologists deriving the forced form of the cost function from scale-invariance selection in pre-Big-Bang cosmology cite this symmetry. The proof reduces immediately to the core Jcost symmetry lemma already established in the Cost module.
Claim. For every positive real number $x$, the J-cost satisfies $J(x) = J(x^{-1})$.
background
The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, which satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This module formalizes selection of scale-invariant cost functions in the pre-Big-Bang setting, where naive scale invariance $J(cx) = J(x)$ fails but the ratio is bounded by the cost of the scale change itself. The upstream Jcost_symm lemma establishes the inversion symmetry directly from the definition by algebraic simplification and field simplification.
proof idea
One-line wrapper that applies the Jcost_symm lemma from the Cost module.
why it matters
This symmetry is a structural fact used in proving the uniqueness of J under the Recognition Composition Law and the forcing chain to three spatial dimensions. It supports the claim in the pre-Big-Bang paper that only the hyperbolic form of J survives cost minimization. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.