def definition def or abbrev

`phi`

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

formal statement (Lean)

  50def phi {M : RecognitionStructure} (L : Recognition.Ledger M) : M.U → ℤ :=

Definition body.

  51  Recognition.phi L
  52
  53/-- Re-export: Chain flux. -/

Lean names referenced from this declaration's body.

Chain in IndisputableMonolith.Chain decl_use
RecognitionStructure in IndisputableMonolith.Chain decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
RecognitionStructure in IndisputableMonolith.Foundation.RecognitionForcing decl_use
Chain in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition decl_use
RecognitionStructure in IndisputableMonolith.Recognition decl_use
U in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
Chain in IndisputableMonolith.RRF.Core.Recognition decl_use
RecognitionStructure in IndisputableMonolith.RRF.Core.Recognition decl_use
RecognitionStructure in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use