pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge

show as:
view Lean formalization →

The ContinuumBridge module supplies the logarithmic coordinate form of the J-cost, J(e^ε) = cosh(ε) − 1, converting discrete ledger costs into additive expressions suited to continuum analysis. Researchers building the field-curvature identity and simplicial-to-continuum maps cite it as the translation layer. The module consists of direct algebraic definitions and equivalences drawn from the base J-cost and the simplicial sheaf.

claim$J(e^ε) = cosh(ε) − 1$, where $J$ denotes the recognition cost and $ε$ the logarithmic deviation on the simplicial ledger.

background

The SimplicialLedger module formalizes the ledger as a simplicial 3-complex with a coordinate-free sheaf representation that unifies local and global J-cost variations. Constants supplies the RS time quantum τ₀ = 1 tick. The Cost module provides the base multiplicative definition of J. ContinuumBridge translates this into log coordinates so that discrete costs become compatible with continuum field and curvature expressions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds ContinuumTheorem (Phase D of the program to make the paper's Theorem 5.1, the field-curvature identity at κ = κ_Einstein, an unconditional Lean theorem) and supports CubicDeficitDischarge, CubicSimplicialEquivalence, NonlinearBridge, and related modules that address Beltracchi §§5–7. It supplies the log-coordinate bridge required for the discrete-to-continuum step in the Recognition framework.

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)