121theorem wrapPhase_eq_of_int_diff (x y : ℝ) (n : ℤ) (h : x - y = (n : ℝ)) : 122 wrapPhase x = wrapPhase y := by
proof body
Tactic-mode proof.
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 152 `Θ v - Θ w ∈ ℤ` for any pair `v, w`) and `wrapPhase_eq_of_int_diff` 153 (which projects out the integer-winding ambiguity onto the torus 154 `ℝ/ℤ`). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.