Reference · Finite types, distributions and Markov chains

rainbow.math.finite.markov-point-mass

Finite types, distributions and Markov chains src/rainbow/math/finite/markov_point_mass.clj1 definitions, 7 theorems

Canonical point masses for finite exact-rational Markov kernels. A point mass is the unit diagonal spike induced by a certified Boolean equality decision. On an exhaustive duplicate-free carrier, pushing that mass through one kernel step is equivalent to the selected source row. This is the exact bridge from the mass-based iteration API to finite-step reachability. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.diagonal-spike

markov/nnrat-point-mass

DefinitionSource, line 82

markov/nnrat-point-mass.{u} :
  (S : Type u) (decision : S → S → data/Bool) (x₁ x₂ : S)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-point-mass-positive-at-selected

TheoremFor all inputsNo axiomsSource, line 102

markov/nnrat-point-mass-positive-at-selected.{u} :
  (S : Type u) (decision : S → S → data/Bool)
  (certified : finite/certified-equality-decision S decision) (selected : S)
  → nnrat/positive (markov/nnrat-point-mass S decision selected selected)

markov/nnrat-kernel-step-point-mass

TheoremFor all inputsNo axiomsSource, line 136

markov/nnrat-kernel-step-point-mass.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (selected target : S)
  → markov/nnrat-kernel-step S states kernel (fun state => mass state) target = kernel selected target
  where mass := markov/nnrat-point-mass S decision selected

= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-kernel-step-point-mass-positive

TheoremFor all inputsNo axiomsSource, line 212

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

Finset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-kernel-iterate-one-point-mass

TheoremFor all inputsNo axiomsSource, line 260

markov/nnrat-kernel-iterate-one-point-mass.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  (selected target : S)
  → markov/nnrat-kernel-iterate S states kernel 1 (fun state => mass state) target = kernel selected target
  where mass := markov/nnrat-point-mass S decision selected

= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-kernel-iterate-one-point-mass-positive

TheoremFor all inputsNo axiomsSource, line 291

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

Finset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-kernel-iterate-zero-point-mass-positive

TheoremFor all inputsNo axiomsSource, line 326

markov/nnrat-kernel-iterate-zero-point-mass-positive.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (selected : S)
  → nnrat/positive (markov/nnrat-kernel-iterate S states kernel 0 (fun state => mass state) selected)
  where mass := markov/nnrat-point-mass S decision selected

Finset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

markov/nnrat-point-mass-iterate-positive-along-trajectory

TheoremFor all inputsNo axiomsSource, line 358

markov/nnrat-point-mass-iterate-positive-along-trajectory.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (kernel : S → S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (trajectory : ℕ → S)
  (trajectory-member : ∀ (step : ℕ), list/membership S (finset-data/enumeration S states) (trajectory step))
  (edge-positive : ∀ (step : ℕ), nnrat/positive (kernel (trajectory step) (trajectory (data/succ step))))
  (steps : ℕ)
  → nnrat/positive (markov/nnrat-kernel-iterate S states kernel steps (fun state => mass state) (trajectory steps))
  where mass := markov/nnrat-point-mass S decision (trajectory 0)

Finset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational