Reference · Finite types, distributions and Markov chains

rainbow.math.finite.index-hastings

Finite types, distributions and Markov chainssrc/rainbow/math/finite/index_hastings.clj0 definitions, 3 theorems

The canonical Hastings kernel instantiated on structural finite indices. This closes the obligation left open earlier, one step further than stated: they asked for index-equality soundness and then this assembly, and pushed the soundness themselves in a final commit, so what remained -- and what this module is -- is the assembly. Three declarations: - the certified equality decision for `Index n`, the conjunction of the soundness and completeness theorems the finite-index module already carries, at every bound; - the certified exhaustive carrier for `Index n` with its canonical finset: the decision certificate conjoined with enumeration coverage. The carrier-covered premise that was found by needing it holds here BY CONSTRUCTION -- `Index n` has no inhabitants outside its enumeration; - the capstone: for EVERY bound n, every normalized exact-rational target and proposal over `Index n`, the canonical Hastings kernel -- ratio acceptance, diagonal rejection, nothing supplied but the two normalization facts -- is stationary for the target. This is the first fully-instantiated MCMC stationarity statement in the corpus: no abstract carrier, no supplied placement, no equality hypothesis, no coverage hypothesis. Everything the caller once certified is now proved from the structure of `Index`. Still Level 3 and stated so: nothing here samples, and no executable claim is made. Native and axiom-free on D63.

Depends onmath.finite.markov-hastings-flowmath.finite.index

finite/index-certified-equality-decision :
  (upper : ℕ)
  → finite/certified-equality-decision (finite/Index upper) (finite/index-decide-equality upper)

finite/index-certified-exhaustive-carrier :
  (upper : ℕ)
  → finite/certified-exhaustive-carrier (finite/Index upper) (finite/index-finset upper) (finite/index-decide-equality upper)

mcmc/nnrat-hastings-index-canonical-kernel-stationary :
  (upper : ℕ) (target : finite/Index upper → ℚ≥0)
  (proposal : finite/Index upper → finite/Index upper → ℚ≥0)
  (target-normalized : probability/nnrat-total-mass (finite/Index upper) (finite/index-finset upper) target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized (finite/Index upper) (finite/index-finset upper) proposal)
  → markov/nnrat-stationary (finite/Index upper) (finite/index-finset upper) (kernel) target
  where kernel := mcmc/nnrat-hastings-canonical-kernel (finite/Index upper) (finite/index-finset upper) target proposal (finite/index-decide-equality upper)