wrapPhase_eq_of_int_diff

formal source

 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`.
 135    - The lattice is connected (every pair related by reflexive-transitive
 136      closure of `adj`).
 137    - Each vertex carries a real-valued local phase `Θ : V → ℝ`.
 138    - The GCIC edge condition holds: every adjacent pair has zero reduced
 139      phase cost `Jtilde lam (Θ v - Θ w) = 0` (this is the ratio
 140      energy on phases at base `b = e^lam`).
 141    - The base parameter `lam` is nonzero (the canonical choice is
 142      `lam = ln φ`, where `φ` is the golden ratio).
 143
 144    Then every pair of vertices has the **same wrapped phase**: there is
 145    a single `Θ_global ∈ [0, 1)` independent of the vertex chosen.
 146
 147    This is the Lean-derivable form of the Anno Recognitionis §V statement
 148    "all stable boundaries share one global phase across the universal
 149    recognition field".
 150
 151    The proof is direct composition of `phase_rigidity` (which gives