RiemannSum
plain-language theorem explainer
RiemannSum defines the partial sum approximating the integral of an observable f over the first n cells of a coarse graining CG. Researchers establishing discrete-to-continuum limits for the continuity equation cite it when passing from tick embeddings to continuum fields. The definition is a direct Finset range sum of the product f at each embedded cell times the cell volume.
Claim. Let $CG$ be a coarse graining structure with embedding function $embed: Nat → α$ and volume function $vol: α → ℝ$. For observable $f: α → ℝ$ and natural number $n$, the Riemann sum equals $∑_{i=0}^{n-1} f(embed(i)) · vol(embed(i))$.
background
CoarseGrain is a structure supplying an explicit embedding of natural numbers (ticks) into cells of type α together with a volume weight for each cell and the axiom that all volumes are nonnegative. The module sets up coarse graining to connect discrete Recognition Science objects to classical continuum equations. Upstream results supply the embed operation from ArithmeticFromLogic (mapping LogicNat orbits into positive reals) and the divergence operator from DiscreteNSOperator, both of which feed the cell-wise summation.
proof idea
The definition is a one-line wrapper that applies Finset.range n to sum the product of f(CG.embed i) and CG.vol(CG.embed i) for each index i.
why it matters
RiemannSum supplies the discrete approximant required by the downstream hypothesis H_Convergence, which posits that the sums converge to a finite limit I, and by the theorem zero_field_converges that constructs the witness for the zero field. It therefore closes the classical bridge step that converts the Recognition Science tick structure into the divergence form of the continuity equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.