StochasticProcessType
plain-language theorem explainer
Five stochastic process types are defined inductively to realize configuration dimension D = 5 in Recognition Science. Researchers deriving stochastic J-cost dynamics from recognition fluctuations cite this enumeration when modeling Brownian motion as random walks in J-space or enforcing the Markov property across successive ticks. The inductive construction directly supplies the finite set whose cardinality is later certified by decision.
Claim. The type of stochastic processes is the inductive type whose five constructors are Markov chain, Brownian motion, Poisson process, martingale, and Gaussian process, equipped with decidable equality and finite cardinality.
background
In Recognition Science, recognition fluctuations are modeled as stochastic J-cost dynamics. Brownian motion arises as a random walk in J-space, and the Markov property requires that the recognition state at tick k+1 depends only on the state at tick k. The module therefore enumerates five canonical process types to match configDim D = 5.
proof idea
The definition is given directly as an inductive type with five constructors; DecidableEq, Repr, BEq, and Fintype instances are derived automatically by the compiler.
why it matters
This definition supplies the finite set whose cardinality is asserted to be exactly 5 in the downstream structure StochasticProcessesCert and the theorem stochasticProcessTypeCount. It realizes the discrete configuration space required for the Recognition Science derivation of stochastic processes from J-cost fluctuations, aligning with the five-dimensional configDim stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.