zero_field_converges
The theorem establishes that the zero observable satisfies discrete-to-continuum continuity for any coarse graining structure CG on a type α. Researchers modeling continuum limits from discrete embeddings would cite it to anchor the trivial baseline case. The proof supplies an explicit witness I = 0 and verifies the convergence condition by direct simplification of the associated Riemann sum to zero.
claimLet $CG$ be a coarse graining structure on a type $α$, with embedding $embed : ℕ → α$ and volume $vol : α → ℝ$. Then the zero function on $α$ satisfies discrete-to-continuum continuity: there exists $I ∈ ℝ$ such that the Riemann sums of the zero observable converge to $I$ under the $H_Convergence$ predicate.
background
The module defines coarse graining via the structure CoarseGrain α, which supplies an explicit embedding of natural-number ticks into cells together with a nonnegative volume weight on each cell. The associated RiemannSum CG f n is the finite sum over the first n embedded cells of f(embed i) multiplied by the cell volume. The predicate discrete_to_continuum_continuity CG div asserts existence of a real limit I such that H_Convergence CG div I holds for the given observable div. The local setting is an explicit bridge from discrete ticks to continuum statements via weighted Riemann sums.
proof idea
The term-mode proof constructs the witness I = 0 directly. For arbitrary ε > 0 it selects N = 1. For every n ≥ 1 the Riemann sum of the zero function is identically zero, which lies below ε. Simplification of the RiemannSum definition yields the required inequality without further lemmas.
why it matters in Recognition Science
The declaration supplies the constructive witness for the zero observable, replacing a vacuous existence claim inside the discrete-to-continuum continuity predicate. It anchors the trivial case in the ClassicalBridge module and supports the broader forcing-chain development of continuum limits from discrete structures. No downstream theorems are recorded, but the result closes the zero-field baseline required for any later non-trivial convergence statements.
scope and limits
- Does not prove convergence for any non-zero observable.
- Does not supply rates or explicit error bounds beyond the ε-N definition.
- Does not define or discharge the H_Convergence predicate.
- Does not address specific physical distributions or LNAL models.
formal statement (Lean)
36theorem zero_field_converges {α : Type} (CG : CoarseGrain α) :
37 discrete_to_continuum_continuity CG (fun _ => 0) := by
proof body
Term-mode proof.
38 use 0
39 intro ε hε
40 use 1
41 intro n _hn
42 simp [RiemannSum]
43 exact hε
44
45end ClassicalBridge
46end IndisputableMonolith