pith. machine review for the scientific record. sign in
def definition def or abbrev high

nonlinearDynamicsCert

show as:
view Lean formalization →

The nonlinear dynamics certificate packages three RS-derived facts into one structure: exactly five bifurcation types, period-doubling reaching 8, and zero J-cost at unit scale. A physicist modeling chaos via recognition cost would cite this to anchor the period-doubling route in the RS framework. The definition assembles the three upstream theorems by direct field assignment with no further reasoning.

claimThe certificate asserts that the set of bifurcation types has cardinality 5, the period-doubling target equals 8, and the J-cost at argument 1 vanishes: $|BifurcationType|=5$, $periodDoublingTarget=8$, $Jcost(1)=0$.

background

In the Recognition Science treatment of nonlinear dynamics, chaos arises when J-cost exceeds the J(φ) threshold. The module identifies five canonical bifurcation types (saddle-node, pitchfork, transcritical, Hopf, period-doubling) that match configuration dimension 5, with period doubling proceeding through powers of 2 up to 2^3=8. The structure NonlinearDynamicsCert collects these properties into three named fields.

proof idea

The definition constructs an instance of NonlinearDynamicsCert by assigning its three fields directly from the sibling results bifurcationTypeCount, periodDoublingTarget_8, and equilibrium. Each assignment is a one-line reference to a prior theorem proved by decide or by the unit property of Jcost.

why it matters in Recognition Science

This definition supplies the certified properties of nonlinear dynamics required for the B11/B12 physics claims. It encodes the five bifurcation types together with the eight-tick period-doubling octave (T7) and the zero-equilibrium J-cost condition. No downstream uses are recorded, leaving open how the certificate integrates into larger dynamical models or simulations.

scope and limits

formal statement (Lean)

  42def nonlinearDynamicsCert : NonlinearDynamicsCert where
  43  five_bifurcations := bifurcationTypeCount

proof body

Definition body.

  44  eight_periods := periodDoublingTarget_8
  45  zero_equilibrium := equilibrium
  46
  47end IndisputableMonolith.Physics.NonlinearDynamicsFromRS

depends on (4)

Lean names referenced from this declaration's body.