structure definition def or abbrev

`RecognitionOperator`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  38structure RecognitionOperator where
  39  evolve : LedgerState → LedgerState
  40  minimizes_J : ∀ s, admissible s → RecognitionCost (evolve s) ≤ RecognitionCost s
  41
  42/-- **DEFINITION: Ledger Entropy**
  43    Entropy defined as the absolute log-imbalance of the ledger. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

eight_tick_dissipation_limit in IndisputableMonolith.Information.Thermodynamics decl_use

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
LedgerState in IndisputableMonolith.Foundation.VariationalDynamics decl_use
LedgerState in IndisputableMonolith.Information.InformationIsLedger decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
admissible in IndisputableMonolith.Information.Thermodynamics decl_use
LedgerState in IndisputableMonolith.Information.Thermodynamics decl_use
RecognitionCost in IndisputableMonolith.Information.Thermodynamics decl_use
LedgerState in IndisputableMonolith.LedgerPostingAdjacency decl_use
LedgerState in IndisputableMonolith.QFT.GaugeInvariance decl_use
evolve in IndisputableMonolith.Thermodynamics.SecondLaw decl_use