Reference · Non-negative rationals

rainbow.math.rational.nnrat.map-sum-positive

Non-negative rationalssrc/rainbow/math/rational/nnrat/map_sum_positive.clj0 definitions, 1 theorems

Strict positivity of finite exact nonnegative-rational sums. If a listed element maps to a positive rational, the full finite map-sum is positive. The proof is constructive List.rec induction over membership and needs neither decidable equality nor duplicate freedom. This is the generic path-term-to-positive-transition bridge for finite Markov composition. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.positive

nnrat/map-sum-positive-of-member.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (items : List A) (selected : A)
  (member : list/membership A items selected)
  (selected-positive : nnrat/positive (mapping selected))
  → nnrat/positive (nnrat/map-sum A mapping items)