module module high

`IndisputableMonolith.QFT.NoetherTheorem`

This module defines symmetries of the J-cost function and the associated conservation laws in the Recognition Science framework. It supplies the abstract core linking continuous symmetries to conserved charges along trajectories. Researchers deriving QFT structures from the J-action would cite it when extending to specific fields. The module consists of layered definitions establishing invariance, group properties, and the central conservation implication.

claimA map $T: X → X$ is a symmetry of the cost function $J$ when $J(Tx) = J(x)$ for all $x ∈ X$. A one-parameter group of such symmetries yields a conserved charge along any trajectory satisfying the cost dynamics.

background

The module imports the fundamental RS time quantum τ₀ = 1 tick and the cost functional J. It introduces the predicate that a transformation leaves J invariant, the notion of a one-parameter group generating continuous symmetries, and the predicate that a quantity remains constant along a trajectory. These notions sit inside the J-action setting of Recognition Science, where the Recognition Composition Law governs how costs combine under scaling and inversion.

proof idea

This is a definition module, no proofs. It assembles basic facts that the identity map is a symmetry, that symmetries compose and invert, that the conservation predicate is equivalent under reparametrization, and that a one-parameter group produces a Noether charge when the action is invariant.

why it matters in Recognition Science

The module supplies the abstract conservation statement that is specialized in the Action.Noether module to the concrete J-action, producing conserved quantities from continuous symmetries. It feeds the broader QFT derivations that obtain quantum field theory fundamentals from the Recognition Science forcing chain. It closes the step from symmetry invariance to charge conservation before any field-specific calculations.

scope and limits

Does not compute explicit charges for any particular field or Lagrangian.
Does not address quantization or operator ordering issues.
Does not treat discrete symmetries or anomalies.
Does not derive the full Noether theorem for arbitrary actions outside the J-cost setting.

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