Don't Label Twice: Game, Set, Match

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.

This file states a single theorem whose statement is a conjunction of four universally quantified implications, joined by "and" (all four must hold). The four conjuncts are read back separately below, followed by an explicit comparison of their hypotheses. The proof is sorry.

Conjunct 1

For every real number q and all natural numbers m and n, if

• 1/2 < q (strict),
• q < 1 (strict),
• m is odd,
• 1 < m (strict, so m ≥ 3 given oddness),
• n is odd,
• 1 < n (strict, so n ≥ 3 given oddness),

then

B_n( B_m(q) ) < B_{n·m}(q)

i.e. the strict-majority binomial tail of n trials whose success parameter is itself the strict-majority tail of m trials at parameter q is strictly less than the strict-majority tail of n·m trials at parameter q. Spelled out with the definition unfolded, the claim is

Σ_{j ≤ n, 2j > n} C(n, j) · X^j · (1 − X)^(n − j)
      <  Σ_{k ≤ nm, 2k > nm} C(nm, k) · q^k · (1 − q)^(nm − k)

where X = Σ_{i ≤ m, 2i > m} C(m, i) · q^i · (1 − q)^(m − i). The hypotheses are satisfiable (e.g. q = 0.6, m = n = 3), so the conjunct is not vacuous.

Conjunct 2

For every real q, every list ms of natural numbers, and every natural n, if

• 1/2 < q,
• q < 1,
• every entry m of the list ms satisfies both "m is odd" and 1 < m,
• ms is not the empty list,
• 1 < n (so n ≥ 2; n is not required to be odd here),

then

F_n( Nest(ms, q) )  <  F_{n · ∏ms}(q)

where F_N(x) = B_N(x) + T_N(x)/2 adds half of the "exact tie" term to the strict-majority tail, Nest(ms, q) is the iterated composition B_{m₁}(B_{m₂}(…B_{m_k}(q)…)) with the head of ms outermost, and ∏ms = m₁·m₂·⋯·m_k. Because ms is nonempty and each entry is odd and at least 3, ∏ms is odd and at least 3, so T_{∏ms} would be 0 — but note the tie term on the right is T_{n·∏ms}, and n·∏ms is even whenever n is even, in which case that term is nonzero. On the left the tie term is T_n, nonzero exactly when n is even. The inequality is strict and points left-to-right (nested value strictly smaller). Hypotheses are satisfiable (e.g. q = 0.6, ms = [3], n = 2).

Conjunct 3

For all real numbers a, b, c, q, every list ms of natural numbers, and every natural n, if

• 0 ≤ a,
• 0 ≤ b,
• 0 ≤ c,
• a + b + c = 1,
• c < a (strict),
• 1/2 < q,
• q < 1,
• every entry m of ms is odd and satisfies 1 < m,
• ms ≠ [],
• 1 < n (n not required odd),

then

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

Unfolded: on the left, put r = Nest(ms, q) and form the three-point weight function on ℤ that assigns r·a + (1−r)·c to +1, r·c + (1−r)·a to −1, b to 0, and 0 elsewhere; convolve it with itself n times starting from the point mass at 0 (that is, form L^ν_n by the recursion of definition (i)); then take the sum of L^ν_n(z) over integers 1 ≤ z ≤ n plus one half of L^ν_n(0). On the right, do exactly the same with r replaced by the bare q and with n replaced by n · ∏ms (so the outer sum runs over 1 ≤ z ≤ n·∏ms and the tie term is L^ν_{n·∏ms}(0)/2). The claim is that the left quantity is strictly less than the right one. Note that the number of convolution steps differs between the two sides (n versus n·∏ms), as does the parameter fed into ν (Nest(ms, q) versus q), while a, b, c are the same on both sides. Note also that no hypothesis directly constrains Nest(ms, q) to lie in [0, 1]; only 1/2 < q < 1 and the list conditions are assumed. The hypotheses 0 ≤ a, 0 ≤ c, c < a and a + b + c = 1 force 0 ≤ c < a ≤ 1 and 0 ≤ b < 1; they are satisfiable (e.g. a = 0.5, b = 0.3, c = 0.2), so the conjunct is not vacuous.

Conjunct 4

Same shape as conjunct 3 with two changes. For all reals a, b, c, q, every list ms of naturals, and every natural n, if

• 0 ≤ a,
• 1/2 ≤ b (non-strict),
• 0 ≤ c,
• a + b + c = 1,
• c < a,
• 1/2 < q,
• q < 1,
• every entry of ms is odd and greater than 1,
• ms ≠ [],
• 1 < n,

then

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

i.e. the same construction as conjunct 3 but with the tie term dropped on both sides: the left side is Σ_{z=1}^{n} L^ν_n(z) for ν = ν[a,b,c; Nest(ms,q)] and the right side is Σ_{z=1}^{n·∏ms} L^ν_{n·∏ms}(z) for ν = ν[a,b,c; q]. Strict inequality, left less than right. The hypotheses 1/2 ≤ b, 0 ≤ a, 0 ≤ c, a + b + c = 1 force a + c ≤ 1/2, hence 0 ≤ c < a ≤ 1/2; they are satisfiable (e.g. a = 0.3, b = 0.6, c = 0.1), so this conjunct is not vacuous either.

How the four conjuncts' hypotheses differ

• Conjunct 1 vs conjunct 2. Conjunct 1 quantifies over a single natural m and requires m odd, m > 1, and additionally n odd, n > 1. Conjunct 2 replaces the single m by a list ms, requires each entry odd and greater than 1 plus ms ≠ [], and drops the oddness requirement on n, keeping only n > 1. Correspondingly the conclusion of conjunct 1 uses B (strict majority only) on both sides, whereas conjunct 2 uses F = B + T/2 (strict majority plus half the exact-tie term) on both sides. Conjunct 1's conclusion compares B_n(B_m(q)) with B_{n·m}(q); conjunct 2's compares F_n(Nest(ms,q)) with F_{n·∏ms}(q).
• Conjunct 2 vs conjunct 3. Conjunct 3 keeps every hypothesis of conjunct 2 verbatim (1/2 < q, q < 1, all entries of ms odd and > 1, ms ≠ [], 1 < n) and adds three new real parameters a, b, c together with five new hypotheses: 0 ≤ a, 0 ≤ b, 0 ≤ c, a + b + c = 1, and c < a. The conclusion changes from the binomial quantities F to the convolution quantities W built from ν[a,b,c; ·].
• Conjunct 3 vs conjunct 4. The variable lists and every other hypothesis are identical. The only hypothesis difference is that conjunct 3's 0 ≤ b is replaced in conjunct 4 by the strictly stronger 1/2 ≤ b. The conclusion differs by dropping the half-tie term: conjunct 3 compares W = S + Tie/2, conjunct 4 compares S alone. So conjunct 4 has a stronger hypothesis and a different (not weaker or stronger by inspection) conclusion; neither conjunct implies the other by inspection.
• Across all four. 1/2 < q and q < 1 appear in all four. 1 < n appears in all four. Oddness of n appears only in conjunct 1. The list hypotheses (ms ≠ [] and entrywise odd, > 1) appear in conjuncts 2, 3, 4. The parameters a, b, c and their constraints appear only in conjuncts 3 and 4. In every conjunct the final inequality is strict and oriented with the "nested / smaller index" expression on the left (the smaller side).

---