gcic_one_statement
plain-language theorem explainer
Researchers deriving global phase coherence from local rigidity in recognition lattices cite this theorem as the compact one-statement form of the Global Co-Identity Constraint. It asserts that connectedness plus vanishing reduced phase cost Jtilde(lam, ΔΘ) = 0 on edges forces all wrapped phases to coincide in [0,1). The proof is a one-line wrapper that applies the prior uniqueness result for integer windings and the standard bounds on the fractional-part map.
Claim. Let $(V, E)$ be a connected graph with adjacency relation adj. Let $λ ∈ ℝ$ be nonzero and let $Θ : V → ℝ$ satisfy $Jtilde(λ, Θ(v) - Θ(w)) = 0$ for every adjacent pair. Then wrapPhase(Θ(v)) = wrapPhase(Θ(w)) for all $v, w ∈ V$, and $0 ≤ wrapPhase(Θ(v)) < 1$ for every $v ∈ V$.
background
The module derives the Global Co-Identity Constraint from local ingredients. wrapPhase is the canonical fractional-part projection $x ↦ x - ⌊x⌋$ that lands in [0,1). The edge condition uses Jtilde, the reduced phase potential defined in ReducedPhasePotential, which vanishes precisely when phase differences are integer multiples of the base period set by nonzero lam. Upstream gcic_global_phase_unique already shows that zero reduced cost on a connected graph forces all Θ differences to be integers; the present theorem simply wraps those integers onto the torus.
proof idea
The proof is a one-line wrapper that applies gcic_global_phase_unique to obtain the pairwise equality of wrapped phases and then invokes wrapPhase_bounds to confirm the range [0,1).
why it matters
This theorem supplies the compact one-statement version of the GCIC required by the Anno Recognitionis essay §V and arc 8 of the AR-anchored plan. It closes the derivation from graph rigidity and phase rigidity lemmas to the global statement that all vertices share one wrapped phase. In the Recognition Science framework it supports the eight-tick octave by guaranteeing a single global phase across the recognition field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.