pith. machine review for the scientific record. sign in
def definition def or abbrev high

J_log

show as:
view Lean formalization →

J_log re-expresses J-cost in additive log coordinates by the substitution J_log(ε) = Jcost(exp(ε)). Workers deriving the Regge action from the simplicial ledger cite it to obtain the quadratic Laplacian form needed for the continuum limit. The definition is the direct composition that yields cosh(ε) − 1.

claim$J_ {log} : ℝ → ℝ$ is given by $J_{log}(ε) = J(e^ε)$ where $J(x) = (x + x^{-1})/2 - 1$. This equals $cosh(ε) - 1$.

background

The ContinuumBridge module links the discrete J-cost on the simplicial ledger to the Regge action that converges to the Einstein field equations. J-cost is the functional $J(x) = (x + x^{-1})/2 - 1$ whose unique minimum at $x=1$ enforces discreteness (T5). In log coordinates $ε = ln ψ$ the coupling between neighboring simplices is $J(exp(ε_1 - ε_2)) = (ε_1 - ε_2)^2/2 + O((ε_1 - ε_2)^4)$, which is the discrete Laplacian action.

proof idea

The definition is a one-line wrapper that applies the upstream Jcost functional to the exponential map. It composes directly with the identity supplied by DiscretenessForcing.J_log.

why it matters in Recognition Science

This definition supplies the log form used by discreteness_forcing_principle and the quadratic-bound theorems in DiscretenessForcing. It fills the step in the module chain SimplicialLedger.J_global → log expansion → discrete Laplacian → Regge action → EFE. It implements T5 J-uniqueness in additive coordinates and supports the RCL composition law.

scope and limits

formal statement (Lean)

  67def J_log (ε : ℝ) : ℝ := Jcost (Real.exp ε)

proof body

Definition body.

  68
  69/-- The quadratic approximation of J in log coordinates. -/

used by (27)

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

depends on (6)

Lean names referenced from this declaration's body.