wrapPhase
plain-language theorem explainer
wrapPhase is the canonical fractional-part projection sending each real x to x minus its floor, landing in [0,1). It is cited by derivations of global phase uniqueness on connected recognition lattices. The definition is a direct one-line subtraction of the floor function.
Claim. The map $xmapsto x - lfloor x rfloor$ from $mathbb{R}$ to $[0,1)$.
background
The Global Co-Identity Constraint module derives a global phase statement from local rigidity on a connected graph. Vertices carry real phases Θ; the reduced phase cost vanishes on every edge, forcing differences to be integers. wrapPhase projects these differences onto the torus ℝ/ℤ to obtain a single shared value in [0,1).
proof idea
The definition is a direct one-line wrapper: wrapPhase x := x - Int.floor x. It implements the standard fractional-part projection without additional lemmas.
why it matters
wrapPhase supplies the torus projection required by gcic_global_phase_unique, gcic_existence_of_global_phase, and gcic_one_statement. These theorems establish that every vertex shares the same wrapped phase, realizing the GCIC that all stable boundaries share one global phase. The construction closes the integer-winding ambiguity left by the phase-rigidity result from ReducedPhasePotential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.