module module high

`IndisputableMonolith.QFT.NoetherTheorem`

This module defines symmetries of the J-cost function and states an abstract Noether theorem in the Recognition Science setting. Researchers deriving conserved quantities for QFT from the J-action would cite it. The module consists of definitions establishing invariance under transformations, one-parameter groups, and core conservation statements along trajectories.

claimA map $T: X → X$ is a symmetry of the cost function $J$ when $J(T(x)) = J(x)$ for all $x$. One-parameter groups generate continuous symmetries that yield conserved charges along trajectories in the J-action.

background

The module sits inside the Recognition Science derivation of QFT from the single J-cost functional. It imports the RS time quantum $τ₀ = 1$ tick from Constants and the cost definitions from the Cost module. The supplied doc-comment states that a transformation $T$ on a space $X$ is a symmetry of a function $J$ if $J$ is invariant under $T$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the abstract Noether theorem (noether_core) that Action.Noether specializes to the J-action, producing conserved quantities along trajectories. It feeds the parent QFT module's derivations of quantum field theory fundamentals from Recognition Science and supports the symmetry-conservation step in the overall framework.

scope and limits

Does not derive explicit conserved charges for concrete symmetries.
Does not address quantization of the conserved quantities.
Does not prove the abstract Noether statement from the forcing chain; assumes it as a definition module.

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