Jtilde_add_int
plain-language theorem explainer
The theorem establishes invariance of the reduced phase potential under integer shifts of its argument. Researchers deriving GCIC stiffness bounds would cite this when collapsing periodic phase terms over the discrete scaling quotient. The proof is a one-line wrapper that unfolds the definition of Jtilde and rewrites via the integer periodicity of the distance-to-nearest-integer function.
Claim. For all real numbers $λ$ and $δ$ and every integer $n$, $J̃(λ, δ + n) = J̃(λ, δ)$, where $J̃(λ, δ) := cosh(λ · d_ℤ(δ)) - 1$ and $d_ℤ(δ)$ is the distance from $δ$ to the nearest integer.
background
The Reduced Phase Potential module formalizes the reduced phase-mismatch potential induced by the discrete scaling quotient x ~ b^n x. The function J̃ is defined by J̃(λ, δ) = cosh(λ · distZ δ) - 1, where λ = ln b and distZ δ denotes the distance to the nearest integer. The upstream theorem distZ_add_int establishes that distZ(δ + n) = distZ(δ) for any integer n, which is the direct algebraic ingredient for the present result.
proof idea
The proof is a one-line wrapper: unfold Jtilde to expose the cosh expression, then rewrite the distZ argument using the upstream theorem distZ_add_int that proves integer periodicity of the distance function.
why it matters
This periodicity result feeds directly into the theorem neg_Jtilde_coupling_periodic in the GCICDerivation module, which supports the stiffness analysis for base φ in the GCIC paper (Thapa–Washburn, 2026, Section IV). It closes the structural loop on 1-periodicity of the reduced potential, aligning with the discrete scaling quotient and the Recognition framework's use of periodic J-cost terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.