Part (c): randomly scored sets, fair coin on ties

Blind read-back by an independent auditor agent (Opus 5) given only the Lean code and the platform auditor instructions; docstrings and comments ignored; identifier names treated as opaque; no access to the informal statement, the source proof, or the captain's intent.

A single theorem, proof sorry. Explicit arguments: four real numbers a, b, c, q, a list ms of naturals, and a natural n. Hypotheses, in order:

1. 0 ≤ a (non-strict);
2. 0 ≤ b (non-strict);
3. 0 ≤ c (non-strict);
4. a + b + c = 1;
5. c < a (strict; together with 1 and 3 this forces a > 0 and 0 ≤ c < a ≤ 1);
6. 1/2 < q (strict);
7. q < 1 (strict);
8. every member m of the list ms is odd and satisfies 1 < m;
9. ms ≠ [];
10. 1 < n (no oddness requirement on n).

Conclusion:

W( ν[a,b,c; Nest(ms, q)] , n )   <   W( ν[a,b,c; q] , n · ∏ms )

Fully unfolded: for a real parameter r, let ν_r : ℤ → ℝ be the three-point weight function

ν_r(+1) = r·a + (1 − r)·c,    ν_r(−1) = r·c + (1 − r)·a,    ν_r(0) = b,
ν_r(z)  = 0 for every integer z outside {−1, 0, +1};

note ν_r(+1) + ν_r(−1) + ν_r(0) = a + b + c, which the hypotheses fix at 1. Let L^{ν_r}_N be defined by L^{ν_r}_0 = the indicator of 0 and

L^{ν_r}_{N+1}(z) = ν_r(−1)·L^{ν_r}_N(z+1) + ν_r(0)·L^{ν_r}_N(z) + ν_r(+1)·L^{ν_r}_N(z−1),

and let W(ν_r, N) = Σ_{z = 1}^{N} L^{ν_r}_N(z) + L^{ν_r}_N(0)/2, the sum running over integers z from 1 to N inclusive plus half the value at 0. The theorem asserts

[ Σ_{z=1}^{n} L^{ν_R}_n(z) + L^{ν_R}_n(0)/2 ]
      <  [ Σ_{z=1}^{n·∏ms} L^{ν_q}_{n·∏ms}(z) + L^{ν_q}_{n·∏ms}(0)/2 ]

where R = Nest(ms, q) = B_{m₁}(B_{m₂}(⋯B_{m_k}(q)⋯)) with the head of ms outermost and B_M(x) = Σ_{i ≤ M, 2i > M} C(M, i) x^i (1 − x)^(M − i), and ∏ms is the product of the list entries. Key structural points: the two sides use the same a, b, c; they differ in the parameter fed to ν (the nested value R on the left, the bare q on the right) and in the number of convolution steps (n on the left, n·∏ms on the right, the latter being at least 3n). The summation range on each side is tied to that side's own step count. The inequality is strict, with the nested/fewer-steps expression on the left. Degenerate values are reachable under the hypotheses: b may be 0, and c may be 0. No hypothesis asserts that R lies in [0, 1] or that ν_R has nonnegative values; these would have to be derived. The hypotheses are satisfiable (a = 0.5, b = 0.3, c = 0.2, q = 0.6, ms = [3], n = 2), so the statement is not vacuous. This theorem matches conjunct 3 of file 2.