def
definition
fepBridgeLocalCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Information.FEPBridgeFromJCost on GitHub at line 139.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
FEPBridgeLocalCert -
jcost_kl_same_second_order_at_equilibrium -
jcost_log_exact -
markov_blanket_sparsity_iff_ledger_boundary_sparsity
used by
formal source
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