compactPhase_range
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.