def
definition
compactPhase
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Papers.GCIC.DiscreteGauge on GitHub at line 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
152/-! ## Corollary: compact phase is well-defined -/
153
154/-- The compact phase Θ = r / (ln φ) mod 1. -/
155noncomputable def compactPhase (r : ℝ) : ℝ :=
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