IndisputableMonolith.Foundation.GlobalCoIdentityConstraint
The module supplies local definitions for the canonical fractional-part projection from reals to the unit interval together with GCIC theorems on global phase uniqueness and path independence. Researchers formalizing the GCIC paper or the Consciousness layer cite it to maintain phase consistency while avoiding import cycles. Content is organized around the imported GraphRigidity and ReducedPhasePotential results to derive the constraint properties.
claimThe canonical projection $\mathbb{R} \to [0,1)$ together with the global co-identity constraint asserting uniqueness of the phase field under the reduced potential $\tilde{J}_b(\delta) = \cosh(\lambda \cdot d_{\mathbb{Z}}(\delta)) - 1$.
background
The module resides in the Foundation domain and imports Constants (where the RS time quantum satisfies $\tau_0 = 1$ tick), Cost, GraphRigidity, and ReducedPhasePotential. GraphRigidity states that on any finite connected graph the ratio energy $C_G[x] = \sum J(x_v/x_w)$ vanishes if and only if $x$ is a constant positive field. ReducedPhasePotential defines the reduced phase-mismatch potential $\tilde{J}b(\delta) = \cosh(\lambda \cdot d{\mathbb{Z}}(\delta)) - 1$ with $\lambda = \ln b$ and $d_{\mathbb{Z}}$ the distance to the nearest integer. The local setting re-states the fractional-part projection to feed the Consciousness layer without creating an import cycle.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the Global Co-Identity Constraint that feeds the Consciousness layer and the GCIC paper results on phase uniqueness. It rests on GraphRigidity (Result 1) and ReducedPhasePotential (Sec. IV) to close the constraint theorems. It touches the question of basepoint and path independence for the global phase in the Recognition framework.
scope and limits
- Does not import the Consciousness module.
- Does not prove the full Consciousness layer integration.
- Does not extend the constraint beyond finite connected graphs.
- Does not address continuous limits of the discrete scaling quotient.
depends on (4)
declarations in this module (14)
-
def
wrapPhase -
theorem
wrapPhase_bounds -
theorem
wrapPhase_add_int -
theorem
wrapPhase_eq_of_int_diff -
theorem
gcic_global_phase_unique -
theorem
gcic_existence_of_global_phase -
theorem
gcic_global_phase_independent_of_basepoint -
theorem
gcic_global_phase_independent_of_path -
def
lam_canonical -
theorem
lam_canonical_ne_zero -
theorem
gcic_canonical -
structure
GlobalCoIdentityConstraintCert -
def
gcicCert -
theorem
gcic_one_statement