wrapPhase_bounds
wrapPhase_bounds shows that the fractional-part projection of any real number lands in the half-open unit interval [0,1). Global Co-Identity Constraint derivations on recognition lattices invoke this bound to guarantee a well-defined global phase on the torus. The argument is a direct term-mode reduction that unfolds the definition and applies the standard floor inequalities.
claimFor every real number $x$, the wrapped phase defined by $x - floor(x)$ satisfies $0 ≤ x - floor(x) < 1$.
background
The Global Co-Identity Constraint module derives global phase uniqueness from local rigidity on recognition lattices. wrapPhase is the canonical fractional-part projection $x - floor(x)$ onto [0,1), introduced to avoid import cycles with the Consciousness layer while matching its definition. This bound is the first local ingredient needed before integer-winding reduction and torus identification can produce a single global phase.
proof idea
One-line wrapper that splits the conjunction and applies Int.floor_le for the lower bound together with Int.lt_floor_add_one for the upper bound, then unfolds wrapPhase and closes both goals with linarith.
why it matters in Recognition Science
The bound supplies the wrap_in_unit_interval field of gcicCert and is invoked by gcic_existence_of_global_phase and gcic_one_statement. It completes the wrapping step of arc 8, converting integer windings forced by ReducedPhasePotential.phase_rigidity into a unique Θ_global in [0,1) that is shared across any connected lattice. The result links the 8-tick phase periodicity to the global co-identity statement.
scope and limits
- Does not prove invariance under integer shifts.
- Does not compute the wrapped value for any concrete x.
- Does not extend the bound to complex arguments.
- Does not address continuity or differentiability of wrapPhase.
formal statement (Lean)
107theorem wrapPhase_bounds (x : ℝ) : 0 ≤ wrapPhase x ∧ wrapPhase x < 1 := by
proof body
Term-mode proof.
108 refine ⟨?_, ?_⟩
109 · have := Int.floor_le x; unfold wrapPhase; linarith
110 · have := Int.lt_floor_add_one x; unfold wrapPhase; linarith
111
112/-- Wrapped phase is invariant under shifts by integers. -/