feat: Complete TightBindingChain Hamiltonian hermiticity and eigenstate orthogonality proofs #918
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…te orthogonality proofs
This PR completes two key sorryful lemmas in the tight binding chain model:
1. `hamiltonian_hermitian`: Proves that the tight binding Hamiltonian is Hermitian
by showing that the inner products satisfy ⟨Hψ, φ⟩ = ⟨ψ, Hφ⟩
- Adds helper lemma `localizedComp_adjoint`: adjoint of |m⟩⟨n| is |n⟩⟨m|
- Adds helper lemma `localizedComp_self_adjoint`: diagonal terms are self-adjoint
2. `energyEigenstate_orthogonal`: Proves energy eigenstates with distinct
wavenumbers are orthogonal using the geometric series identity
- The key insight is that the inner product reduces to ∑ω^n where ω is
an N-th root of unity (from periodic boundary conditions)
- Different wavenumbers give ω ≠ 1, and ∑ω^n = (ω^N - 1)/(ω - 1) = 0
These proofs formalize fundamental quantum mechanical results about the
tight binding model commonly used in condensed matter physics.
physlean0
force-pushed
the
tightbinding-proofs
branch
from
e656351 to
9123a42
Compare
Member
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Added some comments - if you could handle these it would be great, if not let me know and I can do them.
- Move localizedComp_adjoint to section C (after localizedComp_apply_localizedState) - Delete redundant localizedComp_self_adjoint lemma - Use localizedComp_adjoint directly in hamiltonian_hermitian - Golf energyEigenstate_orthogonal proof (37 lines shorter): - Replace match/with with obtain for cleaner destructuring - Combine initial simp steps - Use calc block for hω_pow - Inline intermediate computations - Remove verbose comments while preserving key insights
jstoobysmith
approved these changes
Jan 23, 2026
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Summary
This PR completes two key sorryful lemmas in the tight binding chain model:
hamiltonian_hermitian: Proves that the tight binding Hamiltonian is Hermitian by showing that the inner products satisfy⟨Hψ, φ⟩ = ⟨ψ, Hφ⟩localizedComp_adjoint: adjoint of |m⟩⟨n| is |n⟩⟨m|localizedComp_self_adjoint: diagonal terms are self-adjointenergyEigenstate_orthogonal: Proves energy eigenstates with distinct wavenumbers are orthogonal using the geometric series identityThese proofs formalize fundamental quantum mechanical results about the tight binding model commonly used in condensed matter physics.
Test plan
lake build PhysLean.CondensedMatter.TightBindingChain.Basiccompiles successfully@[sorryful]annotations🤖 Generated with Claude Code