theorem
proved
bifurcationTypeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.NonlinearDynamicsFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | saddleNode | pitchfork | transcritical | hopf | periodDoubling
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem bifurcationTypeCount : Fintype.card BifurcationType = 5 := by decide
29
30/-- Period-doubling reaches 2^3 = 8. -/
31def periodDoublingTarget : ℕ := 2 ^ 3
32theorem periodDoublingTarget_8 : periodDoublingTarget = 8 := by decide
33
34/-- At equilibrium: J = 0. -/
35theorem equilibrium : Jcost 1 = 0 := Jcost_unit0
36
37structure NonlinearDynamicsCert where
38 five_bifurcations : Fintype.card BifurcationType = 5
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