pith. sign in
module module high

IndisputableMonolith.Papers.GCIC.DiscreteGauge

show as:
view Lean formalization →

The DiscreteGauge module formalizes the compact phase and discrete gauge that emerge from J-cost convexity and phi self-similarity in the recognition science chain. It defines single-step displacements as integer multiples of ln phi, constructs canonical trajectories, and proves the resulting phase lies in R/Z while remaining gauge invariant under the eight-tick octave. Researchers deriving gauge structure from the T5-T7 forcing sequence cite this module for the compactification step that precedes the GCIC. The module consists of targeted defs,

claimA valid single-step displacement is an integer multiple of $ln phi$, i.e., $t = k ln phi$ for $k in Z$. The induced compact phase satisfies $Theta in R/Z$ and is invariant under the discrete gauge transformations generated by the eight-tick period.

background

The module sits inside the GCIC paper series and imports the J-cost landscape from DiscretenessForcing, where $J(x) = 1/2(x + x^{-1}) - 1$ attains its unique minimum at $x=1$ and appears as the convex bowl $cosh(t)-1$ in log coordinates. PhiForcing supplies the self-similarity argument that forces the golden ratio phi as the fixed point of the discrete ledger. Constants contributes the fundamental time quantum tau_0 = 1 tick. These upstream results are used to define valid displacements and trajectories that close under the eight-tick octave.

proof idea

This is a definition module, no proofs. It declares the valid-step and trajectory predicates, proves the positivity and non-vanishing of ln phi together with the net-zero property of canonical trajectories, and verifies the compact-phase range and gauge invariance by direct algebraic reduction from the imported J-cost and phi-forcing lemmas.

why it matters in Recognition Science

The module supplies the compact phase Theta in R/Z and its gauge invariance that the downstream GCICDerivation requires to reach uniform phase at J-stationarity. It completes the T6+T7 segment of the forcing chain, converting the eight-tick octave into a discrete gauge that enables the Global Co-Identity Constraint without additional empirical input.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (12)