pith. sign in
module module high

IndisputableMonolith.Econ.MarketEquilibriumFromJCost

show as:
view Lean formalization →

The module Econ.MarketEquilibriumFromJCost applies the J-cost function to normalized price ratios p/p* to define deviation measures and equilibrium certificates. It supplies the basic objects needed to link price stability to the Recognition Science cost structure. Economists working inside the RS framework would cite these definitions when deriving equilibrium conditions from J-uniqueness. The module consists entirely of definitions and elementary properties with no complex proofs.

claimThe deviation of a price ratio is given by $d = J(p/p^*)$ where $J(x) = (x + x^{-1})/2 - 1$. Equilibrium holds when $d = 0$, with associated non-negativity, threshold, and certification structures.

background

The Recognition Science framework supplies the J-cost via the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ together with the explicit form $J(x) = (x + x^{-1})/2 - 1$. The Constants module fixes the base time unit as the tick with τ₀ = 1. This module extends the Cost definitions to economic prices by treating the ratio p/p* as the argument of J, thereby producing a deviation function and related equilibrium objects.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core objects (priceDeviation, MarketEquilibriumCert and their properties) that allow market equilibrium to be expressed directly in terms of J-cost. It thereby connects price dynamics to the J-uniqueness and self-similar fixed-point steps of the forcing chain. No downstream theorems are recorded yet, so the module functions as a foundational layer for subsequent economic derivations within Recognition Science.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)