Pith. sign in
module module high

IndisputableMonolith.Foundation.JCostHessianC7

show as:
view Lean formalization →

This module supplies the exact quadratic numerator in the local J-cost expansion. It derives the Taylor quadratic coefficient of 1/2 and the Hessian coefficient of 1 from the base J-cost. Researchers modeling universal equilibria cite it to establish the shared kernel across domains. The module consists of supporting lemmas and a Hessian certificate built on the imported Cost definitions.

claimThe local J-cost expansion has quadratic term $\frac12 \delta^2$ with Hessian coefficient exactly 1 at equilibrium.

background

The upstream Cost module defines the J-cost via the recognition composition law and the function J(x) = (x + x^{-1})/2 - 1. This module introduces the local quadratic kernel, the Taylor quadratic coefficient, and the Hessian coefficient for expansions around equilibrium points. These objects formalize the quadratic behavior that any RS equilibrium inherits when modeled by the same local J-cost kernel.

proof idea

This is a definition module, no proofs. It contains a sequence of lemmas that establish the quadratic kernel, the Taylor coefficient, and the Hessian certificate directly from the imported Cost definitions.

why it matters in Recognition Science

This module feeds the Universal Equilibrium Response C7, which states that any RS equilibrium modeled by the local J-cost kernel inherits the quadratic coefficient 1/2 and Hessian coefficient 1. It supplies the formal common core behind the claim that Nash, market, and health equilibria share the same J-kernel at r = 1. The downstream module notes that empirical cross-field comparisons are not proved here.

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)