module module high

`IndisputableMonolith.QFT.GaugeInvariance`

The GaugeInvariance module defines ledger states that encode physical reality together with U(1) gauge transformations and physical equivalence. It supplies the basic objects needed for gauge-invariant QFT constructions inside Recognition Science. The module consists entirely of definitions and elementary properties of the equivalence relation and group actions.

claimA ledger state $L$ encodes physical reality. Physical equivalence is an equivalence relation on ledger states. $U(1)$ transformations act on field configurations via global and local gauge maps that preserve the equivalence relation.

background

The module imports the RS time quantum from Constants and the discrete 8-tick cycle from EightTick, whose phases are multiples of π/4. It introduces LedgerState as the object that encodes physical reality and defines physicallyEquivalent as the relation that identifies states related by gauge transformations. U1Transform, FieldConfig, globalGauge and localGauge supply the group action and its local description.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the parent QFT module, which assembles Tier 2 derivations of quantum field theory fundamentals from the Recognition Science framework. It supplies the gauge-invariance layer required before dynamical or spectral results can be stated.

scope and limits

Does not derive equations of motion or propagators.
Does not treat non-Abelian gauge groups.
Does not connect ledger states to specific mass ladders or particle content.
Does not address quantization or path-integral measures.

used by (1)

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

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (26)

structure LedgerState L38
def physicallyEquivalent L45
theorem physical_equiv_refl L49
theorem physical_equiv_symm L57
def U1Transform L83
theorem U1_identity L86
theorem U1_composition L90
theorem U1_inverse L99
def FieldConfig L110
def globalGauge L113
def localGauge L119
def localGaugeDescription L125
structure GaugeField L134
theorem gauge_field_components L138
def transformGaugeField L142
theorem gauge_symmetry_from_redundancy L155
theorem gauge_phase_unobservable L164
def discretePhases L178
theorem eight_tick_span L181
structure NonAbelianLedger L196
def SUN_action L200
def consequences L212
theorem gauge_breaking_masses L223
def smHyperchargeDescription L235
def derivationSummary L248
structure GaugeFalsifier L261