pith. sign in
module module high

IndisputableMonolith.Cost.JcostCore

show as:
view Lean formalization →

JcostCore supplies the primitive definition of the J-cost function together with its algebraic properties and derivative. Workers on Hamiltonian emergence, R-hat fixed points, and the phi-ladder frequency bridge cite these identities as the starting point for quadratic approximations and contraction arguments. The module is organized as a collection of definitions and short lemmas establishing non-negativity, inversion symmetry, and the exact first derivative.

claim$J(x) := ½(x + x^{-1}) - 1$ for $x > 0$, satisfying $J'(x) = ½ - ½x^{-2}$.

background

Recognition Science adopts the reciprocal cost $J(x) = ½(x + x^{-1}) - 1$ as its fundamental scalar measure of deviation from equilibrium. The function is non-negative, vanishes only at $x = 1$, and is symmetric under inversion. Its derivative formula is recorded directly in the module header.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

JcostCore is imported by twenty-two downstream modules. It supplies the cost function for the Hamiltonian emergence result (quadratic limit near $x = 1$), the F1 log-domain geometry paper, R-hat fixed-point theory, and the moral-debt criterion that treats externalization of sigma as measurable injustice. It also feeds the Turing-bridge and frequency-ladder constructions.

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)