neg_Jtilde_coupling_nonpos
plain-language theorem explainer
neg_Jtilde_coupling_nonpos establishes that the negative of the reduced phase potential is non-positive for any real lam and δ. Researchers deriving the Global Co-Identity Constraint from the forcing chain cite this to confirm the attractive sign of the coupling term. The result follows directly from the non-negativity of J̃. The proof is a one-line wrapper applying linear arithmetic to the upstream non-negativity theorem.
Claim. For all real numbers $λ$ and $δ$, $-J̃(λ, δ) ≤ 0$, where $J̃(λ, δ) = cosh(λ · d_ℤ(δ)) - 1$.
background
The module derives the Global Co-Identity Constraint (GCIC) from the J-cost forcing chain with zero empirical axioms, linking T5 J-uniqueness through compact phase to uniform Θ at stationarity. The reduced phase potential is defined as J̃(lam, δ) = cosh(lam · distZ δ) - 1, with lam = ln b for the base of the discrete quotient. Its non-negativity J̃ ≥ 0 is proved upstream by unfolding the definition and applying one_le_cosh to the scaled distance.
proof idea
This is a one-line wrapper that invokes Jtilde_nonneg lam δ and applies linarith to obtain the negated inequality.
why it matters
This declaration confirms the attractive character of the negative J̃ coupling, zero at alignment and negative for misalignment, as stated in the module doc. It supports downstream results such as phase_alignment_minimizes_Jtilde and aligned_collective_cost_zero in the GCIC derivation. The result sits inside the T5-to-T8 forcing chain that forces the compact phase and ratio rigidity used throughout the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.