gcic_existence_of_global_phase
plain-language theorem explainer
On any connected graph where the reduced phase cost vanishes on every edge for nonzero lambda, there exists a single wrapped phase value in [0,1) shared by all vertices. Recognition physicists cite this when deriving the global co-identity constraint from local rigidity. The proof is a term construction that selects the wrapped phase at the default vertex and invokes uniqueness to match all others.
Claim. Let $V$ be an inhabited type with adjacency relation $adj$ whose reflexive transitive closure connects every pair of vertices. Let $lambda neq 0$ and $Theta : V to mathbb{R}$ satisfy $J_{tilde lambda}(Theta(v) - Theta(w)) = 0$ for all adjacent $v,w$. Then there exists $Theta_{global} in [0,1)$ such that $wrapPhase(Theta(v)) = Theta_{global}$ for every $v in V$.
background
The GlobalCoIdentityConstraint module derives the global co-identity constraint from local rigidity on a recognition lattice. wrapPhase is the canonical fractional-part projection of a real onto [0,1), matching the earlier Consciousness.GlobalPhase definition. The hypothesis hzero encodes vanishing of the reduced phase cost on edges; under connectedness this forces integer phase differences, which wrapPhase then collapses to a common value.
proof idea
This is a term-mode proof. It refines the existential by supplying wrapPhase applied to the phase of the default inhabitant together with the interval bounds from wrapPhase_bounds. The remaining universal goal is discharged by applying the uniqueness lemma gcic_global_phase_unique at the default basepoint and an arbitrary vertex v.
why it matters
The theorem supplies the existence half of the global co-identity constraint and is invoked inside the master certificate gcicCert. It completes the derivation from the local rigidity results in Papers/GCIC/GraphRigidity and Papers/GCIC/ReducedPhasePotential, realizing the statement in the Anno Recognitionis essay that all stable boundaries share one global phase. It closes the local-to-global step while leaving open the explicit link to the phi-ladder or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.