IndisputableMonolith.Papers.GCIC.ReducedPhasePotential
The ReducedPhasePotential module defines the toroidal distance distZ to the nearest integer and the reduced Jtilde function for phase analysis. Researchers deriving the Global Co-Identity Constraint cite these when reducing phase to the compact circle. The module supplies the core definitions plus elementary lemmas on non-negativity, periodicity, and zero sets, all built from the imported Cost and Constants structures.
claim$d_ℤ(δ) = min(fract(δ), 1 - fract(δ))$ lies in $[0, 1/2]$ and equals zero precisely when $δ ∈ ℤ$. The reduced potential satisfies $Jtilde(δ) ≥ 0$, $Jtilde(δ + n) = Jtilde(δ)$ for $n ∈ ℤ$, and $Jtilde(δ) = 0$ iff $δ ∈ ℤ$.
background
The module sits inside the Recognition Science treatment of phase compactness for the Global Co-Identity Constraint. It imports the fundamental time quantum τ₀ = 1 tick from Constants and the J-cost functional from Cost. distZ is introduced exactly as the distance to the nearest integer on the circle, while Jtilde is the corresponding reduced potential obtained by composing J with the exponential map to the phase circle.
proof idea
This is a definition module. distZ is defined via the fractional-part minimum and its four basic properties (non-negativity, bound by 1/2, periodicity, zero set) are proved by direct fractional-part arithmetic. Jtilde is then defined from the upstream J and shown to inherit non-negativity, periodicity, and the zero condition by substitution and the already-established distZ lemmas.
why it matters in Recognition Science
These objects supply the compact-phase ingredient required by the downstream GlobalCoIdentityConstraint (all stable boundaries share one global phase) and by GCICDerivation (T5 J-uniqueness plus T6-T7 compact phase Θ ∈ ℝ/ℤ yields GCIC at J-stationarity). The module therefore closes the phase-reduction step in the forcing-chain derivation of the GCIC.
scope and limits
- Does not derive or state the Global Co-Identity Constraint itself.
- Does not invoke the full T0-T8 forcing chain or ratio-rigidity lemmas.
- Does not address spatial dimension D=3 or the eight-tick octave.
- Does not treat multi-field or interacting-phase extensions.
used by (2)
depends on (2)
declarations in this module (16)
-
def
distZ -
theorem
distZ_nonneg -
theorem
distZ_le_half -
theorem
distZ_add_int -
theorem
distZ_periodic -
theorem
distZ_eq_zero_iff -
def
Jtilde -
theorem
Jtilde_nonneg -
theorem
Jtilde_periodic -
theorem
Jtilde_add_int -
lemma
cosh_eq_one_iff -
theorem
Jtilde_zero_iff -
theorem
Jtilde_stiffness_lb -
def
gcic_kappa -
theorem
gcic_kappa_pos -
theorem
phase_rigidity