`TrivialState`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Models.Trivial
domain: RRF
line: 24 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Models.Trivial on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  21/-! ## The Trivial Model -/
  22
  23/-- Trivial state space: a single point. -/
  24abbrev TrivialState := Unit
  25
  26/-- Trivial strain: always zero. -/
  27def trivialStrain : StrainFunctional TrivialState where
  28  J := fun _ => 0
  29
  30instance : StrainFunctional.NonNeg trivialStrain where
  31  nonneg := fun _ => le_refl 0
  32
  33/-- The single state is balanced. -/
  34theorem trivial_balanced : trivialStrain.isBalanced () := rfl
  35
  36/-- The single state is a minimizer. -/
  37theorem trivial_is_minimizer : trivialStrain.isMinimizer () :=
  38  StrainFunctional.equilibria_are_minimizers () trivial_balanced
  39
  40/-- Trivial ledger: zero debit and credit. -/
  41def trivialLedger : LedgerConstraint TrivialState where
  42  debit := fun _ => 0
  43  credit := fun _ => 0
  44
  45/-- Trivial ledger is closed. -/
  46theorem trivial_ledger_closed : trivialLedger.isClosed () := rfl
  47
  48/-- Trivial strain-ledger system. -/
  49def trivialStrainLedger : StrainLedger TrivialState where
  50  strain := trivialStrain
  51  ledger := trivialLedger
  52
  53/-- The trivial state is valid. -/
  54theorem trivial_is_valid : trivialStrainLedger.isValid () :=

papers checked against this theorem

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