The Bernoulli parameter is its mean, over an arbitrary setoid ordered ring and with no hypothesis on the parameter

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

Recorded description

Let R be an AlgS.OrderedRing and q an element of R. The expectation of the two-outcome indicator bernoulliVar R (0 |-> 0, succ _ |-> 1) against the weights bernoulliMass R q (0 |-> 1 - q, succ _ |-> q) over the index range [0, 2) is equivalent to q. No hypothesis on q is needed: the identity is algebraic, and only the companion IsDistribution statement cares whether the weights are a distribution. The expectation reduces by iota to (0 + 0*(1-q)) + 1*q, which zero_mul, the left multiplicative unit law and the left additive unit law collapse to q.

Formal statement

theorem AlgS.OrderedRing.bernoulli_expectation : forall (R : AlgS.OrderedRing) (q : R.carrier), R.equiv (AlgS.OrderedRing.expectation R (AlgS.OrderedRing.bernoulliVar R) (AlgS.OrderedRing.bernoulliMass R q) 2) q

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

kernel-axiom-free-s

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.

value-mean-computes

Kind: kernel-term
Status: checked

Supports: At AlgS.Rat.orderedRingS the expectation term is REDUCED by the kernel and compared against the parameter -- 1/2 for the fair coin and 1/3 for the biased one -- with a negative control requiring that the 1/3 mean is not 1/2. The two definitions are separately evaluated at concrete small arguments, which is the only check that can catch a Definition computing the wrong value, since the trusted gate type-checks whatever it computes.

Checker command

cargo test --release -p axeyum-lean-kernel --lib rat_prelude::binomial_s::binomial_s_tests::bernoulli_expectation_computes_to_the_parameter -- --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)"
}