Jtilde_zero_iff
plain-language theorem explainer
The theorem states that the reduced phase potential vanishes exactly when the phase difference is an integer, for any nonzero scaling parameter. Workers on phase rigidity and discrete scaling quotients cite it to characterize alignment conditions where couplings disappear. The proof unfolds the definition, reduces the cosh-equals-one condition via the product-zero property, and applies the integer-distance characterization in both directions.
Claim. For nonzero real $λ$ and real $δ$, the reduced phase potential satisfies $J̃(λ, δ) = 0$ if and only if there exists an integer $n$ such that $δ = n$.
background
The module formalizes the reduced phase-mismatch potential induced by the discrete scaling quotient. distZ(δ) is the distance from δ to the nearest integer, and J̃(λ, δ) is defined by J̃(λ, δ) = cosh(λ · distZ(δ)) − 1 with λ = ln b. This appears in the GCIC paper Section IV on rigidity and compact phase emergence in scale-invariant ratio-based energies. The result rests on the upstream fact that cosh(t) = 1 precisely when t = 0, together with the absence of zero divisors for the logic integers.
proof idea
The tactic proof proceeds by constructor on the biconditional. Forward: J̃ = 0 gives cosh(λ distZ δ) = 1, hence λ distZ δ = 0 by the cosh characterization; mul_eq_zero then splits the product, the nonzero assumption on λ eliminates the first factor, and distZ_eq_zero_iff yields the integer conclusion. Reverse: the integer hypothesis gives distZ δ = 0 by the same distance lemma, after which cosh(0) = 1 produces J̃ = 0.
why it matters
This lemma is applied directly by coupling_vanishes_iff_aligned and neg_Jtilde_coupling_zero_iff in GCICDerivation, and supplies the key step for phase_rigidity, which concludes that a phase field is constant modulo integers on any connected graph once J̃ vanishes on every edge. It supplies the structural zero characterization required for the reduced potential in the scale-invariant framework, supporting the emergence of compact phases under discrete scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.