module module high

`IndisputableMonolith.QFT.NoetherTheorem`

The QFT.NoetherTheorem module defines symmetries of the J-cost function and states the abstract Noether theorem for one-parameter groups. Researchers deriving conservation laws from the Recognition Science J-action cite it as the source of noether_core. The module consists of basic invariance definitions followed by the core conservation statement.

claimA transformation $T$ on a space $X$ is a symmetry of a function $J$ if $J$ is invariant under $T$, i.e., $J(T(x)) = J(x)$ for all $x$. For a one-parameter group of such symmetries the associated Noether charge is conserved along trajectories.

background

The module sits in the QFT domain and imports Constants (where the RS time quantum satisfies $ au_0 = 1$ tick) together with the Cost module that supplies the J-cost function. It introduces IsSymmetryOf to express invariance of J, OneParamGroup to encode continuous symmetries, and IsConservedAlong to capture the resulting conservation statements. The local setting is the abstract Noether framework that precedes specialization to the J-action.

proof idea

This is a definition module, no proofs. It assembles the supporting lemmas id_is_symmetry, symmetry_comp and symmetry_inv, then states the core result noether_core that links one-parameter symmetry groups to conserved charges.

why it matters in Recognition Science

The module supplies the abstract noether_core that IndisputableMonolith.Action.Noether specializes to the cost-functional setting, producing conserved quantities from continuous symmetries of the J-action. It also supports the QFT derivations collected in IndisputableMonolith.QFT. This step closes the abstract symmetry-to-conservation link in the Recognition Science chain.

scope and limits

Does not specialize the theorem to the J-action (handled in Action.Noether).
Does not derive explicit charges for particular fields or Lagrangians.
Does not address quantum corrections or operator ordering.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Action.Noether module_import
IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (25)

def IsSymmetryOf L46
theorem id_is_symmetry L50
theorem symmetry_comp L55
theorem symmetry_inv L62
def IsConservedAlong L74
def IsConservedAlong' L78
theorem conserved_iff_conserved' L82
structure OneParamGroup L99
theorem noether_core L111
def NoetherCharge L118
theorem invariant_is_noether_charge L122
def TimeTranslation L130
theorem time_invariance_implies_conservation L137
def SpaceTranslation L145
theorem space_invariance_implies_conservation L152
def PhaseRotation L160
theorem phase_invariance_implies_conservation L171
structure PhasePoint L179
def harmonicEnergy L184
def harmonicFlow L188
theorem harmonic_energy_conserved L198
theorem noether_summary L242
def standardModelConservation L250
structure NoetherFalsifier L271
def apparentViolations L278