def
definition
nonlinearDynamicsCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.NonlinearDynamicsFromRS on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
39 eight_periods : periodDoublingTarget = 8
40 zero_equilibrium : Jcost 1 = 0
41
42def nonlinearDynamicsCert : NonlinearDynamicsCert where
43 five_bifurcations := bifurcationTypeCount
44 eight_periods := periodDoublingTarget_8
45 zero_equilibrium := equilibrium
46
47end IndisputableMonolith.Physics.NonlinearDynamicsFromRS