Markov's inequality holds in every setoid ordered ring, with no strict order and no positivity hypothesis

Identifier: F:algs-orderedring-markov-inequality
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let R be an AlgS.OrderedRing -- a setoid ordered ring: a ring whose equality is a carried equivalence relation with congruence fields, together with a reflexive transitive antisymmetric-up-to-equivalence order that is translation-invariant and closed under products of nonnegatives. Let p be a finite distribution on the index range [0, n) (nonnegative, summing to one), let X and ind be R-valued functions on that range, and let a be an element of R. If a*ind(k) <= X(k) for every k < n, then a*E[ind] <= E[X], where E[Y] = sum over k < n of Y(k)*p(k). This is Markov's inequality with the division cleared, and it is stated with TWO FEWER hypotheses than the rational-carrier version Rat.markov_inequality: that version additionally assumes 0 < a and X >= 0 pointwise, and its proof uses neither. The generic statement is therefore strictly stronger, and Rat.markov_inequality is an instance of it obtained by discarding those two arguments. Dropping them was forced rather than chosen: AlgS.OrderedRing carries no strict order at all.

Formal statement

theorem AlgS.OrderedRing.markov_inequality : forall (R : AlgS.OrderedRing) (a : R.carrier) (X ind p : Nat -> R.carrier) (n : Nat), AlgS.OrderedRing.IsDistribution R p n -> (forall k, Nat.lt k n -> R.le (R.mul a (ind k)) (X k)) -> R.le (R.mul a (AlgS.OrderedRing.expectation R ind p n)) (AlgS.OrderedRing.expectation R X p n)

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 1 direct dependents

Evidence

kernel-algs-markov

Kind: kernel-term
Status: checked

Supports: AlgS.OrderedRing.markov_inequality is admitted by the trusted kernel gate with an empty axiom footprint, together with every other declaration of the generic finite-probability layer. The test reads the footprint from Kernel::axiom_footprint and asserts the size of its own name list, so a declaration silently dropped from the layer fails it.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::probability_s::probability_s_tests::probability_s_declarations_are_axiom_free -- --exact 2>&1 | grep -c '^test result: ok. 1 passed'

Evidence notes

grep -c, not grep -q: -q would SIGPIPE the producer under pipefail, and -c exits 1 printing 0 when the line is absent, so a suite that compiled to zero tests and exited 0 is caught rather than counted as a pass. --release is mandatory: the rational prelude SIGABRTs on the default debug thread stack.

instance-rat-markov

Kind: instance-pin
Status: checked

Supports: Rat.markov_inequality is an INSTANCE of this theorem: the test walks the rational theorem's own Pi telescope, feeds the generic theorem only the arguments it takes (skipping the two unused hypotheses), closes the term back over the full telescope, infers its type, and requires definitional equality with Rat.markov_inequality's declared type. A generic statement that had quietly weakened, or that did not in fact subsume the rational one, fails here.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::probability_s::probability_s_tests::rat_markov_is_an_instance_after_dropping_two_unused_hypotheses -- --exact 2>&1 | grep -c '^test result: ok. 1 passed'

Provenance

{
  "date": "2026-09-04",
  "established_by": "lane finite-probability-generic (roadmap W1-10, ADR-1616)"
}