`FEPBridgeLocalCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.FEPBridgeFromJCost
domain: Information
line: 129 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.FEPBridgeFromJCost on GitHub at line 129.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 126  rfl
 127
 128/-- A compact certificate for the theorem-grade part of the FEP bridge. -/
 129structure FEPBridgeLocalCert where
 130  exact_log_cost : ∀ u : ℝ, Jlog u = Real.cosh u - 1
 131  fisher_contact :
 132    Jlog 0 = klQuadratic 0 ∧
 133    deriv Jlog 0 = deriv klQuadratic 0 ∧
 134    deriv (deriv Jlog) 0 = deriv (deriv klQuadratic) 0
 135  blanket_boundary_shape :
 136    ∀ C : Coupling, HasMarkovBlanketSparsity C ↔ HasLedgerBoundarySparsity C
 137
 138/-- The local FEP/RS bridge certificate. -/
 139noncomputable def fepBridgeLocalCert : FEPBridgeLocalCert where
 140  exact_log_cost := jcost_log_exact
 141  fisher_contact := jcost_kl_same_second_order_at_equilibrium
 142  blanket_boundary_shape := markov_blanket_sparsity_iff_ledger_boundary_sparsity
 143
 144theorem fep_bridge_local_cert_holds : Nonempty FEPBridgeLocalCert :=
 145  ⟨fepBridgeLocalCert⟩
 146
 147end
 148end FEPBridgeFromJCost
 149end Information
 150end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.