The mean of a sum of m identically-distributed trials is m times the common mean, in two lines over the existing shelf

Identifier: F:rat-binomial-expectation
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let X be a family of rational-valued random variables on a finite index range [0, n) with weights p, let m be a natural number and q a rational. If every trial below m has expectation q, then the pointwise sum of the first m trials has expectation m*q, where m is read into the rationals as Rat.natDivSucc m 0. NO distribution hypothesis is needed: linearity of expectation does not care whether the weights sum to one. The proof is two steps over the shelf ADR-1616 and the rational development already built -- Rat.expectation_sumVars turns the left side into a sumRange of per-trial means, and one shared helper (Rat.sumRange_congr_lt against the constant function, then the sumRange-of-a-constant collapse) replaces each by q and sums m copies.

Formal statement

theorem Rat.binomial_expectation : forall (X : Nat -> Nat -> Rat) (p : Nat -> Rat) (n m : Nat) (q : Rat), (forall j, Nat.lt j m -> Eq (Rat.expectation (X j) p n) q) -> Eq (Rat.expectation (Rat.sumVars X m) p n) (Rat.mul (Rat.natDivSucc m 0) q)

Dependencies

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

9 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-axiom-free-rat

Kind: kernel-term
Status: checked

Supports: The declaration is admitted by the trusted kernel gate with an empty Kernel::axiom_footprint, together with every other declaration of ADR-1631's rational binomial layer. The test asserts Environment::contains FIRST, because an absent name has an empty footprint too.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::binomial_rat::binomial_rat_tests::binomial_rat_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.

loop-closes-and-computes

Kind: kernel-term
Status: checked

Supports: The per-trial hypothesis is discharged ENTIRELY by the generic AlgS.OrderedRing.bernoulli_expectation instantiated at AlgS.Rat.orderedRingS, and the resulting mean is then COMPUTED: three Bernoulli(1/3) trials have mean Rat.one. The test carries an off-by-one control at the statement level (the instance must not be the four-trial statement) and a value-level negative control (the mean is not 1/3).

Checker command

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

Evidence notes

Provenance

{
  "date": "2026-09-05",
  "established_by": "lane binomial-hoeffding (roadmap W3-12, ADR-1631)"
}