compactPhase_range
The compact phase function reduces any real log-ratio to a representative in the unit interval. Researchers deriving the GCIC from the forcing chain cite it to guarantee a well-defined Θ₀ shared across vertices at J-cost minimum. The proof is a one-line term proof that unfolds the definition and applies the nonnegativity and strict upper bound of the integer fractional part.
claimFor every real number $r$, the compact phase satisfies $0 ≤ compactPhase(r) < 1$, where compactPhase reduces the log-ratio by the φ-lattice to enforce the discrete gauge identification $r ∼ r + n ln φ$.
background
The module derives Mechanism A of the GCIC Response paper: 8-tick neutrality plus φ-self-similarity forces the discrete gauge $r ∼ r + n ln φ$ (n ∈ ℤ) as a consequence rather than an input. The compact phase is the reduction of any real log-ratio to [0,1) via fractional part, the direct analog of the Brillouin zone obtained from the φ-lattice (T6) and crystal period (T7). Upstream, the 8-tick phase is defined as $kπ/4$ for $k=0..7$ and is periodic with period 2π; the wedge phase is the unimodular complex number $e^{i w}$.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of compactPhase and applies the two standard facts Int.fract_nonneg and Int.fract_lt_one to obtain the pair of inequalities directly.
why it matters in Recognition Science
This theorem supplies the range guarantee required by the parent result gcic_from_forcing_chain, which concludes that J-stationarity forces a single compact phase Θ₀ across all vertices. It closes the T6+T7 step of the forcing chain (T0–T8) by establishing the compact phase in [0,1) without hand-imposed periodicity, completing the discrete gauge derivation in the GCIC gap-A argument.
scope and limits
- Does not derive the explicit definition of compactPhase.
- Does not prove invariance under integer multiples of ln φ.
- Does not link the range to numerical values of α or other constants.
- Does not extend the result to non-real or higher-dimensional arguments.
formal statement (Lean)
159theorem compactPhase_range (r : ℝ) :
160 0 ≤ compactPhase r ∧ compactPhase r < 1 := by
proof body
Term-mode proof.
161 unfold compactPhase
162 exact ⟨Int.fract_nonneg _, Int.fract_lt_one _⟩
163
164/-- Compact phase is invariant modulo integer displacements:
165 compactPhase(r + n·ln φ) = compactPhase(r). -/