H_Convergence
Coarse-grained Riemann sums of an observable converge to a finite limit I under the standard epsilon-N criterion. Researchers bridging discrete tick models to continuum field equations cite this when establishing continuity from discrete Recognition Science structures. The definition directly encodes the limit condition using weighted sums over embedded cells with non-negative volume weights.
claimLet $e$ map natural numbers to cells and let $v$ assign non-negative real volumes to those cells. For an observable $f$, the property holds for a real number $I$ when, for every $ε > 0$, there exists $N$ such that for all $n ≥ N$ the absolute difference between the weighted sum of $f(e(i)) v(e(i))$ over $i = 0$ to $n-1$ and $I$ is less than $ε$.
background
Coarse graining is defined by a structure that supplies an embedding from natural numbers to a cell type α together with a volume function on cells that is required to be non-negative on the image of the embedding. The associated Riemann sum computes the weighted sum of observable values over the first n embedded cells using that volume weight. This sits inside the ClassicalBridge module whose module-level setting is coarse graining with an explicit embedding of ticks to cells and a cell volume weight. Upstream structures supply the discrete observables, including nuclear densities on φ-tiers and ledger factorizations that calibrate the J-cost underlying the summed quantities.
proof idea
Direct definition of the epsilon-N convergence criterion applied to the Riemann sum over the first n embedded cells with their volume weights. No lemmas are invoked; the body is the literal statement of the limit.
why it matters in Recognition Science
Supplies the convergence hypothesis required by the downstream discrete-to-continuum continuity definition, which states that if the coarse-grained Riemann sums of a divergence observable converge to a finite limit I then the divergence-form statement holds. It fills the scaffold step that connects discrete φ-ladder and ledger structures to continuum equations in the ClassicalBridge. The open question recorded in the downstream comment is to prove convergence for specific LNAL distributions.
scope and limits
- Does not prove existence of the limit I for any concrete observable.
- Does not restrict the cell type α beyond the non-negativity of volumes.
- Does not invoke the φ-ladder, eight-tick octave, or specific constants such as α^{-1}.
- Does not address convergence rates or error bounds.
Lean usage
def discrete_to_continuum_continuity {α : Type} (CG : CoarseGrain α) (div : α → ℝ) : Prop := ∃ I : ℝ, H_Convergence CG div Iformal statement (Lean)
22def H_Convergence (CG : CoarseGrain α) (f : α → ℝ) (I : ℝ) : Prop :=
proof body
Definition body.
23 ∀ ε > 0, ∃ N, ∀ n ≥ N, |RiemannSum CG f n - I| < ε
24
25/-- Discrete→continuum continuity: if the coarse-grained Riemann sums of a divergence observable
26 converge to a finite limit `I`, the divergence-form statement holds.
27
28 STATUS: SCAFFOLD — The existence of the limit I is a hypothesis.
29 TODO: Prove convergence for specific LNAL distributions. -/