J_log_error_bound
The definition supplies the quartic remainder |ε|^4/24 that controls the error between the exact J-coupling J(e^ε) and its quadratic approximation ε²/2. Researchers deriving the Regge action from the simplicial ledger or passing to the Einstein equations in the continuum limit would cite this bound to justify truncation. It is a direct one-line transcription of the Lagrange remainder for cosh.
claimDefine the quartic remainder function by $b(ε) := |ε|^4 / 24$ for $ε ∈ ℝ$. For the J-cost $J(e^ε) = cosh(ε) - 1$, this bounds the remainder term in the expansion $J(e^ε) = ε²/2 + r(ε)$ with $|r(ε)| ≤ b(ε)$ whenever $|ε| < 1$.
background
The ContinuumBridge module establishes that J-cost stationarity on the simplicial ledger reproduces the Regge action and, in the continuum limit, the Einstein field equations. In log coordinates ε = ln ψ the coupling between neighboring simplices is J(e^(ε₁-ε₂)) = (ε₁-ε₂)²/2 + O((ε₁-ε₂)^4). The J-cost itself is the Recognition Science functional J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1, whose quadratic leading term yields a discrete Laplacian. Upstream structures such as PhiForcingDerived.of supply the algebraic properties of this J-cost, while ObserverForcing.cost and MultiplicativeRecognizerL4.cost embed it into recognition events and multiplicative comparators.
proof idea
One-line definition that directly encodes the standard Taylor remainder for cosh at order four. No lemmas are invoked; the expression |ε|^4/24 is the explicit Lagrange form of the remainder after the quadratic term.
why it matters in Recognition Science
The bound closes the error-control step in the derivation chain SimplicialLedger.J_global → log-coordinate expansion → discrete Laplacian → Regge action → κ = 8φ^5 normalization → continuum limit to the Einstein equations. It therefore supports the central claim of the module that J-cost stationarity is not an extra hypothesis but a theorem following from the quadratic structure of J. No downstream uses are recorded yet, but the definition is required for any rigorous passage from the discrete ledger to the continuum.
scope and limits
- Does not prove the Taylor theorem or derive the remainder from first principles.
- Does not impose or verify the restriction |ε| < 1 inside the definition.
- Does not normalize the bound by physical constants or φ-powers.
- Does not address higher-order terms or global convergence on the ledger.
formal statement (Lean)
75def J_log_error_bound (ε : ℝ) : ℝ := |ε| ^ 4 / 24
proof body
Definition body.
76
77/-! ## The Coupling Cost
78
79The cost of a mismatch between neighboring simplices. -/
80
81/-- The coupling cost between two simplices with log-potentials ε₁, ε₂.
82 J(ψ₁/ψ₂) = J(e^(ε₁−ε₂)) ≈ (ε₁−ε₂)²/2 at leading order. -/