Pith. sign in
module module high

IndisputableMonolith.Cost.JcostCore

show as:
view Lean formalization →

The JcostCore module defines the J-cost function J(x) = ½(x + x⁻¹) - 1 together with its symmetry, non-negativity, and derivative identities. Modules on Hamiltonian emergence, frequency ladders, R-hat fixed points, and moral debt import it as the base cost object. It consists of a short collection of definitions and elementary lemmas derived directly from the functional form.

claimThe central object is the J-cost $J(x) := \frac12(x + x^{-1}) - 1$ for $x > 0$, obeying the derivative identity $J'(x) = \frac12 - \frac{1}{2x^2}$ together with the elementary properties $J(1/x) = J(x)$ and $J(x) \ge 0$ with equality only at $x=1$.

background

Recognition Science places the J-cost in the Cost domain as the canonical measure of ratio deviation. The module imports only Mathlib and introduces the core function Jcost along with the interface CostRequirements. Sibling declarations establish Jcost_symm, Jcost_nonneg, Jcost_eq_sq, and the derivative formula quoted in the module header.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

JcostCore supplies the base identities required by JCostGeometry (F1 log-domain geometry), HamiltonianEmergence (quadratic small-deviation limit), FrequencyLadder (phi-ladder bridge), RHatFixedPoint (contraction fixed-point theory), TuringBridge (R-hat landscape), and MoralDebt (externalization criterion).

scope and limits

used by (22)

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

declarations in this module (22)