Jtilde
plain-language theorem explainer
The reduced phase potential J̃(λ, δ) = cosh(λ d_ℤ(δ)) − 1 quantifies the energy cost of a fractional phase mismatch under discrete scaling. Lattice theorists and recognition-model builders cite it when imposing zero-cost edge conditions to derive global phase uniqueness. The definition is a direct substitution of the integer-distance function into the shifted hyperbolic cosine.
Claim. $J̃(λ, δ) := cosh(λ · d_ℤ(δ)) − 1$, where $d_ℤ(δ) = min_{n∈ℤ} |δ − n|$ is the distance to the nearest integer.
background
The module formalizes the reduced phase-mismatch potential induced by the discrete scaling quotient x ~ b^n x. The upstream definition distZ returns the toroidal distance min(fract(δ), 1 − fract(δ)), which lies in [0, 1/2] and vanishes exactly at integers. The parameter λ = ln b sets the stiffness of the potential for a chosen base b.
proof idea
One-line wrapper that applies the definition of distZ inside the hyperbolic cosine and subtracts one.
why it matters
Jtilde supplies the zero-cost predicate used by every GCIC theorem, including gcic_one_statement (arc 8) and gcic_canonical at λ = ln φ. It closes the local-to-global step in the forcing chain by converting edge-wise vanishing of J̃ into integer winding of the phase field. The construction directly implements the J-uniqueness relation at T5 for the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.