wrapPhase_eq_of_int_diff
plain-language theorem explainer
If two real numbers differ by an integer, their images under the canonical fractional-part projection coincide. Researchers deriving global phase uniqueness on connected recognition lattices cite this to remove integer winding ambiguities after local rigidity is established. The proof rewrites the difference hypothesis via linear arithmetic and invokes the additivity lemma for integer shifts.
Claim. Let $x, y : ℝ$ and $n : ℤ$ satisfy $x - y = n$. Then wrapPhase$(x) = $wrapPhase$(y)$.
background
wrapPhase denotes the canonical fractional-part projection ℝ → [0,1), matching the definition in the Consciousness.GlobalPhase module. The GlobalCoIdentityConstraint module derives the global co-identity constraint from local ingredients: ratio_rigidity_iff (zero ratio cost forces constant positive field on connected graphs) and phase_rigidity (zero reduced phase cost forces integer differences). This theorem supplies the projection that converts those integer differences into equality on the torus ℝ/ℤ.
proof idea
One-line wrapper: linarith converts the hypothesis into the additive equation x = y + n; rewrite substitutes into the goal; exact applies the sibling lemma wrapPhase_add_int y n.
why it matters
This lemma completes the projection step that turns phase_rigidity's integer differences into a single wrapped phase, directly enabling the parent theorem gcic_global_phase_unique. That result states the derived GCIC: on any connected lattice with zero reduced phase cost on every edge, all vertices share one Θ_global ∈ [0,1). It realizes the Anno Recognitionis §V claim that all stable boundaries share one global phase across the universal recognition field, using the phi-ladder and eight-tick octave structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.