pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge

show as:
view Lean formalization →

The ContinuumBridge module supplies the logarithmic translation of J-cost for connecting simplicial 3-complex ledgers to continuum curvature expressions in Recognition Science. Researchers formalizing the field-curvature identity cite it when passing between discrete edge lengths and field equations. It consists of targeted definitions that convert the multiplicative J form into the additive cosh expression without a central theorem.

claimThe recognition cost in logarithmic coordinates satisfies $J(e^{\epsilon}) = \cosh(\epsilon) - 1$.

background

This module belongs to the Foundation.SimplicialLedger hierarchy and imports Constants (where $\tau_0 = 1$ tick), Cost, and the base SimplicialLedger module. The latter formalizes the ledger as a simplicial 3-complex with a coordinate-free sheaf representation that unifies local and global J-cost variations.

The supplied DOC_COMMENT isolates the key translation: edge lengths are written in exponential form so that the original J functional becomes an additive function of $\epsilon$. This step aligns the discrete ledger with continuum limits while preserving the Recognition Composition Law.

Upstream results from Constants and Cost fix the native units and the base J definition used throughout the downstream phases.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the logarithmic J-cost bridge required by ContinuumTheorem, which advances Phase D of the program to make the paper's Theorem 5.1 (field-curvature identity at $\kappa = \kappa_{Einstein}$) an unconditional Lean theorem. It is also imported by CubicDeficitDischarge (Phase A), CubicSimplicialEquivalence, NonlinearBridge, and InteriorFlat, each addressing a distinct Beltracchi concern on the Regge identification.

scope and limits

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (26)