Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-hastings-diagonal

Finite types, distributions and Markov chainssrc/rainbow/math/finite/markov_hastings_diagonal.clj1 definitions, 4 theorems

The canonical diagonal rejection placement, from a Boolean equality decider. The completed-Hastings-kernel theorems take the rejection placement as a PARAMETER with certificates, and the off-diagonal-zero corollary discharges the symmetry certificate -- but still asks the caller for a placement and for PROPOSITIONAL decidability of state equality. That decidability is a Church-encoded disjunction, so it eliminates only into Prop: no placement FUNCTION can be built from it. This module supplies the missing constructive half. Given a Boolean decider with soundness and completeness -- decide l r = true exactly when Eq l r -- the canonical placement puts the whole rejection mass on the diagonal: diagonal-placement decide mass x y = if (decide x y) then mass x else 0 and three theorems make it plug directly into the existing corollaries: the placement is provably zero off the diagonal, carries exactly `mass x` on it, and the Boolean decider yields the PROPOSITIONAL decidability the symmetry corollary asks for. The capstone then restates completed-kernel stationarity with the placement CONSTRUCTED rather than supplied: the caller provides the decider, its two laws, and the mass certificate for the diagonal function -- no separate placement, no symmetry certificate, no hand-written off-diagonal proof. For indexed state spaces this closes the practical gap entirely: nat/decide-equality with its existing true-sound and equality-implies-decide-equality-true theorems is precisely such a decider, and the test instantiates exactly that. Scope boundary, stated because the neighbouring cone is live: the exact ROW-TOTAL theorem -- that the diagonal placement's row over an enumeration sums to the single diagonal entry -- is NOT here. It needs sum-over- enumeration machinery against finset no-duplicates evidence, which is the diagonal-spike route that was explored separately. The mass certificate stays a hypothesis in the capstone for that reason. Native and axiom-free on D63.

Depends onmath.finite.markov-hastings-flow

mcmc/diagonal-placement.{u} :
  (S : Type u) (decide : S → S → data/Bool) (mass : S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

mcmc/diagonal-placement-diagonal-mass.{u} :
  (S : Type u) (decide : S → S → data/Bool) (mass : S → ℚ≥0)
  (complete : ∀ (complete-left : S), ∀ (complete-right : S), complete-left = complete-right → decide complete-left complete-right = data/true)
  (state : S)
  → mcmc/diagonal-placement S decide mass state state = mass state

mcmc/diagonal-placement-off-diagonal-zero.{u} :
  (S : Type u) (decide : S → S → data/Bool) (mass : S → ℚ≥0)
  (sound : ∀ (sound-left : S), ∀ (sound-right : S), decide sound-left sound-right = data/true → sound-left = sound-right)
  → mcmc/nnrat-off-diagonal-zero S (mcmc/diagonal-placement S decide mass)

mcmc/state-equality-decidable-of-boolean.{u} :
  (S : Type u) (decide : S → S → data/Bool)
  (sound : ∀ (sound-left : S), ∀ (sound-right : S), decide sound-left sound-right = data/true → sound-left = sound-right)
  (complete : ∀ (complete-left : S), ∀ (complete-right : S), complete-left = complete-right → decide complete-left complete-right = data/true)
  (left right : S)
  → proposition/disjunction (left = right) (left = right → proposition/falsity)

mcmc/nnrat-hastings-completed-kernel-stationary-of-diagonal-placement.{u} :
  (S : Type u) (states : Finset S) (target : S → ℚ≥0) (proposal : S → S → ℚ≥0)
  (decide : S → S → data/Bool)
  (sound : ∀ (sound-left : S), ∀ (sound-right : S), decide sound-left sound-right = data/true → sound-left = sound-right)
  (complete : ∀ (complete-left : S), ∀ (complete-right : S), complete-left = complete-right → decide complete-left complete-right = data/true)
  (mass : S → ℚ≥0)
  (target-normalized : probability/nnrat-total-mass S states target = 1)
  (proposal-normalized : markov/nnrat-kernel-rows-normalized S states proposal)
  (placement-has-rejection-mass : ∀ (source : S), probability/nnrat-total-mass S states (mcmc/diagonal-placement S decide mass source) = mcmc/nnrat-hastings-rejection-mass S states target proposal source)
  → markov/nnrat-stationary S states (kernel) target
  where kernel := mcmc/nnrat-hastings-completed-kernel S states target proposal (mcmc/diagonal-placement S decide mass)