module module high

`IndisputableMonolith.Information.FEPBridgeFromJCost`

The module supplies the local quadratic proxy for KL divergence in a single log-ratio coordinate, derived from J-cost. Researchers building the information bridge to variational free energy in Recognition Science cite these results when linking ledger costs to the KL term. The module consists of definitions for the proxy together with lemmas on its first and second derivatives that confirm agreement at equilibrium.

claimThe local quadratic proxy for KL divergence is the function $q(x)$ in the log-ratio coordinate $x$ satisfying $q(1)=0$, $q'(1)=0$, and $q''(1)$ matching the second derivative of the exact KL at equilibrium.

background

The module sits in the Information domain and imports the Cost module, which defines the J-cost function obeying the Recognition Composition Law. Its central construction is the quadratic proxy klQuadratic for KL divergence together with its derivatives. The downstream VariationalFreeEnergyFromRCL module uses this proxy inside the Friston functional $F[q;p]=\mathbb{E}q[E]+\mathrm{KL}[q||p\mathrm{prior}]$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Information aggregator that assembles the information-theoretic foundation of Recognition Science and supplies the KL quadratic proxy required by VariationalFreeEnergyFromRCL. It thereby connects J-cost ledger coordinates to the free-energy descent property.

scope and limits

Does not supply global error bounds away from equilibrium.
Does not treat multi-dimensional or non-log-ratio coordinates.
Does not derive the monotone descent of the free energy itself.
Does not reference the phi-ladder or spatial dimension D=3.

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