wrapPhase_add_int
plain-language theorem explainer
Wrapped phase, the fractional-part projection of a real, stays fixed under addition of any integer. Workers deriving global phase uniqueness on connected recognition graphs cite the invariance to quotient out integer windings onto the torus. The term proof unfolds the fractional-part definition, rewrites via the floor-addition identity for integers, and reduces the equality by ring simplification.
Claim. If $x : ℝ$ and $n : ℤ$, then wrapPhase$(x + n) =$ wrapPhase$(x)$, where wrapPhase$(x) := x - ⌊x⌋$.
background
wrapPhase is the canonical fractional-part projection ℝ → [0,1) defined by wrapPhase x := x - Int.floor x. The definition is placed locally to avoid import cycles with the Consciousness layer, where an identical frac operation is used. The module derives the Global Co-Identity Constraint from local rigidity: ratio rigidity on connected graphs forces constant fields, while vanishing reduced phase cost forces phase differences to be integers; the present result supplies the invariance that projects those integers onto the circle.
proof idea
The proof unfolds the definition of wrapPhase, rewrites using the integer floor-addition identity, pushes the cast, and concludes by ring simplification.
why it matters
The theorem is invoked by gcicCert, the master certificate that assembles the global co-identity constraint for any inhabited vertex set, and by wrapPhase_eq_of_int_diff. It completes the wrapping step that turns local integer windings into a single global phase shared across all vertices, realizing the GCIC statement from the Anno Recognitionis essay. The result closes the link from local phase rigidity to global uniqueness on the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.