`FEPStateClass`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.FEPBridgeFromJCost on GitHub at line 94.

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

  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) :

papers checked against this theorem

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