wrapPhase

formal source

 101    `Consciousness.GlobalPhase.frac`; we re-state it locally to avoid
 102    introducing a Consciousness import cycle (this module sits in
 103    Foundation and feeds the Consciousness layer, not the other way). -/
 104def wrapPhase (x : ℝ) : ℝ := x - Int.floor x
 105
 106/-- Wrapped phase is in `[0, 1)`. -/
 107theorem wrapPhase_bounds (x : ℝ) : 0 ≤ wrapPhase x ∧ wrapPhase x < 1 := by
 108  refine ⟨?_, ?_⟩
 109  · have := Int.floor_le x; unfold wrapPhase; linarith
 110  · have := Int.lt_floor_add_one x; unfold wrapPhase; linarith
 111
 112/-- Wrapped phase is invariant under shifts by integers. -/
 113theorem wrapPhase_add_int (x : ℝ) (n : ℤ) :
 114    wrapPhase (x + (n : ℝ)) = wrapPhase x := by
 115  unfold wrapPhase
 116  rw [Int.floor_add_intCast]
 117  push_cast
 118  ring
 119
 120/-- If two reals differ by an integer, they wrap to the same value. -/
 121theorem wrapPhase_eq_of_int_diff (x y : ℝ) (n : ℤ) (h : x - y = (n : ℝ)) :
 122    wrapPhase x = wrapPhase y := by
 123  have hx : x = y + (n : ℝ) := by linarith
 124  rw [hx]
 125  exact wrapPhase_add_int y n
 126
 127/-! ## §2. The headline theorem: global phase uniqueness -/
 128
 129variable {V : Type*}
 130
 131/-- **THE GLOBAL CO-IDENTITY CONSTRAINT (derived form).**
 132
 133    Suppose:
 134    - The recognition lattice has vertex type `V` with adjacency `adj`.