sampledPhasePoint
plain-language theorem explainer
Samples continuum configuration and momentum fields onto the n-site periodic lattice by evaluating at nodes j/n. Anyone binding continuum Dirac-algebra data to the discrete HamDynN bracket cites this map. It is a pure definitional pairing of the two pointwise samples into a PhaseSpace point.
Claim. For $n \ge 1$ and continuum fields $q,p:\mathbb{R}\to\mathbb{R}$, the sampled phase point is the lattice pair $(q_j,p_j)_{j\in\mathbb{Z}/n\mathbb{Z}}$ with $q_j=q(j/n)$ and $p_j=p(j/n)$.
background
The ambient setting is the Wave C2 R4 repair: bind freestanding Riemann-shape sampled bracket sums to the genuine lattice bracket of dynamic Hamiltonians after periodic wrap treatment, then land the continuum-limit ledger terminal for 1-periodic $C^1$ data.
Upstream, the canonical phase space on an $n$-site periodic lattice is the product of configuration and conjugate momentum maps $q,\pi:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$. Continuum fields live on $\mathbb{R}$; the lattice only sees values at the uniform nodes $j/n$ for $j=0,\ldots,n-1$. On $\mathbb{Z}/n\mathbb{Z}$ the successor of site $n-1$ wraps to $0$, so periodic sampling is the correct discrete image of 1-periodic continuum data.
proof idea
Definitional construction, not a proof. The body is the ordered pair of maps $j\mapsto q(j.\mathrm{val}/n)$ and $j\mapsto p(j.\mathrm{val}/n)$ on $\mathbb{Z}/n\mathbb{Z}$, which inhabits the phase-space product type by construction. No lemmas are applied.
why it matters
This is the continuum-to-lattice injection used everywhere the discrete dynamic bracket is evaluated on continuum samples. Downstream, the identity equating the HamDynN bracket at these samples to the periodic sampled sum unfolds definitionally through it; the continuum lattice bracket packages the same evaluation (with a junk zero at $n=0$); and the continuum-limit theorem for HamDynN takes the lattice form built on these samples under 1-periodicity and $C^1$ hypotheses. Without a uniform sampling map, the discrete Dirac algebra cannot be compared to its continuum target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.