H_Convergence
plain-language theorem explainer
Coarse-grained Riemann sums of an observable f converge to a finite limit I under this definition. Researchers bridging discrete tick embeddings to continuum equations in Recognition Science cite it when passing from cell volumes to integral statements. The definition directly encodes the standard epsilon-N criterion applied to the sequence of partial sums from the RiemannSum operator.
Claim. Let CG be a coarse graining with an embedding of natural numbers into cells and nonnegative volume weights. For a real-valued observable $f$ on the cells and a candidate limit $I$, the property holds when the partial sums satisfy $∀ε>0 ∃N ∀n≥N |∑_{i=0}^{n-1} f(embed(i))⋅vol(embed(i)) - I| < ε$.
background
The module sets up coarse graining through the CoarseGrain structure, which supplies an embedding map from naturals (ticks) to a cell type α together with a volume weight function obeying nonnegativity. RiemannSum then forms the weighted partial sums of any observable f over the first n embedded cells. This sits inside the classical bridge that converts discrete Recognition Science objects into continuum statements, drawing on upstream ledger factorizations and phi-forcing structures for the underlying J-cost calibration.
proof idea
The declaration is a direct definition of the epsilon-N convergence criterion. It applies the standard limit definition to the sequence of partial sums produced by the RiemannSum function over increasing n.
why it matters
This supplies the convergence hypothesis required by the downstream discrete_to_continuum_continuity, which asserts existence of such an I for divergence observables and thereby obtains the continuum continuity equation. It fills a scaffold step in the classical bridge from discrete embeddings to continuum limits, connecting to the phi-ladder and eight-tick octave in the broader framework. The associated TODO flags the need to establish convergence for concrete LNAL distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.