 156  Int.fract (r / Real.log phi)
 157
 158/-- The compact phase is in [0, 1). -/
 159theorem compactPhase_range (r : ℝ) :
 160    0 ≤ compactPhase r ∧ compactPhase r < 1 := by
 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). -/
 166theorem compactPhase_gauge_invariant (r : ℝ) (n : ℤ) :
 167    compactPhase (r + n * Real.log phi) = compactPhase r := by
 168  unfold compactPhase
 169  have h : (r + n * Real.log phi) / Real.log phi =
 170           r / Real.log phi + n := by
 171    rw [add_div, mul_div_cancel_of_imp (fun h => absurd h log_phi_ne_zero)]
 172  rw [h]
 173  exact Int.fract_add_intCast (r / Real.log phi) n
 174
 175end DiscreteGauge
 176end Papers.GCIC
 177end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.