StochasticProcessesCert
plain-language theorem explainer
The declaration defines a certificate structure asserting that exactly five stochastic process types exist in the Recognition Science model of fluctuations. Physicists deriving Brownian motion as random walks in J-space or Markov chains from tick-dependent recognition would reference this to fix the discrete basis set. The structure is introduced directly with a cardinality field that is later instantiated by counting the constructors of the inductive type.
Claim. Let $S$ be the inductive type with constructors for the Markov chain, Brownian motion, Poisson process, martingale, and Gaussian process. StochasticProcessesCert is the structure whose sole field requires that the cardinality of $S$ equals 5.
background
The module derives stochastic processes from Recognition Science by equating five process types to the configuration dimension D = 5. Recognition fluctuations correspond to stochastic J-cost dynamics, Brownian motion to random walks in J-space, and the Markov property to dependence only on the previous tick. The referenced inductive definition StochasticProcessType lists the five constructors markovChain, brownianMotion, poissonProcess, martingale, and gaussianProcess, and automatically derives Fintype and related structures.
proof idea
The declaration introduces a structure type with a single field five_types requiring Fintype.card StochasticProcessType = 5. No proof steps or lemmas are involved; it is a bare structure definition whose field is satisfied by the downstream instantiation that computes the cardinality directly from the inductive type.
why it matters
This definition supplies the discrete count of five process types that realizes the Recognition Science identification of configDim D = 5. It is used by the definition stochasticProcessesCert to provide the concrete instance. Within the framework, the five types support modeling of recognition as stochastic J-cost dynamics and connect to the forcing chain landmarks including the eight-tick octave and spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.