def definition def or abbrev

`cascadeIterate`

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

formal statement (Lean)

 154def cascadeIterate {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 155    ℕ → Finset (Fin n)
 156  | 0     => L
 157  | k + 1 => cascadeStep E (cascadeIterate E L k)
 158

used by (7)

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

cascadeIterate_card_monotone in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
cascadeIterate_subset in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
cascadeIterate_subset_initial in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
cascadeIterate_succ in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
cascadeIterate_zero in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
ExtinctionCascadeCert in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
extinction_cascade_one_statement in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use

depends on (5)

Lean names referenced from this declaration's body.

cascadeStep in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
Ecosystem in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy decl_use
E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use