stochasticProcessTypeCount
plain-language theorem explainer
Recognition Science enumerates exactly five canonical stochastic process types. Researchers modeling recognition fluctuations as stochastic J-cost dynamics would cite this result to fix the dimension of the process space. The types correspond to Markov chains, Brownian motion, Poisson processes, martingales, and Gaussian processes. The proof is a one-line decision procedure that exhausts the constructors via the derived finite type instance.
Claim. The set of stochastic process types has cardinality five: $|S| = 5$ where $S = $ {Markov chain, Brownian motion, Poisson process, martingale, Gaussian process}.
background
The module states that five canonical stochastic process types equal configDim D = 5. Recognition fluctuations are modeled as stochastic J-cost dynamics, with Brownian motion as random walk in J-space and the Markov property holding between successive ticks. The inductive type lists the five constructors explicitly and derives DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive type derives a Fintype instance, allowing exhaustive enumeration of the five constructors to confirm the cardinality.
why it matters
This cardinality feeds the stochastic processes certificate definition, which packages the five types for higher constructions. It realizes the module claim that the process types match configDim D = 5. In the Recognition Science setting it supports J-cost dynamics and tick-by-tick Markov dependence without invoking the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.