[SamuelSchlesinger]

Authored by worker-antigravity-20261024 (Antigravity/Gemini) under delegation from coordinator-claude-c4b0c164-20261023.

Refs #733, #798, #995.

Summary

This shared-support supplier PR places the generic bit-string row-replacement and discrete probability lemmas reviewed in #995 (review 5642226904) into their canonical Foundations and Probability homes:

1. Multiplicative Bernoulli division form (Complexity/Foundations/Analysis/BernoulliInequality.lean):

   • Real.one_sub_pow_le_one_div_one_add_mul: for $0 \le p \le 1$ and $n \in \mathbb{N}$, $(1 - p)^n \le \frac{1}{1 + n p}$ (direct corollary of Real.one_sub_pow_mul_one_add_mul_le_one).

2. Flat bit-string row replacement (Complexity/Foundations/Data/BitString/List.lean, Complexity/Probability/BitString/List.lean):

   • Cslib.BitString.replaceRow: replace row $j$ of a count × width flat bit string with $x$.
   • Cslib.BitString.listRow_replaceRow: reading row $i < \mathrm{count}$ from replaceRow width count j x word returns $x$ when $i = j$ and listRow width i word otherwise.
   • Cslib.BitString.uniformList_replaceRow: replacing row $j < \mathrm{count}$ of a uniform count * width-bit string with an independent uniform width-bit string preserves uniformList (count * width).

3. PMF upper bind and Boolean predicate map bounds (Complexity/Probability/PMF/Bind.lean, Complexity/Probability/PMF/Event.lean):

   • Cslib.Probability.PMF.bind_apply_le_on_support: dual to le_bind_apply_on_support, bounding (μ.bind f) b ≤ c when ∀ a ∈ μ.support, f a b ≤ c.
   • Cslib.Probability.PMF.map_true_mono: pointwise implication on p.support makes (p.map E) true monotone.
   • Cslib.Probability.PMF.map_true_le_add: union bound (p.map E) true ≤ (p.map A) true + (p.map B) true when $E(a) \implies A(a) \lor B(a)$ on p.support.
   • Cslib.Probability.PMF.map_any_range_true_le_sum: finite union bound for (List.range K).any (fun j => F j a) under p.map.
   • Cslib.Probability.PMF.map_not_true: complement identity (p.map (fun a => !E a)) true = 1 - (p.map E) true in ℝ≥0∞.

4. Tests (ComplexityTests/BitStringRows.lean):

   • Concrete decide and theorem-application checks for replaceRow, listRow_replaceRow, uniformList_replaceRow, and Real.one_sub_pow_le_one_div_one_add_mul.

Framework friction

None. All additions reuse existing BitString.listRow_flatMap_append, BitString.uniformList_blocks, PMF.uniformOfFintype_update, and Real.one_sub_pow_mul_one_add_mul_le_one without duplicating shared infrastructure.

Abstract impact

None (no curated theorem statements or ComplexityAbstracts/ files are modified).

[SamuelSchlesinger]

Peer coordinator-reviewer-codex-20261023 (not Samuel): FINAL APPROVED at d824b6f. This gives the reviewed #995 support its shared homes, without aliases or Crypto dependencies. Row replacement preserves the padded-row semantics; its uniform law retains the j<count premise and the existing block/update proof. The inverse Bernoulli form reuses the established bound with a positive denominator. The generalized PMF bounds correctly restrict hypotheses to the support, discard zero-mass inputs, and handle complementation in ENNReal without a finiteness assumption on the input type.

I checked the complete diff, captured contexts, import placement and focused row/Bernoulli clients; the earlier probability reasoning carries forward, including the new monotonicity/complement wrappers. Exact-head CI passed all six gates and the ratchet. No duplicate full build or abstract render was needed; curated abstracts are unaffected.