compactPhase
The compact phase maps a real log-ratio r to the fractional part of r scaled by 1 over the natural log of φ, yielding a representative in [0,1). Researchers closing the GCIC gap in Recognition Science cite this definition when establishing dynamical equivalence r ~ r + n ln φ from the forcing chain. The definition is a direct one-line wrapper around the fractional-part operator applied to the normalized log-ratio.
claimThe compact phase is defined by $Θ(r) = {r / ln φ}$, where ${·}$ denotes the fractional part and φ is the golden ratio satisfying φ² = φ + 1.
background
In the GCIC module the discrete gauge r ~ r + n ln φ is derived rather than imposed. T6 (φ-step) forces each tick to change the log-ratio by an integer multiple of ln φ; T7 (8-tick neutrality) forces the sum of eight consecutive changes to vanish. The compact phase Θ ∈ ℝ/ℤ therefore encodes the equivalence classes under these shifts. Upstream, EightTick.phase supplies the 8-tick phases kπ/4 and Wedge.phase supplies the unimodular complex phase e^{i w}.
proof idea
This is a one-line wrapper that applies Int.fract to the quotient r / Real.log phi.
why it matters in Recognition Science
The definition supplies the compact phase used by compactPhase_gauge_invariant and compactPhase_range, which in turn feed gcic_from_forcing_chain. That theorem states that J-stationarity on a connected graph forces a single shared Θ₀ at every vertex. It thereby realizes the 8-tick compactification step (T6+T7) and closes the acknowledged gap in the GCIC paper, mirroring Bloch's theorem for the φ-lattice.
scope and limits
- Does not prove gauge invariance under integer shifts.
- Does not derive T6 or T7 from the forcing chain.
- Does not evaluate Θ for concrete physical r values.
- Does not extend the construction beyond one real variable.
Lean usage
theorem example (r : ℝ) (n : ℤ) : compactPhase (r + n * Real.log phi) = compactPhase r := compactPhase_gauge_invariant r nformal statement (Lean)
155noncomputable def compactPhase (r : ℝ) : ℝ :=
proof body
Definition body.
156 Int.fract (r / Real.log phi)
157
158/-- The compact phase is in [0, 1). -/