Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-reachability-witness

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_reachability_witness.clj0 definitions, 2 theorems

Existential finite-horizon witnesses for exact-rational Markov support. This module deliberately does not choose a public reachability predicate. It packages the two canonical evidence constructors that such an API needs: zero steps witness reflexive support of a point mass, and one step witnesses support whenever the corresponding kernel entry is positive. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.markov-point-mass

markov/nnrat-positive-entry-iterate-witness.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (source target : S) (entry-positive : nnrat/positive (kernel source target))
  → proposition/existence ℕ (fun steps => nnrat/positive (iterate steps (fun state => mass state) target))
  where iterate := markov/nnrat-kernel-iterate S states kernel
  where mass := markov/nnrat-point-mass S decision source

markov/nnrat-point-mass-reflexive-iterate-witness.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (source : S)
  → proposition/existence ℕ (fun steps => nnrat/positive (iterate steps (fun state => mass state) source))
  where iterate := markov/nnrat-kernel-iterate S states kernel
  where mass := markov/nnrat-point-mass S decision source