IndisputableMonolith.Information.FEPBridgeFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# FEP Bridge from J-Cost
   6
   7This module is the first Lean anchor for comparing Recognition Science with
   8Friston-style free-energy-principle (FEP) mechanics.
   9
  10The result is deliberately local.  FEP uses KL / variational free energy,
  11while RS uses the reciprocal cost
  12
  13`J(x) = (x + x⁻¹) / 2 - 1`.
  14
  15In log-ratio coordinates `x = exp u`, RS gives `J(exp u) = cosh u - 1`.
  16Therefore the local quadratic contact with the Fisher/KL geometry is exact
  17at the level of value, first derivative, and second derivative at equilibrium.
  18
  19This does not yet derive Markov blankets or Bayesian filtering from RCL.  It
  20marks the theorem-grade part of the bridge and names the remaining structure.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Information
  25namespace FEPBridgeFromJCost
  26
  27open Cost
  28
  29noncomputable section
  30
  31/-! ## Local KL / Fisher Contact -/
  32
  33/-- The local quadratic proxy for KL divergence in one log-ratio coordinate. -/
  34noncomputable def klQuadratic (u : ℝ) : ℝ := u ^ 2 / 2
  35
  36/-- In log coordinates, reciprocal J-cost is exactly `cosh u - 1`. -/
  37theorem jcost_log_exact (u : ℝ) :
  38    Jlog u = Real.cosh u - 1 :=
  39  Jlog_as_cosh u
  40
  41/-- The KL quadratic has zero value at equilibrium. -/
  42@[simp] theorem klQuadratic_zero : klQuadratic 0 = 0 := by
  43  simp [klQuadratic]
  44
  45/-- The KL quadratic has zero first derivative at equilibrium. -/
  46theorem hasDerivAt_klQuadratic (u : ℝ) :
  47    HasDerivAt klQuadratic u u := by
  48  unfold klQuadratic
  49  have hsq : HasDerivAt (fun v : ℝ => v ^ 2) (2 * u) u := by
  50    simpa using (hasDerivAt_pow 2 u)
  51  have h := hsq.div_const 2
  52  convert h using 1
  53  ring
  54
  55@[simp] theorem deriv_klQuadratic_zero : deriv klQuadratic 0 = 0 := by
  56  simpa using (hasDerivAt_klQuadratic 0).deriv
  57
  58/-- The second derivative of the KL quadratic at equilibrium is `1`. -/
  59theorem hasDerivAt_deriv_klQuadratic_zero :
  60    HasDerivAt (deriv klQuadratic) 1 0 := by
  61  have h_eq : deriv klQuadratic = fun u : ℝ => u := by
  62    funext u
  63    exact (hasDerivAt_klQuadratic u).deriv
  64  rw [h_eq]
  65  simpa using (hasDerivAt_id 0)
  66
  67/-- The second derivative of log-coordinate J-cost at equilibrium is `1`. -/
  68theorem hasDerivAt_deriv_Jlog_zero :
  69    HasDerivAt (deriv Jlog) 1 0 := by
  70  have h_eq : deriv Jlog = Real.sinh := by
  71    funext u
  72    exact (hasDerivAt_Jlog u).deriv
  73  rw [h_eq]
  74  simpa using (Real.hasDerivAt_sinh 0)
  75
  76/-- RS reciprocal cost and the KL quadratic have the same Fisher curvature
  77at equilibrium.  This is the exact local crossover with FEP-style free energy.
  78-/
  79theorem jcost_kl_same_second_order_at_equilibrium :
  80    Jlog 0 = klQuadratic 0 ∧
  81    deriv Jlog 0 = deriv klQuadratic 0 ∧
  82    deriv (deriv Jlog) 0 = deriv (deriv klQuadratic) 0 := by
  83  constructor
  84  · simp [Jlog_zero]
  85  constructor
  86  · simp
  87  · have hJ := hasDerivAt_deriv_Jlog_zero.deriv
  88    have hK := hasDerivAt_deriv_klQuadratic_zero.deriv
  89    rw [hJ, hK]
  90
  91/-! ## Markov-Blanket Scaffold -/
  92
  93/-- The four FEP state classes in the particular partition. -/
  94inductive FEPStateClass where
  95  | external
  96  | sensory
  97  | active
  98  | internal
  99  deriving DecidableEq, Repr, BEq, Fintype
 100
 101/-- A sparse coupling relation between FEP state classes. -/
 102abbrev Coupling := FEPStateClass → FEPStateClass → Prop
 103
 104/-- The FEP Markov-blanket sparsity condition: no direct internal-external
 105coupling in either direction.  Coupling must pass through sensory/active
 106boundary states. -/
 107def HasMarkovBlanketSparsity (C : Coupling) : Prop :=
 108  ¬ C FEPStateClass.internal FEPStateClass.external ∧
 109  ¬ C FEPStateClass.external FEPStateClass.internal
 110
 111/-- Recognition-ledger boundary condition with the same sparse-coupling shape.
 112This is the RS-side object that future work must derive from RCL/ledger forcing,
 113instead of assuming as a partition. -/
 114def HasLedgerBoundarySparsity (C : Coupling) : Prop :=
 115  ¬ C FEPStateClass.internal FEPStateClass.external ∧
 116  ¬ C FEPStateClass.external FEPStateClass.internal
 117
 118/-- The current bridge between FEP blankets and RS ledger boundaries is a
 119shape theorem: the two sparsity predicates are definitionally the same.
 120
 121The hard follow-on is deriving `HasLedgerBoundarySparsity` from RCL/J-cost
 122dynamics for a concrete recognition field.
 123-/
 124theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity (C : Coupling) :
 125    HasMarkovBlanketSparsity C ↔ HasLedgerBoundarySparsity C := by
 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
 151