pith. sign in
module module high

IndisputableMonolith.Papers.GCIC.ReducedPhasePotential

show as:
view Lean formalization →

This module supplies the reduced phase potential objects used in GCIC derivations. It defines distZ as toroidal distance to the nearest integer together with the derived Jtilde function and their elementary properties. Researchers citing the Global Co-Identity Constraint or its forcing-chain derivation would reference these definitions. The module consists entirely of definitions and basic lemmas with no complex proofs.

claim$d_{\mathbb{Z}}(\delta) := \min(\{\delta\}, 1 - \{\delta\})$ where $\{\delta\}$ denotes the fractional part; this lies in $[0,1/2]$ and equals zero precisely when $\delta \in \mathbb{Z}$. The module also introduces the associated periodic function $\tilde{J}$ together with its non-negativity and zero-set characterizations.

background

The ReducedPhasePotential module belongs to the Papers.GCIC series and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with the J-cost apparatus from the Cost module. Its central definition is distZ, the distance to the nearest integer on the circle, given explicitly by the supplied doc-comment as $d_{\mathbb{Z}}(\delta) = \min(\mathrm{fract}(\delta), 1 - \mathrm{fract}(\delta))$. This quantity is non-negative, at most $1/2$, periodic with period 1, and vanishes exactly on the integers.

Sibling definitions establish the same properties for the auxiliary function Jtilde, including its non-negativity, periodicity, and the equivalence Jtilde($\delta$)=0 $\iff$ $\delta \in \mathbb{Z}$ via the cosh identity. These objects prepare the phase reduction needed for global co-identity arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Global Co-Identity Constraint, which asserts that all stable boundaries share one global phase, and the GCICDerivation, which obtains that constraint from the J-cost forcing chain via ratio rigidity plus compact phase. By supplying the concrete distance and Jtilde functions, it closes the local-to-global step in the T5–T7 arc without introducing new axioms.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)