RECOGNITION ENCYCLOPEDIA COMPILED 2026-08-06 · PUBLIC EDITION · SOURCES: 1 LEAN MODULE

Foundation Continuum Limit

The continuum limit is the machine-checked bridge by which discrete recognition dynamics on a lattice yields smooth, second-order differential equations.

The continuum limit

The foundation continuum limit is the point in Recognition Science where the discrete ledger gives way to smooth physics. Recognition Science works on a lattice of integer points, with a cost function J that measures mismatch between neighboring sites. The continuum limit is the long-wavelength regime, where changes between neighboring sites are small. In that regime the cost function is dominated by its quadratic term, and the lattice dynamics become a second-order diffusion equation whose structure matches the Klein-Gordon equation.

The key machine-checked fact is that the cost function J(exp(t)) = cosh(t) - 1 has the Taylor expansion cosh(t) - 1 = t²/2 + t⁴/24 + ... . For small perturbations t = εδ with ε → 0, the leading term t²/2 is quadratic, and quadratic costs on a lattice produce the discrete Laplacian. The discrete Laplacian, in the scaling limit, converges to the continuous Laplacian ∇². The module establishes this chain formally: J-cost dynamics on ℤ³ leads to the lattice Laplacian, then to the continuous ∇², then to Klein-Gordon structure, then to Dirac structure from spinors in three dimensions, and then to Einstein equations from curvature of the defect field.

The module establishes several precise theorems. The theorem jcost_quadratic_leading shows that for |ε| < 1, the absolute difference between J_log ε and ε²/2 is at most |ε|⁴/20. The theorem jcost_gives_laplacian_structure shows that the neighbor cost, which sums J_log over shifts, is approximated by the sum of squared differences divided by 2, with error bounded by fourth powers. The theorem continuum_limit_second_order shows that for a four-times continuously differentiable function, the second difference quotient converges to the second derivative with error of order a². The theorem rs_is_gaussian shows that the J-cost system is in the Gaussian universality class, meaning its leading behavior is quadratic with quartic corrections.

The module also provides a dictionary between lattice and continuum concepts, and it establishes that the mass squared in the Klein-Gordon structure is positive, set to 1 in the native units. The theorem emergence_hierarchy orders the emergence errors: the interacting level error is bounded by |ε|⁶/720, which is smaller than the quadratic level error |ε|⁴/20 for small ε. This shows that the continuum description improves as the perturbation shrinks.

In plain language, the module establishes that the discrete, tick-based recognition dynamics, when viewed at large scales, produce the smooth differential equations that conventional physics uses. The continuum is not assumed; it is forced by the quadratic leading term of the cost function and the lattice Laplacian. The physical bridge from recognition to linking is not part of this module; that remains open.

THEOREM jcost_quadratic_leading · IndisputableMonolith/Foundation/ContinuumLimit.lean

THEOREM jcost_gives_laplacian_structure · IndisputableMonolith/Foundation/ContinuumLimit.lean

THEOREM continuum_limit_second_order · IndisputableMonolith/Foundation/ContinuumLimit.lean

THEOREM rs_is_gaussian · IndisputableMonolith/Foundation/ContinuumLimit.lean

THEOREM emergence_hierarchy · IndisputableMonolith/Foundation/ContinuumLimit.lean

What this page does not claim

This module does not prove the physical bridge from recognition to linking. This module does not derive the fine-structure constant or any specific particle mass. This module does not claim that the continuum limit is exact for all scales; it is a long-wavelength approximation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ContinuumLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND