neg_Jtilde_coupling_zero_iff
plain-language theorem explainer
The equivalence shows that the negated reduced phase potential vanishes exactly when the phase defect is an integer. Researchers deriving the Global Co-Identity Constraint from the forcing chain cite it to confirm sign invariance of the discrete gauge condition. The proof is a direct biconditional reduction to the positive Jtilde zero lemma via linear arithmetic.
Claim. For nonzero real number $λ$ and real number $δ$, $-J̃(λ, δ) = 0$ if and only if there exists an integer $n$ such that $δ = n$.
background
The module derives the Global Co-Identity Constraint from the J-cost forcing chain. The reduced phase potential is defined by J̃(λ, δ) := cosh(λ · distZ δ) − 1, where distZ measures distance to the nearest integer. This supplies the compact phase Θ ∈ ℝ/ℤ required by T6+T7 of the forcing chain after ratio rigidity is imposed at J = 0.
proof idea
The term proof constructs the biconditional by applying Jtilde_zero_iff in both directions. The forward direction invokes the positive implication and linarith to absorb the outer negation; the converse invokes the reverse implication and linarith.
why it matters
The result closes the sign-invariant half of the phase-alignment argument inside the GCIC derivation. It sits among siblings that establish coupling stiffness and collective-cost minimization, confirming that the discrete-gauge condition from T5 J-uniqueness survives sign flip of the potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.