wrapPhase_bounds
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.