id_is_symmetry
plain-language theorem explainer
The identity map on any space X leaves an arbitrary real-valued cost function J invariant. Researchers building Noether's theorem from cost stationarity cite this as the trivial base case that initiates symmetry constructions. The proof is a one-line term reduction that invokes the definition of invariance and reflexivity.
Claim. For any set $X$ and function $J: X → ℝ$, the identity map satisfies $J(x) = J(x)$ for all $x ∈ X$.
background
The module derives Noether's theorem from Recognition Science cost stationarity, where a symmetry is any transformation T that leaves the J-cost unchanged and conservation follows from ledger balance under that transformation. The referenced definition states that T is a symmetry of J precisely when J(T x) equals J x for every x. Upstream results include the identity automorphism from CostAlgebra and the Composition axiom, which encodes the Recognition Composition Law forcing multiplicative consistency on the cost functional.
proof idea
The term proof introduces the arbitrary element x and applies reflexivity to obtain the required equality, which holds immediately from the definition of invariance.
why it matters
This base case anchors the symmetry group constructions that feed the core Noether derivation in the same module, where symmetries yield conserved charges such as energy under time translation. It directly supports the ledger-factorization mechanism outlined in the module doc-comment and aligns with the cost axioms that generate the phi-ladder and eight-tick structure in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.