wrapPhase_add_int
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not prove existence or uniqueness of the global phase value.
- Does not apply to shifts by non-integers.
- Does not invoke graph structure or cost functions.
- Holds for the specific fractional-part definition only.
formal statement (Lean)
113theorem wrapPhase_add_int (x : ℝ) (n : ℤ) :
114 wrapPhase (x + (n : ℝ)) = wrapPhase x := by
proof body
Term-mode proof.
115 unfold wrapPhase
116 rw [Int.floor_add_intCast]
117 push_cast
118 ring
119
120/-- If two reals differ by an integer, they wrap to the same value. -/