GlobalCoIdentityConstraintCert
plain-language theorem explainer
Global phase uniqueness on connected graphs follows from local vanishing of the reduced phase cost Jtilde once phases are projected onto the unit interval via the fractional-part map. Researchers deriving the Anno Recognitionis global co-identity constraint would invoke this certificate to assert that all vertices share one wrapped phase. The structure directly enumerates five properties: interval landing for wrapPhase, integer-shift invariance, uniqueness of the wrapped phase, existence of a single global value in [0,1), and basepoint freedom.
Claim. A certificate structure on an inhabited vertex set $V$ whose fields assert: (i) the fractional-part projection satisfies $0 ≤ wrap(x) < 1$ for all real $x$; (ii) $wrap(x + n) = wrap(x)$ for every integer $n$; (iii) on any connected adjacency relation, for nonzero base $λ$ and phase map $Θ$ with $Jtilde_λ(Θ(v) - Θ(w)) = 0$ on every edge, one has $wrap(Θ(v)) = wrap(Θ(w))$ for all vertices; (iv) there exists $Θ_g ∈ [0,1)$ such that $wrap(Θ(v)) = Θ_g$ for every $v$; (v) the common wrapped value is independent of basepoint choice.
background
The module derives the global co-identity constraint from already-proved local rigidity. wrapPhase is the canonical fractional-part map $x ↦ x - ⌊x⌋$, definitionally equal to the earlier Consciousness.GlobalPhase.wrapPhase. Upstream, ratio_rigidity_iff shows vanishing ratio cost on a connected graph forces a constant positive field, while phase_rigidity shows that vanishing reduced phase cost forces phase differences to be integers (windings). The local theoretical setting is the Anno Recognitionis essay §V claim that all stable boundaries share one global phase, now expressed as a Lean-derivable statement on any connected recognition lattice.
proof idea
The declaration is a structure definition whose five fields are stated directly as the required properties. No tactics appear; the inhabitant is supplied downstream by gcicCert, which applies the sibling lemmas wrapPhase_bounds, wrapPhase_add_int, and gcic_global_phase_unique to populate the fields.
why it matters
This certificate realizes arc 8 of the AR-anchored completion plan by packaging the global GCIC statement. It is consumed by gcicCert to furnish an inhabited instance for any Inhabited V. The construction closes the derivation from local graph rigidity (GraphRigidity.ratio_rigidity_iff and ReducedPhasePotential.phase_rigidity) to the global phase uniqueness asserted in the Recognition Physics Institute working paper. In the framework it supports phase coherence across the recognition lattice, consistent with the eight-tick octave and the universal forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.