sample
plain-language theorem explainer
Sampling map that evaluates a continuum scalar field on the unit 3-torus at the normalized coordinates of a side-N periodic cubic vertex. Gravity and continuum-limit arguments cite it whenever a lattice field is obtained from a smooth witness. The body is a pure evaluation: f at x/N in each coordinate.
Claim. For $N \in \mathbb{N}$, a continuum field $f : (\mathrm{Fin}\,3 \to \mathbb{R}) \to \mathbb{R}$, and a vertex $x$ of the side-$N$ periodic cubic lattice, the sample is $f(x_1/N,\, x_2/N,\, x_3/N)$, i.e. the value of $f$ at the point $x/N$ on the unit 3-torus.
background
The module develops the action-level continuum limit of the frozen quadratic energy on the canonical Freudenthal family (QG Phase 2b, panel-locked Test G stage 2). The fixed nonconstant $C^2$ witness is $f(x,y,z)=\sin(2\pi x)$; lattice computations compare its discrete energy to the independent continuum target $\int_{[0,1]^3}\langle\nabla f, A_0\nabla f\rangle$.
Vertices are the periodic cubic points Vertex N N N := Fin N × Fin N × Fin N. Each discrete index triple sits at the continuum location $x/N$ in the unit cube with opposite faces identified. The sampling map is the bridge that turns any continuum field into a lattice configuration on that family.
Upstream, the geometry layer only supplies the vertex type; no energy or stencil data enters the definition itself.
proof idea
Pure definition, not a theorem. Unpack the triple product vertex into its three Fin N components, cast each valuation to $\mathbb{R}$, divide by $N$, and feed the resulting three-vector into $f$ via the matrix cons notation ![·,·,·]. No lemmas are applied.
why it matters
Every stage-2 energy comparison in this module is stated on the sampled witness: scaledCanonicalEnergy N (sample N witnessField) versus continuumTarget. Downstream theorems scaledCanonicalEnergy_witness_rate, freudenthal_witness_energy_limit, and the integral-form rate bound all apply this map; sample_witnessField identifies it with the explicit first-coordinate form witnessSample. The closed-form distance bound and SPARC/exclusivity checkers also thread through the same sampling. It is the lattice embedding step that makes the panel-locked $O(1/N)$ continuum-limit observable well-defined. Framework context is the tensor-first anisotropic action limit on the Freudenthal family; the path-sum pillar remains out of scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.