CoarseGrain
plain-language theorem explainer
CoarseGrain defines a structure that embeds natural-number ticks into cells of type α while assigning nonnegative real volumes to those cells. Researchers deriving continuum limits from discrete Recognition Science models cite this interface when constructing Riemann sums and convergence statements. The declaration is a bare structure with three fields and no further computational content.
Claim. A structure CoarseGrain($α$) consisting of an embedding map embed : $ℕ → α$, a volume function vol : $α → ℝ$, and the nonnegativity axiom ∀ i, 0 ≤ vol(embed i).
background
The ClassicalBridge module supplies the interface between the foundational forcing chain and classical continuum statements. Coarse graining here uses an explicit embedding of ticks together with cell volumes to prepare Riemann sums. The embed field generalizes the orbit embedding from ArithmeticFromLogic, which recursively maps LogicNat into positive reals by repeated multiplication with a generator value. The vol field supplies weights whose nonnegativity is required for physical interpretation.
proof idea
The declaration is a structure definition that introduces the three fields directly with no lemmas or tactics applied.
why it matters
CoarseGrain supplies the type used by discrete_to_continuum_continuity to assert existence of a finite limit I for divergence observables, by H_Convergence to encode the convergence hypothesis, and by RiemannSum to define the partial sums. It therefore supports the discrete-to-continuum step that connects the eight-tick octave and phi-ladder constructions to classical equations. The structure remains open for concrete embeddings that would discharge the scaffolding in zero_field_converges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.