bifurcationTypeCount
plain-language theorem explainer
The theorem asserts that the Recognition Science model of nonlinear dynamics admits exactly five bifurcation types. A physicist tracing chaos to J-cost thresholds above J(φ) would cite this count to anchor the period-doubling route that reaches eight periods. The proof is a one-line term reduction that invokes the decide tactic on the Fintype instance derived by the inductive type.
Claim. The set of bifurcation types consisting of saddle-node, pitchfork, transcritical, Hopf, and period-doubling has cardinality five: $|$saddle-node, pitchfork, transcritical, Hopf, period-doubling$| = 5$.
background
The module treats chaotic dynamics as J-growth once recognition cost exceeds the J(φ) threshold, producing sensitive dependence on initial conditions. Five canonical bifurcation types are introduced as the inductive type with constructors saddle-node, pitchfork, transcritical, Hopf, and period-doubling; the module states that this enumeration equals configDim D = 5 and supports the period-doubling sequence 1 → 2 → 4 → 8 (= 2^3).
proof idea
The proof is a one-line term proof that applies the decide tactic to Fintype.card BifurcationType = 5. The inductive definition of BifurcationType derives Fintype, so decide evaluates the finite cardinality of the five constructors by direct computation.
why it matters
The result supplies the five_bifurcations field inside the nonlinearDynamicsCert definition that certifies the full nonlinear-dynamics package. It realizes the module claim that five types equal configDim D = 5 and links to the eight-tick octave (T7) through the period-doubling target of eight periods, closing the B11/B12 physics section with a proved statement free of axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.