recognition › ask › explain-the-lean-theorem-symmetry-inv-in-module-indisputable-45b9c4df

Explain the Lean theorem `symmetry_inv` in module `IndisputableMonolith.QFT.NoetherTheorem`. Write for an educated reader who knows science and programming but may not know Lean. Cover: (1) what the declaration says in plain English, (2) why it matters in Recognition Science, (3) how to read the formal statement, (4) visible dependencies or certificates in the supplied source, and (5) what this declaration does not prove. Cite only declarations present in the supplied Recognition source.

permalink: https://pith.science/recognition/ask/explain-the-lean-theorem-symmetry-inv-in-module-indisputable-45b9c4df · first asked 2026-05-10 · browse all asks

confidence: high in recognition cached

Explanation of symmetry_inv in IndisputableMonolith.QFT.NoetherTheorem

(1) In plain English, the declaration states that if a transformation T on a nonempty space X is bijective and leaves a real-valued function J unchanged (i.e., J is invariant under T), then the inverse transformation (constructed via Mathlib's invFun) also leaves J unchanged.

(2) In Recognition Science this matters because symmetries of the cost functional J must form a group under composition and inversion. This group structure is a prerequisite for the ledger-balance mechanism that converts cost stationarity into conserved quantities, as developed in the surrounding Noether material.

(3) The formal statement is:

theorem symmetry_inv {X : Type*} [Nonempty X] {T : X → X} {J : X → ℝ}
    (hT : Function.Bijective T) (hsym : IsSymmetryOf T J) :
    IsSymmetryOf (Function.invFun T) J

It takes a bijective map T and a proof that T is a symmetry of J, then returns a proof that the inverse map is also a symmetry. The proof uses the right-inverse property of invFun together with the invariance assumption.

(4) Visible dependencies in the supplied source are the definition IsSymmetryOf (same module) and the helper theorems id_is_symmetry and symmetry_comp, which together establish that symmetries form a group. The proof itself invokes only Mathlib primitives; no external RS theorems are required.

(5) The declaration does not prove the full Noether correspondence (see noether_core), does not construct any concrete physical symmetry (time translation, phase rotation, etc.), and does not derive conservation of any quantity. It only closes the group axioms for the abstract symmetry relation.

cited recognition theorems

NoetherTheorem.symmetry_inv The theorem whose explanation is requested; its statement and proof are the direct source material.
NoetherTheorem.id_is_symmetry Complementary theorem establishing the identity as a symmetry, used to show the symmetry relation forms a group.
NoetherTheorem.symmetry_comp Complementary theorem showing closure under composition, completing the group structure with symmetry_inv.
NoetherTheorem.noether_core Downstream theorem that applies the symmetry group (including inverses) to obtain conservation from cost invariance.

outside recognition

Aspects Recognition does not yet address:

Any explicit embedding of this abstract symmetry group into the J-cost functional or the Recognition Forcing chain from other modules.
Concrete physical examples (time translation, U(1) phase) are present in the module but are not proved to arise from the RS ledger axioms.

recognition modules consulted

The Recognition library is at github.com/jonwashburn/shape-of-logic. The model is restricted to the supplied Lean source and instructed not to invent theorem names. Treat output as a starting point, not a verified proof.