IndisputableMonolith.Papers.GCIC.DiscreteGauge
The DiscreteGauge module defines the discrete gauge forced by J-cost and phi self-similarity, introducing ValidStep as integer multiples of ln φ along with ValidTrajectory, eight_tick_compactification, and compactPhase. Researchers deriving the GCIC from the RS forcing chain cite it to obtain the compact phase Θ ∈ ℝ/ℤ. The module supplies definitions and short lemmas that connect upstream forcing results to gauge invariance without complex derivations.
claimValidStep(k) holds when the displacement equals k ln φ for integer k; compactPhase lies in ℝ/ℤ and remains invariant under the gauge action induced by the eight-tick octave.
background
The module sits inside the Recognition Science forcing chain. DiscretenessForcing states that J(x) = ½(x + x⁻¹) - 1 has a unique minimum at x = 1 and that J(e^t) = cosh(t) - 1 forms a convex bowl centered at t = 0. PhiForcing shows that self-similarity on a discrete ledger with this J-cost forces the golden ratio φ. Constants supplies the base time quantum τ₀ = 1 tick. Sibling definitions then encode displacements as integer multiples of ln φ and close trajectories under the eight-tick period.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the compact-phase and gauge-invariance objects required by GCICDerivation. That parent derives the Global Co-Identity Constraint from the J-cost chain: T5 yields ratio rigidity, T6+T7 produce the compact phase Θ ∈ ℝ/ℤ (discrete gauge), and their combination forces uniform Θ at J-stationarity.
scope and limits
- Does not derive the GCIC equation itself.
- Does not treat continuous or non-discrete limits.
- Does not compute numerical spectra or coupling values.
- Does not extend beyond the eight-tick octave.
used by (1)
depends on (4)
declarations in this module (12)
-
def
ValidStep -
lemma
log_phi_pos -
lemma
log_phi_ne_zero -
lemma
int_mul_log_phi_valid_step -
structure
ValidTrajectory -
def
canonicalTrajectory -
theorem
canonicalTrajectory_net_zero -
theorem
eight_tick_compactification -
theorem
discrete_gauge_forced -
def
compactPhase -
theorem
compactPhase_range -
theorem
compactPhase_gauge_invariant