structure definition def or abbrev

`LocalComposition`

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

formal statement (Lean)

  39structure LocalComposition (L : ZeroParameterLedger) where
  40  compose : ℕ → ℝ
  41  compose_from_levels : ∀ k, compose k = L.levels k / L.levels (k + 1)
  42  compose_positive : ∀ k, 0 < compose k
  43

used by (1)

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

binary_is_minimal in IndisputableMonolith.Foundation.LocalityFromLedger decl_use

depends on (4)

Lean names referenced from this declaration's body.

compose in IndisputableMonolith.Ethics.VirtueComposition decl_use
ZeroParameterLedger in IndisputableMonolith.Foundation.LocalityFromLedger decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use