gcic_global_phase_unique
plain-language theorem explainer
If a connected recognition lattice carries a phase field Θ such that every adjacent pair satisfies vanishing reduced phase cost Jtilde lam (ΔΘ) at nonzero lam, then wrapPhase(Θ v) equals wrapPhase(Θ w) for every pair of vertices. Recognition physicists cite this as the derived uniqueness half of the global co-identity constraint in Anno Recognitionis §V. The proof first extracts an integer winding via phase_rigidity on the connected graph and then projects onto the torus with wrapPhase_eq_of_int_diff.
Claim. Let $G=(V,adj)$ be connected, meaning the reflexive-transitive closure of $adj$ relates every pair of vertices. For nonzero base parameter $λ∈ℝ$ and phase assignment $Θ:V→ℝ$ satisfying $Jtilde(λ,Θ(v)−Θ(w))=0$ on every edge, it follows that $wrapPhase(Θ(v))=wrapPhase(Θ(w))$ for all $v,w∈V$, where $wrapPhase(x)=x−⌊x⌋$.
background
The module derives the global co-identity constraint from local graph rigidity. wrapPhase is the canonical projection ℝ→[0,1) given by wrapPhase x = x − floor x. The edge condition hzero encodes vanishing of the reduced phase potential Jtilde lam on adjacent phase differences. Upstream, phase_rigidity (from ReducedPhasePotential) establishes that zero reduced cost on a connected graph forces all phase differences to be integers. The local theoretical setting is the GCIC derivation arc that obtains global phase uniqueness by composing integer rigidity with torus projection.
proof idea
The term-mode proof is a direct two-step composition. First apply phase_rigidity to the connectedness hypothesis, the nonzero lam condition, and the zero-cost edge condition to obtain an integer n with Θ v − Θ w = n. Then invoke wrapPhase_eq_of_int_diff on that integer difference to conclude the wrapped phases agree.
why it matters
This theorem supplies the uniqueness statement that feeds gcic_canonical (the canonical lam = ln φ instance), gcicCert, gcic_existence_of_global_phase, and gcic_one_statement. It completes the Lean derivation of the Anno Recognitionis §V claim that all stable boundaries share one global phase across the recognition field. In the broader framework it realizes the global phase invariance implied by the J-cost functional equation and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.