stochasticProcessesCert
plain-language theorem explainer
The definition certifies that the finite set of stochastic process types has cardinality exactly 5, matching the configuration dimension in the RS model. Researchers modeling recognition fluctuations as J-cost dynamics would cite it to link canonical processes such as Markov chains and Brownian motion to the recognition framework. It is assembled as a direct field assignment from the decidable count of enumerated types.
Claim. The certificate asserts that the cardinality of the type of stochastic process types equals 5: $Fintype.card(StochasticProcessType)=5$.
background
The module treats five canonical stochastic process types (Markov chain, Brownian motion, Poisson process, martingale, Gaussian process) as equal to configDim D=5. Recognition fluctuations are identified with stochastic J-cost dynamics; Brownian motion appears as a random walk in J-space and the Markov property requires that recognition at tick k+1 depends only on the state at tick k.
proof idea
One-line wrapper that assigns the result of the upstream theorem stochasticProcessTypeCount directly to the five_types field of the StochasticProcessesCert structure.
why it matters
The definition supplies the concrete witness required by the StochasticProcessesCert structure, completing the module's claim that exactly five process types arise from RS recognition fluctuations. It supports the framework's assignment of configDim D=5 to stochastic classification while remaining separate from the spatial dimension D=3 fixed by the forcing chain. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.