discrete_to_continuum_continuity
A divergence observable on a coarse-grained space satisfies discrete-to-continuum continuity precisely when its Riemann sums converge to some finite limit I. Researchers deriving continuum field equations from discrete tick embeddings would cite this when establishing continuity of divergence forms. The definition is realized as an existential wrapper around the convergence hypothesis for Riemann sums.
claimLet $CG$ be a coarse-graining structure consisting of an embedding from natural numbers to cells together with nonnegative volume weights. For a divergence observable $div : α → ℝ$, the continuity condition holds if there exists a real number $I$ such that the Riemann sums of $div$ under $CG$ converge to $I$.
background
The CoarseGrain structure equips a type α with an embedding of natural-number ticks into cells and a volume weight function on cells, with the nonnegativity condition on volumes. The associated Riemann sum aggregates the observable values weighted by cell volumes over the first n embedded cells. H_Convergence states that the Riemann sums of an observable f converge to a limit I in the sense that for every positive ε there is an N beyond which the sums stay within ε of I. This definition appears in the module on coarse graining, which supplies an explicit tick-to-cell embedding and volume weights to connect discrete structures to continuum statements.
proof idea
The definition is a one-line wrapper that asserts the existence of a real number I for which the H_Convergence predicate holds on the coarse-graining CG and the divergence observable div.
why it matters in Recognition Science
This definition provides the continuity predicate invoked by the zero-field convergence theorem, which supplies a constructive witness by taking I equal to zero. It advances the classical bridge by formalizing the condition under which discrete Riemann sums yield a continuum divergence statement. The scaffold status highlights the open task of proving the required convergence for specific distributions arising in the LNAL framework.
scope and limits
- Does not prove the existence of the convergence limit I for arbitrary observables.
- Does not specify convergence rates or quantitative error estimates.
- Does not link the limit I to explicit values from the phi-ladder or forcing chain.
- Does not extend beyond the given coarse-graining structure to other embeddings.
formal statement (Lean)
30def discrete_to_continuum_continuity {α : Type}
31 (CG : CoarseGrain α) (div : α → ℝ) : Prop :=
proof body
Definition body.
32 ∃ I : ℝ, H_Convergence CG div I
33
34/-- **THEOREM**: Trivial convergence for zero field.
35 Replaces the vacuous `∃ I, True` with a constructive witness. -/