RiemannSum
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convergence of the sums to any limit.
- Does not invoke the nonneg_vol field of CoarseGrain.
- Does not extend the sum to the infinite case or define an integral.
- Does not depend on specific algebraic properties of the observable f.
formal statement (Lean)
14def RiemannSum (CG : CoarseGrain α) (f : α → ℝ) (n : Nat) : ℝ :=
proof body
Definition body.
15 (Finset.range n).sum (fun i => f (CG.embed i) * CG.vol (CG.embed i))
16
17/-- Statement schema for the continuum continuity equation (divergence form in the limit). -/