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

IndisputableMonolith.Foundation.JCostHessianC7

show as:
view Lean formalization →

JCostHessianC7 isolates the exact quadratic numerator of the local J-cost expansion around the fixed point at unity. Equilibrium modelers cite the module when they need the invariant quadratic coefficient 1/2 and Hessian coefficient 1 that every RS equilibrium inherits from the same kernel. The module consists of a short chain of definitions and equality lemmas built directly on the J-cost imported from the Cost module.

claimThe local J-cost expansion has quadratic numerator $(x-1)^2$ and coefficient $1/2$, with Hessian coefficient $1$.

background

Recognition Science derives equilibria from the J-function obeying the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The Cost module supplies the concrete J-cost kernel. This module extracts only the local Taylor behavior of that kernel near $x=1$, where the first derivative vanishes and the second derivative equals 1.

proof idea

This is a definition module. It introduces jcost_local_quadratic_kernel and jcostHessianCoefficient, then supplies the equality lemmas jcostHessianCoefficient_eq_one and jcostTaylorQuadraticCoefficient_eq that fix the coefficients at the stated values.

why it matters in Recognition Science

The module supplies the shared local J-kernel required by UniversalEquilibriumResponseC7. That file uses the quadratic coefficient 1/2 and Hessian coefficient 1 to establish the common core behind the claim that Nash, market, and health equilibria coincide at r=1. The empirical cross-field sensitivity comparison is left to later work.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)