auto-task(energyEigenstate_orthogonal): golf the tight-binding chain orthogonality proof

[jakeuribe]

Summary

Golfs the proof of TightBindingChain.energyEigenstate_orthogonal in
Physlib/CondensedMatter/TightBindingChain/Basic.lean from 57 lines to 32.
The statement is unchanged.

What changed

• Term lemma instead of a sum rewrite. The old proof stated hsum_eq, a full
  equality of sums, and re-typed the whole summand inside
  Fin.sum_univ_eq_sum_range (fun n => ...). It is replaced by a pointwise
  hterm (n : ℕ) : conj (exp (I * k1 * n * a)) * exp (I * k2 * n * a) = ω ^ n,
  which simp only applies under the binder, so the index-set conversion becomes
  the one-liner Fin.sum_univ_eq_sum_range (ω ^ ·).
• geom_sum_eq instead of mul_geom_sum. The final three steps
  (mul_geom_sum → rw → mul_eq_zero.mp ... |>.resolve_left ...) collapse into
  geom_sum_eq hω_ne_one, hω_pow, sub_self, zero_div, folded into the closing rw.
• hω_pow as a single rw chain. The calc block with two ring_nf calls and
  two auxiliary haves becomes one rw using a show ... by push_cast; ring
  bridge and T.quantaWaveNumber_exp_N applied directly.
• Divisibility instead of nlinarith. m = 0 was derived by bounding
  T.N * m and calling nlinarith. It is now
  Int.eq_zero_of_abs_lt_dvd on (T.N : ℤ) ∣ (n2 : ℤ) - n1, removing the
  nlinarith call and three cast haves.
• Smaller cleanups: hω_ne_one is a term-mode fun ... => hne <| by ...;
  starRingEnd_apply/Complex.star_def are dropped in favour of rewriting
  with ← Complex.exp_conj directly; the hand-written ofReal_* simp only
  list becomes push_cast; (T.N : ℂ) ≠ 0 is a term
  (Nat.cast_ne_zero.mpr (NeZero.ne T.N)) rather than a simp call.

The remaining comments were rewritten to sit above the three structural steps
(per-term root of unity → ω ^ N = 1 → ω ≠ 1 → geometric sum vanishes).

Verification

lake build completes successfully (9264 jobs), with no new warnings, sorrys,
or axioms.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.