gcicCert
plain-language theorem explainer
gcicCert constructs the master Global Co-Identity Constraint Certificate for any inhabited type V. It assembles the fractional-part wrapping map bounds, integer invariance, and the uniqueness plus existence of a single global wrapped phase on connected graphs with zero reduced phase cost. The definition is a direct record construction that delegates each field to sibling lemmas on phase wrapping and graph rigidity.
Claim. For any inhabited type $V$, the Global Co-Identity Constraint Certificate is the structure whose fields assert that the wrapping projection lands in $[0,1)$, remains invariant under integer shifts, that every pair of vertices shares the same wrapped phase on any connected graph with vanishing reduced phase cost at nonzero base, that a unique global phase in $[0,1)$ exists, and that this phase is independent of basepoint.
background
The module derives the Global Co-Identity Constraint from local graph rigidity on recognition lattices. The wrapping projection is the canonical fractional-part map sending each real to its representative in $[0,1)$. The structure GlobalCoIdentityConstraintCert collects the five properties: interval bounds on the wrap, integer invariance, global uniqueness of wrapped phase when the graph is connected and reduced phase cost vanishes on edges for nonzero base, existence of the single global phase, and basepoint independence. Upstream results on ratio rigidity and phase rigidity force phase differences to be integers on connected components, which the wrapping then collapses to a unique value.
proof idea
The definition is a record construction. It sets the interval bound field to the wrapPhase_bounds lemma, the integer invariance field to wrapPhase_add_int, the global uniqueness field to gcic_global_phase_unique, the existence field to gcic_existence_of_global_phase, and the basepoint independence field to gcic_global_phase_independent_of_basepoint, each applied under the connectedness and zero-cost hypotheses.
why it matters
This definition supplies the inhabited master certificate for the GCIC, realizing the one-statement theorem that all stable boundaries share one global phase on the recognition lattice. It closes arc 8 of the completion plan by packaging the local rigidity results into the global coherence statement. The result sits in the foundation layer and supports further derivations of universal phase coherence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.