The Bernoulli variance is q(1-q) in a ring with NO commutativity, because the identity needs commutativity exactly once and it is derivable

Identifier: F:algs-orderedring-bernoulli-variance
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 variance of the two-outcome indicator bernoulliVar R against the weights bernoulliMass R q over [0, 2) -- the CENTRED form E[(X - E X)^2] -- is equivalent to q*(1 - q). AlgS.OrderedRing carries no mulComm (ADR-1592 built it Ring-based on purpose), and the identity looks like it needs one. It does not: the subring generated by a single element is commutative, and the ONE instance the identity uses is (1-q)*q ~ q*(1-q), which is proved by expanding both sides to q + -(q*q) with the two distributive laws, the two multiplicative unit laws and the two negation-through-multiplication lemmas. With that supplied the computation is four steps: (q*q)*u + (u*u)*q ~ q*(q*u) + u*(q*u) ~ (q + u)*(q*u) ~ 1*(q*u) ~ q*u, where u := 1 - q and q + u ~ 1. No trichotomy, no field inverse, no commutative ring.

Formal statement

theorem AlgS.OrderedRing.bernoulli_variance : forall (R : AlgS.OrderedRing) (q : R.carrier), R.equiv (AlgS.OrderedRing.variance R (AlgS.OrderedRing.bernoulliVar R) (AlgS.OrderedRing.bernoulliMass R q) 2) (R.mul q (R.add R.one (R.neg q)))

Dependencies

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

4 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.

value-variance-computes-and-a-half-is-not-enough

Kind: kernel-term
Status: checked

Supports: At AlgS.Rat.orderedRingS the variance term is REDUCED by the kernel: 1/4 at q = 1/2 and 2/9 at q = 1/3. The q = 1/3 instance is load-bearing rather than decorative, and the suite says so in its own assertions: the true answer q(1-q) and the plausible wrong answer q*q are BOTH 1/4 at q = 1/2, so a suite instantiated only there could not distinguish them. The negative control requires that the q = 1/3 variance is not 1/9, and carries a positive control (1/9 is definitionally itself) so a def_eq that had stopped deciding would be visible.

Checker command

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