The Bernoulli weights are nonnegative at EVERY index, not only inside the two-outcome range

Identifier: F:algs-orderedring-bernoulli-mass-nonneg
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let R be an AlgS.OrderedRing and q an element of R with 0 <= q <= 1. Then 0 <= bernoulliMass R q k for every natural k, including k >= 2 where the mass function returns q by its own recursion. Stating it unbounded rather than for k < 2 is what lets AlgS.OrderedRing.bernoulli_isDistribution discharge its bounded half with `fun i _ => ...` and never invert a Nat.lt; the bounded form would have cost a two-case-plus-absurd analysis for nothing. The proof is Nat.rec on k: the base case is AlgS.OrderedRing.sub_nonneg_of_le applied to q <= 1, whose conclusion 0 <= 1 + -q is literally the iota-reduct of the mass at 0, and every successor case is the 0 <= q hypothesis unchanged.

Formal statement

theorem AlgS.OrderedRing.bernoulliMass_nonneg : forall (R : AlgS.OrderedRing) (q : R.carrier), R.le R.zero q -> R.le q R.one -> forall (k : Nat), R.le R.zero (AlgS.OrderedRing.bernoulliMass R q k)

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-axiom-free

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 generic Bernoulli layer. The test asserts Environment::contains FIRST, because an absent name has an empty footprint too, and it pins its own name-list length, so a declaration silently dropped from the layer fails it.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::binomial_s::binomial_s_tests::binomial_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.

Provenance

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