Jtilde_periodic
plain-language theorem explainer
J̃(λ, δ) is invariant under unit shifts in the phase mismatch δ. Workers on the GCIC reduced phase potential would invoke this to establish that the energy depends only on the fractional part of δ. The proof reduces directly to the already-proved periodicity of the integer-distance function distZ by unfolding the cosh definition.
Claim. $J̃(λ, δ + 1) = J̃(λ, δ)$ for all real $λ, δ$, where $J̃(λ, δ) := cosh(λ · d_ℤ(δ)) - 1$ and $d_ℤ(δ)$ denotes the distance from $δ$ to the nearest integer.
background
The module ReducedPhasePotential formalizes the reduced phase-mismatch potential induced by the discrete scaling quotient $x ~ b^n x$. It defines the function $J̃(λ, δ) = cosh(λ · distZ δ) - 1$ with $λ = ln b$ for the base $b$ of the quotient and distZ the distance to the nearest integer. This construction appears in Section IV of Thapa–Washburn (2026) on rigidity and compact phase emergence in scale-invariant ratio-based energies.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of Jtilde to expose the distZ argument inside the cosh, then rewrites the shifted argument via the sibling theorem distZ_periodic, which itself reduces to distZ_add_int.
why it matters
The periodicity guarantees that J̃ depends only on the fractional part of δ, a structural property required for the phase potential in discrete scaling models. It supports the module's main results including Jtilde_zero_iff and the stiffness lower bound. In the Recognition Science setting it aligns with the self-similar fixed point (T6) and eight-tick octave periodicity (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.