Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-full-support

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_full_support.clj4 definitions, 5 theorems

An executable full-support decision, and what its verdict is worth. The positivity cone gives pointwise theorems: positive target here, positive proposal there, positive canonical-kernel entry. A CALLER holds a whole model, and the honest interface is a single boolean they can compute: full-support-decision folds an executable positivity check over the finite enumeration -- every target mass, every proposal edge in both directions -- and this module's theorems make a true verdict discharge EVERY pointwise positivity hypothesis at once, for every state the carrier covers. On structural Index n, where coverage is by construction, the two capstones follow with no hypothesis beyond the verdict: every canonical-kernel entry is positive, and from every state, one step of the actual mass iterator started at the certified point mass puts positive mass on every state. That second statement is one-step reachability -- the exists-n irreducibility definition's n = 1 witness, stated without yet defining irreducibility, per the agreed split: the path-induction engine below this API is an earlier cone; this module adds the decision layer and its wiring. The decision is deliberately naive -- a fold of numerator-positivity over enumerations, quadratic in states -- because its job is to be READ and to be sound, not to be fast. Native and axiom-free on D63.

Depends onmath.logic.boolean-andmath.finite.index-hastingsmath.finite.markov-point-massmath.finite.markov-hastings-positive

mcmc/decide-positive :
  (x₁ : ℚ≥0)
  → data/Bool

mcmc/all-positive.{u} :
  (S : Type u) (weights : S → ℚ≥0) (items : List S)
  → data/Bool

mcmc/all-pairs-positive.{u} :
  (S : Type u) (kernel : S → S → ℚ≥0) (sources targets : List S)
  → data/Bool

mcmc/full-support-decision.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  → data/Bool

mcmc/decide-positive-true-sound :
  (value : ℚ≥0)
  (h₁ : mcmc/decide-positive value = data/true)
  → nnrat/positive value

mcmc/all-positive-member-sound.{u} :
  (S : Type u) (weights : S → ℚ≥0) (items : List S)
  (h₁ : mcmc/all-positive S weights items = data/true)
  (value : S) (member : list/membership S items value)
  → nnrat/positive (weights value)

mcmc/all-pairs-positive-member-sound.{u} :
  (S : Type u) (kernel : S → S → ℚ≥0) (sources targets : List S)
  (h₁ : mcmc/all-pairs-positive S kernel sources targets = data/true)
  (source destination : S) (source-member : list/membership S sources source)
  (destination-member : list/membership S targets destination)
  → nnrat/positive (kernel source destination)

mcmc/nnrat-hastings-index-canonical-kernel-positive-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  (left right : finite/Index upper)
  → nnrat/positive (mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper) left right)

mcmc/nnrat-hastings-index-one-step-reachable-of-full-support :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (verdict : mcmc/full-support-decision (finite/Index upper) (finite/index-finset upper) target proposal = data/true)
  (selected destination : finite/Index upper)
  → nnrat/positive (markov/nnrat-kernel-iterate (finite/Index upper) (finite/index-finset upper) (kernel) 1 (fun state => mass state) destination)
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)
  where mass := markov/nnrat-point-mass (finite/Index upper) (finite/index-decide-equality upper) selected