Encyclopedia Gravity Gravity Continuum Manifold Emergence Jcost Neighbor Is Laplacian
ARTICLE 2 claims 2 theorems
Gravity Continuum Manifold Emergence Jcost Neighbor Is Laplacian
On a discrete lattice, a specific cost function for neighboring sites behaves, in the limit of small differences, exactly like the Laplacian operator of calculus.
The neighbor cost as a Laplacian
The Laplacian is a central object in physics and mathematics: it measures how a quantity at a point differs from the average of its surroundings. On a discrete lattice, the natural analogue compares a value at a site with the values at its immediate neighbors. The Recognition Science declaration jcost_neighbor_is_laplacian establishes that a particular cost function, derived from the framework's fundamental cost J, reproduces this discrete Laplacian structure.
The theorem states a precise bound. For a field f on a three-dimensional lattice, and for a site x where the differences to all six neighboring sites are small (each less than 1 in absolute value), the neighbor cost is close to the sum of squared differences divided by 2. The error is bounded by a term proportional to the fourth power of those differences. This is the signature of a Laplacian: the leading quadratic term, with corrections that vanish as the differences shrink.
This result is a consequence of a more general fact about the cost function J. Near the point where its argument equals 1, J behaves quadratically: J(1+ε) is approximately ε²/2. The theorem jcost_is_euclidean_metric makes this precise, bounding the difference by |ε|⁴/20. The neighbor Laplacian result applies this local quadratic behavior to each pair of neighboring sites.
In Recognition Science, this is a step in a larger argument. The framework models spacetime as emerging from a discrete ledger of recognition events. This theorem provides the bridge from the discrete cost to the continuous Laplacian operator, which appears in the classical equations of physics. The result is unconditional: it holds for any field satisfying the small-difference condition, with no further assumptions.
What the theorem does not claim is equally important. It does not assert that the discrete lattice is a manifold, nor that the Laplacian here is the full curved-space Laplacian of general relativity. It establishes the local quadratic structure on a flat, three-dimensional lattice. The passage from this discrete Laplacian to a curved Lorentzian manifold, and ultimately to the Einstein equations, is a separate and conditional step in the framework's program.
THEOREM jcost_neighbor_is_laplacian · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.lean
/-- The J-cost on neighbor pairs gives the lattice Laplacian (from ContinuumLimit). -/
theorem jcost_neighbor_is_laplacian (f : LatticeField 3) (x : Fin 3 → ℤ)
(h_small : ∀ k : Fin 3,
|f (shift_plus k x) - f x| < 1 ∧ |f (shift_minus k x) - f x| < 1) :
|neighbor_cost f x -
∑ k : Fin 3, ((f (shift_plus k x) - f x) ^ 2 / 2 +
(f (shift_minus k x) - f x) ^ 2 / 2)| ≤
∑ k : Fin 3, (|f (shift_plus k x) - f x| ^ 4 / 20 +
|f (shift_minus k x) - f x| ^ 4 / 20) :=
jcost_gives_laplacian_structure f x h_small
THEOREM jcost_is_euclidean_metric · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.lean
/-- **THEOREM (J-Cost = Metric)**: J-cost is quadratic at leading order.
The quadratic form ε²/2 IS the Euclidean distance-squared in log-ratio space. -/
theorem jcost_is_euclidean_metric (ε : ℝ) (hε : |ε| < 1) :
|J_log ε - ε ^ 2 / 2| ≤ |ε| ^ 4 / 20 :=
jcost_quadratic_leading ε hε
What this page does not claim
The theorem does not establish that the discrete lattice is a smooth manifold. The theorem does not derive the curved-space Laplacian of general relativity. The theorem does not by itself force the Einstein equations; that requires additional, conditional steps.
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/Gravity/ContinuumManifoldEmergence.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:
- How does the discrete Laplacian on a finite lattice converge to the continuous Laplacian as the number of sites grows?
- What conditions are required for the passage from a flat lattice Laplacian to a curved spacetime metric?
- How does the framework derive the Einstein equations from the defect-induced curvature of the discrete ledger?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM jcost_neighbor_is_laplacian · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.lean
/-- The J-cost on neighbor pairs gives the lattice Laplacian (from ContinuumLimit). -/ theorem jcost_neighbor_is_laplacian (f : LatticeField 3) (x : Fin 3 → ℤ) (h_small : ∀ k : Fin 3, |f (shift_plus k x) - f x| < 1 ∧ |f (shift_minus k x) - f x| < 1) : |neighbor_cost f x - ∑ k : Fin 3, ((f (shift_plus k x) - f x) ^ 2 / 2 + (f (shift_minus k x) - f x) ^ 2 / 2)| ≤ ∑ k : Fin 3, (|f (shift_plus k x) - f x| ^ 4 / 20 + |f (shift_minus k x) - f x| ^ 4 / 20) := jcost_gives_laplacian_structure f x h_smallThe neighbor cost is close to the sum of squared differences divided by 2, with an error bounded by a term proportional to the fourth power of those differences. jcost_neighbor_is_laplacian · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.leanTHEOREM jcost_is_euclidean_metric · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.lean
/-- **THEOREM (J-Cost = Metric)**: J-cost is quadratic at leading order. The quadratic form ε²/2 IS the Euclidean distance-squared in log-ratio space. -/ theorem jcost_is_euclidean_metric (ε : ℝ) (hε : |ε| < 1) : |J_log ε - ε ^ 2 / 2| ≤ |ε| ^ 4 / 20 := jcost_quadratic_leading ε hεNear the point where its argument equals 1, J behaves quadratically: J(1+ε) is approximately ε²/2. jcost_is_euclidean_metric · IndisputableMonolith/Gravity/ContinuumManifoldEmergence.lean