The Bernoulli weights are a distribution, discharged from a construction rather than assumed, in every setoid ordered ring

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

Recorded description

Let R be an AlgS.OrderedRing -- a setoid ordered ring -- and let q be an element of R with 0 <= q <= 1. Define the two-outcome mass function bernoulliMass R q by 0 |-> 1 - q and succ _ |-> q. Then it is a finite distribution on the index range [0, 2): it is nonnegative on that range and it sums to one. This is the first IsDistribution in the repository that is PROVED of a constructed weight function rather than assumed of an arbitrary one. Every statement of the finite-probability layer (ADR-1616) and of the rational development takes an arbitrary p, so before this no p existed to discharge the hypothesis with. The nonnegativity half is proved for EVERY index, not only for indices below 2, which is what lets the bounded form be discharged without inverting a Nat.lt; the sum half reduces by iota to (0 + (1 + -q)) + q and is then four record laws.

Formal statement

theorem AlgS.OrderedRing.bernoulli_isDistribution : forall (R : AlgS.OrderedRing) (q : R.carrier), R.le R.zero q -> R.le q R.one -> AlgS.OrderedRing.IsDistribution R (AlgS.OrderedRing.bernoulliMass R q) 2

Dependencies

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

3 direct dependencies 1 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.

instance-rat-is-distribution

Kind: kernel-term
Status: checked

Supports: At AlgS.Rat.orderedRingS with q = 1/3 the two order hypotheses are decided by Rat.ble through Rat.le_of_ble_eq_true, so the rational instance assumes nothing at all; the test infers the instance's type and requires definitional equality with the hand-built IsDistribution statement.

Checker command

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