symmetry_inv
plain-language theorem explainer
If a bijective map preserves the J-cost on a nonempty space, then its functional inverse preserves the same cost. Workers building the symmetry group for the Recognition Science derivation of Noether's theorem cite this result to close the algebraic structure under inversion. The term proof applies the right-inverse property of the inverse function directly to the invariance equation.
Claim. Let $X$ be a nonempty set, $T: X → X$ a bijective map, and $J: X → ℝ$. If $J(T(x)) = J(x)$ for every $x ∈ X$, then $J(T^{-1}(x)) = J(x)$ for every $x ∈ X$.
background
The QFT module derives Noether's theorem from cost stationarity in Recognition Science. A map T is a symmetry of J precisely when J(T x) equals J x for all x, the definition used here. This supplies the algebraic closure properties needed before conserved charges are extracted along orbits, matching the module's emphasis on ledger balance under symmetry transformations.
proof idea
The term proof introduces an arbitrary point x, pulls the right-inverse identity from surjectivity of T, rewrites the invariance condition at the preimage point, reduces by congruence, and finishes with the inverse property.
why it matters
The result closes the symmetry collection under inversion, a required step before the full group of cost-preserving maps can be used to generate conserved quantities. It sits inside the module's program to obtain Noether's theorem from the J-cost functional rather than from an action principle. In the broader framework this supports the link from continuous symmetries to charges such as energy under time translation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.