ContinuityEquation
ContinuityEquation supplies a structure schema for the continuum continuity equation in divergence form. Researchers deriving conservation laws from discrete tick models cite it when passing to the classical limit. The definition is a direct packaging of a single propositional field asserting finite convergence of coarse-grained Riemann sums.
claimLet $α$ be a type. The continuity equation in divergence form is the proposition that coarse-grained Riemann sums converge to a finite limit.
background
The module CoarseGrain develops an explicit embedding of discrete ticks into cells together with cell-volume weights. Sibling definitions supply the RiemannSum construction for the discrete approximation and the H_Convergence predicate for the limiting process. The local setting therefore treats the continuum limit as the target of a coarse-graining map whose convergence is asserted by the divergence_form field.
proof idea
The declaration is a structure definition containing one field of type Prop. No lemmas are applied; the construction simply names the required proposition.
why it matters in Recognition Science
The structure provides the target statement schema for the continuum continuity equation inside the ClassicalBridge. It is referenced by sibling results such as discrete_to_continuum_continuity when the discrete model is shown to recover the classical divergence form. In the Recognition framework this step closes the passage from the eight-tick octave to continuum conservation laws.
scope and limits
- Does not derive the divergence form from the Recognition Composition Law.
- Does not construct the explicit tick-to-cell embedding map.
- Does not address convergence rates or error bounds.
- Does not connect to the phi-ladder or mass formulas.
formal statement (Lean)
18structure ContinuityEquation (α : Type) where
19 divergence_form : Prop
20
21/-- **HYPOTHESIS**: Coarse-grained Riemann sums converge to a finite limit. -/