module module high

`IndisputableMonolith.Information.FEPBridgeFromJCost`

This module defines the local quadratic proxy for KL divergence in one log-ratio coordinate via the J-cost framework. It supplies the explicit definitions and derivative lemmas that link J-cost to the information term in variational calculations. Researchers applying Recognition Science to free-energy methods would cite it to justify the second-order equivalence at equilibrium. The module proceeds through a chain of definitions for the proxy and exact log expressions followed by direct verification of vanishing value and first derivatives.

claimThe local quadratic proxy for KL divergence in the single log-ratio coordinate $ell$ is $kappa(ell) = frac12 ell^2$, satisfying $kappa(0)=0$ and agreeing with the exact J-cost log expression to second order at equilibrium.

background

The module resides in the Information domain of Recognition Science and imports the Cost module, which supplies the J-cost function used throughout the framework. It introduces the quadratic proxy for KL divergence together with auxiliary functions that record the exact log-ratio expression and its derivatives. The local theoretical setting is the construction of an information bridge that approximates the KL term appearing in variational free energy while remaining inside the J-cost formalism.

proof idea

The module opens with definitions of the quadratic proxy, the exact J-cost log expression, and several derivative operators. It then applies standard calculus lemmas to establish that the proxy vanishes at equilibrium, that its first derivative is zero there, and that the second derivatives of the proxy and the exact expression coincide. Each property is obtained by direct differentiation and evaluation at the fixed point.

why it matters in Recognition Science

This module supplies the J-cost to KL bridge imported by the Information aggregator and by VariationalFreeEnergyFromRCL. The latter implements the Friston variational free energy $F[q;p] = E_q[E] + KL[q || p_prior]$ with monotone descent under ledger updates. It therefore completes the local approximation step required to embed information-theoretic quantities inside the Recognition Science foundation.

scope and limits

Does not derive global bounds or error estimates for the KL divergence.
Does not address multi-dimensional or continuous state spaces.
Does not invoke the Recognition Composition Law directly.
Does not supply numerical implementations or simulation examples.

used by (2)

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

IndisputableMonolith.Information module_import
IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (16)

def klQuadratic L34
theorem jcost_log_exact L37
theorem klQuadratic_zero L42
theorem hasDerivAt_klQuadratic L46
theorem deriv_klQuadratic_zero L55
theorem hasDerivAt_deriv_klQuadratic_zero L59
theorem hasDerivAt_deriv_Jlog_zero L68
theorem jcost_kl_same_second_order_at_equilibrium L79
inductive FEPStateClass L94
abbrev Coupling L102
def HasMarkovBlanketSparsity L107
def HasLedgerBoundarySparsity L114
theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity L124
structure FEPBridgeLocalCert L129
def fepBridgeLocalCert L139
theorem fep_bridge_local_cert_holds L144