Research update · 10 September 2026
Our 2D Hubbard project has reached a particularly satisfying milestone: we have connected a concrete interacting quantum Hamiltonian to a short-time dynamical result that Lean checks as a mathematical proof. For the central doublon observable of our 3×3 model, the first nonzero term is exactly the fourth power of time, with coefficient exactly one.
\[F(T)=T^4+R_4(T).\]Here, the remainder is an explicitly defined, convergent series of higher-order terms. The certified result is the complete coefficient sequence through degree four: 0, 0, 0, 0, 1. This gives our project a proof-backed theoretical reference, alongside its classical simulations and quantum-hardware experiments.
For a student-scale research project, that is something worth celebrating: a result we can calculate, explain physically, check independently, and trace back to its mathematical foundations.
A nine-site model with real fermionic structure
We use an open 3×3 square lattice. Each site has an up-spin and a down-spin fermionic mode, giving 18 modes in total. The initial state contains four up-spin and four down-spin particles, arranged around an empty central site:
\[|\psi_0\rangle:\qquad\begin{matrix}
\uparrow & \downarrow & \uparrow \\
\downarrow & \circ & \downarrow \\
\uparrow & \downarrow & \uparrow
\end{matrix}\]
With particle numbers fixed, the state space has a manageable but substantial size:
\[\dim\mathcal H_{4,4}=\binom94\binom94=15\,876.\]The model includes nearest-neighbour hopping, diagonal hopping, and an on-site interaction. In units where the nearest-neighbour hopping and ℏ are one, we take t′ = −1/4 and U = 8:
\[\begin{aligned}H={}&-\sum_{\langle i,j\rangle,\sigma}
\left(c^\dagger_{i\sigma}c_{j\sigma}+c^\dagger_{j\sigma}c_{i\sigma}\right)\\
&+\frac14\sum_{\langle\!\langle i,j\rangle\!\rangle,\sigma}
\left(c^\dagger_{i\sigma}c_{j\sigma}+c^\dagger_{j\sigma}c_{i\sigma}\right)\\
&+8\sum_i n_{i\uparrow}n_{i\downarrow}.
\end{aligned}\]
The first sum covers the 12 nearest-neighbour bonds; the second covers the eight diagonal bonds. The creation and annihilation operators carry the fermionic signs. In the proof and independent checks, those signs are part of the actual calculation.
From the Hamiltonian to a dynamical observable
A doublon is a site occupied by both spin species. Let c denote the centre of the lattice. Its doublon projector is:
\[D_c=n_{c\uparrow}n_{c\downarrow}.\]Our observable is the probability of finding a doublon at that site after evolution for time T:
\[F(T)=\langle\psi_0|e^{iHT}D_c e^{-iHT}|\psi_0\rangle.\]The new Lean connection reaches all the way to this matrix exponential. It establishes a genuinely convergent expansion, for every real T, using the same concrete Hamiltonian, observable, and initial state:
\[F(T)=\sum_{n=0}^{\infty}c_nT^n,\qquadc_0=c_1=c_2=c_3=0,\qquad c_4=1.\]
The exact remainder in our opening formula is:
\[R_4(T)=\sum_{n=0}^{\infty}c_{n+5}T^{n+5}.\]This clean separation identifies precisely what has been certified: the leading short-time behaviour, with higher orders retained in an exact series. It also connects the archived even-power prefix [0, 0, 1] to the underlying time evolution.
Why the first contribution is proportional to T⁴
The physics behind the result is wonderfully concrete. The centre starts empty. A single hop can bring one particle to the centre, but a doublon needs two particles, one of each spin. Consequently, both the initial state and its first Hamiltonian image vanish when projected onto central doublons:
\[D_c|\psi_0\rangle=0,\qquad D_cH|\psi_0\rangle=0.\]Expanding the evolved state therefore gives:
\[D_c e^{-iHT}|\psi_0\rangle=-\frac{T^2}{2}D_cH^2|\psi_0\rangle
+\sum_{n=3}^{\infty}\frac{(-iT)^n}{n!}D_cH^n|\psi_0\rangle.\]
The first possible amplitude is of second order in time. A probability is a squared norm, so its first contribution is of fourth order. The remaining question is the exact coefficient:
\[c_4=\frac14\left\|D_cH^2|\psi_0\rangle\right\|^2.\]How exact integers produce the coefficient one
To make the arithmetic transparent, we scale the Hamiltonian by four. The resulting matrix H₄ = 4H has integer entries. The sparse path calculation finds 32 nonzero two-step contributions, which combine into 16 distinct central-doublon output states.
Contributions leading to the same final state are added as signed amplitudes before taking their squared magnitude. This preserves quantum interference and the fermionic sign structure. The exact result is:
\[\left\|D_cH_4^2|\psi_0\rangle\right\|^2=1024.\]Since squaring the norm of the two-step amplitude introduces four powers of the Hamiltonian, undoing the scaling gives:
\[c_4=\frac14\,\frac{1024}{4^4}=1.\]The coefficient is therefore an exact rational result. The leading term captures the hopping geometry; the same framework provides a route towards higher-order terms that resolve more of the interaction-dependent dynamics.
Three complementary ways to check the result
The final formal audit covers 66 named theorems, including 37 added for the new analytic connection. Their proofs pass Lean’s kernel using the standard foundational axioms, without unfinished proof placeholders or custom assumptions supplying the answer. Three deliberately incorrect coefficient claims are rejected by exact arithmetic.
A separately implemented fermionic calculation checks the path counts and integer norm. An independent numerical calculation then constructs the full 15,876-dimensional sparse Hamiltonian and applies its exponential to the initial state:
| Time T | Numerical F(T) | Leading term T⁴ | F(T) / T⁴ |
|---|---|---|---|
| 0.005 | 6.24872846 × 10⁻¹⁰ | 6.25 × 10⁻¹⁰ | 0.99979655 |
| 0.010 | 9.99186513 × 10⁻⁹ | 1.00 × 10⁻⁸ | 0.99918651 |
| 0.020 | 1.59480139 × 10⁻⁷ | 1.60 × 10⁻⁷ | 0.99675087 |
These floating-point checks show the expected approach to the exact leading coefficient as time becomes smaller. The numerical values supply an independent cross-check; Lean supplies the proof of the coefficient.
A positive step for the whole 2D project
The achievement is a verified connection between the model we wrote down and a concrete piece of the dynamics it generates. Our proof-backed 3×3 reference strengthens the small-system foundation of a project that also explores larger lattices, hardware measurements, and error mitigation.
It also gives us a productive way forward: extend the certified coefficient range, add observables, and build quantitative remainder estimates on top of a working Hamiltonian-to-dynamics connection.
We now have a leading short-time quantum prediction whose coefficient is exactly derived, independently checked, and machine-verified from the concrete model. That is a meaningful mathematical achievement for our 2D project—and a strong foundation to build on.
Research record
This update reports our central-doublon analytic pilot completed on 10 September 2026. The versioned research archive preserves the model conventions, Lean sources, compilation records, transitive theorem audit, rejected false controls, and independent numerical checks.
Reproduce the formal certificate
Retrievable GitHub checkpoint: e7faf3906aad. The self-contained Lean package includes the precise definitions and final theorems, all 145 project source modules, pinned dependencies, the transitive axiom audit, rejected false controls, and reproduction instructions. The repository is private; repository access is required.
The source package has been rebuilt in a fresh local project directory without reusing any old project proof binaries. Pinned upstream Mathlib dependency caches were reused. The clean build includes the prerequisite Hamiltonian certificates and separately audits the 66 pilot theorems. The accepted axioms remain propext, Classical.choice, and Quot.sound.
Original local research checkpoint: d97c3b5. This identifies the earlier local research repository, not a commit in the linked GitHub repository. For independent reproduction, use the retrievable GitHub checkpoint above. Lean 4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Certified numerical scope: the central 3×3 doublon coefficients through degree four. Reproducibility links updated 12 September 2026.