pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge

show as:
view Lean formalization →

Module that defines the J-cost in logarithmic coordinates via J(e^ε) = cosh(ε) - 1, supplying the nonlinear bridge between discrete simplicial ledgers and continuum descriptions. Researchers formalizing the field-curvature identity cite it for the log-coordinate foundation. It consists of targeted definitions and quadratic approximations that feed downstream continuum and discharge modules.

claimThe J-cost function in logarithmic coordinates satisfies $J(e^ε) = cosh(ε) - 1$.

background

The module sits inside the simplicial 3-complex formalization of the ledger. It imports the RS time quantum τ₀ = 1 tick, the J-cost definition, and the coordinate-free sheaf representation that unifies local and global J-cost variations. Log coordinates convert the multiplicative J-cost into an additive hyperbolic form that matches the continuum limit of the Recognition Composition Law.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It feeds ContinuumTheorem (Phase D toward unconditional Theorem 5.1), CubicDeficitDischarge, NonlinearBridge, and CubicSimplicialEquivalence. These modules address Beltracchi §5–§7 concerns and promote the draft paper's field-curvature identity from pattern-matching to Lean theorem. The log form supplies the exact nonlinear J-cost needed for the eight-tick octave and D = 3 spatial structure.

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)