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.

Read-back — Definitions/Def_GameSetMatch.lean

Auditor model: Claude Opus 5 (model id claude-opus-5[1m]), 1M-context configuration.

Scope of this document. This is a blind read-back of the eight definitions in the file. Docstrings and comments were ignored; only the executable code was read. Identifier names are treated as opaque labels — nothing below is inferred from what a name suggests. All math is written in plain text / Unicode.

File-level facts. The file imports all of Mathlib and places every declaration in the namespace GameSetMatch. All eight declarations are marked noncomputable (they live over the real numbers, which have no executable representation), so none of them can be evaluated by the kernel's evaluator; they are mathematical functions only. There are no theorems, no axioms, no typeclass parameters, no hypotheses of any kind attached to any definition — every definition is a total function of its stated arguments, so all arguments range over the full type with no positivity, normalization, or range constraints.

Throughout, I write:

• ℤ for the integers, ℕ for the naturals (including 0), ℝ for the reals;
• L(μ, N, ·) for matchScoreLaw μ N;
• B(m, q) for bestOfWinProb m q.

---

1. matchScoreLaw

noncomputable def matchScoreLaw (μ : ℤ → ℝ) : ℕ → ℤ → ℝ
  | 0,     z => if z = 0 then 1 else 0
  | N + 1, z => ∑ j ∈ Finset.Icc (-1 : ℤ) 1, μ j * matchScoreLaw μ N (z - j)

Type. Takes one explicit argument μ, an arbitrary function ℤ → ℝ (no assumption that it is nonnegative, that it is supported on a finite set, or that it sums to 1). Returns a function ℕ → ℤ → ℝ; i.e. for each natural number N and each integer z it returns a real number L(μ, N, z).

Computation. Defined by structural recursion on the natural-number argument N, with the integer argument z passed along:

• Base case N = 0: L(μ, 0, z) = 1 if z = 0, and 0 otherwise. This is the Kronecker delta / point mass at 0. (The test z = 0 is decidable equality on ℤ; there is no ambiguity.)

• Step case: for every N ≥ 0 and every z,

  L(μ, N+1, z) = Σ over j in Finset.Icc(-1, 1) of  μ(j) · L(μ, N, z − j)
  

  The index set Finset.Icc (-1 : ℤ) 1 is the closed integer interval from −1 to 1, i.e. exactly the three-element set {−1, 0, 1}. So the step unfolds to

  L(μ, N+1, z) = μ(−1)·L(μ, N, z+1) + μ(0)·L(μ, N, z) + μ(1)·L(μ, N, z−1)
  

  Note the subtraction z − j is integer subtraction (ℤ is a group), so there is no truncation anywhere; z ranges over all of ℤ, negative values included.

What it is, unrolled. L(μ, N, ·) is the N-fold discrete convolution power of the three-point weight vector (μ(−1), μ(0), μ(1)) against the point mass at 0. Equivalently, in closed form,

L(μ, N, z) = Σ over (j₁,…,j_N) ∈ {−1,0,1}^N with j₁+…+j_N = z  of  μ(j₁)·…·μ(j_N)

or with multinomial coefficients, summing over p, m ≥ 0 with p + m ≤ N and p − m = z:

L(μ, N, z) = Σ  N! / (p! · m! · (N−p−m)!) · μ(1)^p · μ(−1)^m · μ(0)^(N−p−m)

Edge cases and degeneracies.

• Only three values of μ are ever consulted: μ(−1), μ(0), μ(1). The behaviour of μ at every other integer is completely ignored — two functions agreeing on {−1, 0, 1} give identical results.
• Nothing forces μ to be a probability weight. The three consulted values may be negative, larger than 1, or fail to sum to 1. Consequently L(μ, N, z) may be negative or exceed 1, and the total mass is Σ over z of L(μ, N, z) = (μ(−1) + μ(0) + μ(1))^N, which is 1 only when μ(−1) + μ(0) + μ(1) = 1.
• If μ is identically 0 on {−1, 0, 1}, then L(μ, 0, ·) is still the point mass at 0 (the base case does not consult μ at all), while L(μ, N, ·) ≡ 0 for every N ≥ 1.
• Support: by induction, L(μ, N, z) = 0 whenever |z| > N. This is a consequence of the recursion, not a stipulation.
• Direction of the recursion: the recursion peels off the successor of N, so the summation variable j at level N+1 is the "newest" increment and L(μ, N, z − j) is the accumulated value over the first N levels. Because the same μ is used at every level, the resulting function is symmetric in the order of increments, so this choice is not observable in the value.

Dependencies. None (only Mathlib's Finset.Icc and ℤ/ℝ arithmetic). It is the base of the first cluster of definitions.

---

2. strictWinProb

noncomputable def strictWinProb (μ : ℤ → ℝ) (N : ℕ) : ℝ :=
  ∑ z ∈ Finset.Icc (1 : ℤ) (N : ℤ), matchScoreLaw μ N z

Type. Takes μ : ℤ → ℝ and N : ℕ; returns a real number.

Computation. The finite sum of L(μ, N, z) as z ranges over the closed integer interval [1, N], where N is coerced from ℕ into ℤ:

strictWinProb(μ, N) = L(μ, N, 1) + L(μ, N, 2) + … + L(μ, N, N)

Edge cases.

• N = 0: the index set is Finset.Icc (1 : ℤ) (0 : ℤ), which is empty (since 1 > 0), so the sum is 0. Thus strictWinProb(μ, 0) = 0 by the empty-sum convention, with no case split written in the code.
• N = 1: the sum has a single term, L(μ, 1, 1) = μ(1).
• The upper limit is exactly N, not +∞. Since L(μ, N, z) = 0 for z > N, this finite window happens to capture the entire mass at strictly positive integers; but as written the definition is a finite sum over {1, …, N} and says nothing about z > N.
• The lower limit is 1, so z = 0 is excluded: this is the mass strictly above 0, not at-or-above 0.
• Because μ is unconstrained, this quantity need not lie in [0, 1] and may be negative.

Dependencies. Uses matchScoreLaw (definition 1).

---

3. tieProb

noncomputable def tieProb (μ : ℤ → ℝ) (N : ℕ) : ℝ := matchScoreLaw μ N 0

Type. Takes μ : ℤ → ℝ and N : ℕ; returns a real number.

Computation. Simply the single value of the N-th iterate at the integer 0:

tieProb(μ, N) = L(μ, N, 0)

Edge cases.

• N = 0: by the base case of definition 1, this is 1 (the point mass at 0 evaluated at 0). So tieProb(μ, 0) = 1 for every μ, including μ ≡ 0.
• N = 1: equals μ(0).
• Unconstrained sign/magnitude, as above.

Dependencies. Uses matchScoreLaw (definition 1).

---

4. fairCoinWinProb

noncomputable def fairCoinWinProb (μ : ℤ → ℝ) (N : ℕ) : ℝ :=
  strictWinProb μ N + tieProb μ N / 2

Type. Takes μ : ℤ → ℝ and N : ℕ; returns a real number.

Computation. By Lean's operator precedence, / binds tighter than +, so this is

fairCoinWinProb(μ, N) = strictWinProb(μ, N) + (tieProb(μ, N) / 2)
                      = ( Σ_{z=1}^{N} L(μ, N, z) ) + L(μ, N, 0)/2

The division is real division by the literal 2 (nonzero), so there is no junk-value issue.

Edge cases.

• N = 0: strictWinProb is 0 (empty sum) and tieProb is 1, giving fairCoinWinProb(μ, 0) = 1/2, again for every μ including the identically-zero one.
• N = 1: μ(1) + μ(0)/2.
• Nothing in the definition ties this quantity to the complementary quantity built from negative z; there is no normalization statement anywhere.

Dependencies. Uses strictWinProb (2) and tieProb (3), hence transitively matchScoreLaw (1).

---

5. bestOfWinProb

noncomputable def bestOfWinProb (m : ℕ) (q : ℝ) : ℝ :=
  ∑ k ∈ (Finset.range (m + 1)).filter (fun k => m < 2 * k),
    (m.choose k : ℝ) * q ^ k * (1 - q) ^ (m - k)

Type. Takes m : ℕ and q : ℝ (q entirely unconstrained — not required to lie in [0, 1]); returns a real number.

Computation. Finset.range (m + 1) is the set {0, 1, …, m}. It is filtered by the decidable natural-number predicate m < 2·k, i.e. 2k ≥ m + 1, i.e. k > m/2 in the rational sense. Over the surviving k the sum is of binomial terms:

bestOfWinProb(m, q) = Σ over k in {0,…,m} with 2k > m  of  C(m, k) · q^k · (1 − q)^(m − k)

where C(m, k) = Nat.choose m k is coerced from ℕ into ℝ, and the exponents are natural-number powers.

Concretely the filter selects:

• m = 2t (even): k ∈ {t+1, …, m};
• m = 2t+1 (odd): 2k > 2t+1 ⟺ k ≥ t+1, so k ∈ {t+1, …, m}.

Edge cases.

• Natural subtraction m − k: harmless here, because the index set is a subset of {0, …, m}, so k ≤ m always and m − k is the ordinary difference. No truncation occurs.
• m = 0: Finset.range 1 = {0}, and the filter condition is 0 < 0, which is false, so the index set is empty and bestOfWinProb(0, q) = 0 for every q.
• m = 1: only k = 1 survives (1 < 2), giving C(1,1)·q¹·(1−q)⁰ = q.
• m = 2: only k = 2 survives, giving q².
• m = 3: k ∈ {2, 3}, giving 3q²(1−q) + q³.
• Zero powers: Mathlib's Monoid.npow gives x⁰ = 1 for all real x, including 0⁰ = 1; so the k = m term is C(m,m)·q^m·1 even when q = 1, and terms with q = 0 vanish because every surviving k satisfies 2k > m ≥ 0, hence k ≥ 1 whenever the index set is nonempty.
• q = 0: every surviving term has k ≥ 1, so bestOfWinProb(m, 0) = 0 for every m.
• q = 1: only the k = m term is nonzero (all others carry a factor (1−q)^(m−k) = 0^(positive) = 0), and k = m always satisfies 2m > m for m ≥ 1, so bestOfWinProb(m, 1) = 1 for m ≥ 1 and 0 for m = 0.
• q outside [0, 1]: permitted; the value is then whatever the polynomial evaluates to and may be negative or exceed 1.
• The condition is a strict inequality m < 2k (equivalently 2k > m), so the exactly-half case 2k = m (possible only when m is even) is excluded from this sum.

Dependencies. None (only Mathlib's Finset.range, Finset.filter, Nat.choose).

---

6. bestOfTieProb

noncomputable def bestOfTieProb (N : ℕ) (q : ℝ) : ℝ :=
  if Even N then (N.choose (N / 2) : ℝ) * q ^ (N / 2) * (1 - q) ^ (N / 2) else 0

Type. Takes N : ℕ and q : ℝ (unconstrained); returns a real number.

Computation. A two-branch conditional on the decidable predicate "N is even":

bestOfTieProb(N, q) = C(N, N/2) · q^(N/2) · (1 − q)^(N/2)   if N is even
                    = 0                                      if N is odd

Here N/2 is natural-number (floor) division, but it is only used inside the even branch, where 2·(N/2) = N exactly, so the floor is not lossy in the branch that is actually taken. The odd branch discards q entirely.

Edge cases.

• N = 0: 0 is even, N/2 = 0, C(0,0) = 1, and q⁰ = (1−q)⁰ = 1, so bestOfTieProb(0, q) = 1 for every real q, including q outside [0,1].
• N = 1: odd, so the value is 0 regardless of q.
• N = 2: C(2,1)·q·(1−q) = 2q(1−q).
• Because the conditional is on Even N and Lean's Even on ℕ is decidable, the if resolves definitionally for each numeral; there is no classical-choice junk.
• q is unconstrained, so the value may be negative (e.g. N = 2, q = 2 gives 2·2·(−1) = −4).

Dependencies. None.

---

7. bestOfFairCoinWinProb

noncomputable def bestOfFairCoinWinProb (N : ℕ) (q : ℝ) : ℝ :=
  bestOfWinProb N q + bestOfTieProb N q / 2

Type. Takes N : ℕ and q : ℝ; returns a real number.

Computation. Again / binds tighter than +:

bestOfFairCoinWinProb(N, q) = bestOfWinProb(N, q) + ( bestOfTieProb(N, q) / 2 )

i.e. the strict-majority binomial sum from definition 5 plus one half of the exact-half binomial term from definition 6.

Edge cases.

• N = 0: bestOfWinProb(0, q) = 0 (empty sum) and bestOfTieProb(0, q) = 1, so the value is 1/2 for every q — including q = 0 and q = 1.
• N = 1: q + 0/2 = q.
• N = 2: q² + 2q(1−q)/2 = q² + q(1−q) = q.
• N = 3: 3q²(1−q) + q³ + 0.
• Division is by the nonzero literal 2, so no junk value arises.

Dependencies. Uses bestOfWinProb (5) and bestOfTieProb (6).

---

8. nestedBestOfWinProb

noncomputable def nestedBestOfWinProb : List ℕ → ℝ → ℝ
  | [],      q => q
  | m :: ms, q => bestOfWinProb m (nestedBestOfWinProb ms q)

Type. Takes a list of natural numbers and a real number; returns a real number. Both arguments appear after the colon, so the recursion is structural on the list, with q carried unchanged.

Computation.

• Empty list: returns q unchanged — the identity function on the second argument.

• Cons cell m :: ms: applies the single-level function B(m, ·) to the value obtained by recursing on the tail:

  nestedBestOfWinProb(m :: ms, q) = B( m , nestedBestOfWinProb(ms, q) )
  

Unrolled. For a list [m₁, m₂, …, m_k],

nestedBestOfWinProb([m₁,…,m_k], q) = B(m₁, B(m₂, … B(m_k, q) … ))

So the head of the list is the outermost function application and the last element is applied first, directly to q. Evaluation order in the composition: q is fed to B(m_k, ·) first, and the head m₁'s B is applied last, producing the returned value.

Edge cases.

• Empty list: the result is exactly q, with no binomial computation at all — the value is unaltered, so it can be any real number including one outside [0,1].
• Singleton [m]: the result is B(m, q), i.e. definition 5 applied once.
• A zero anywhere in the list: if some mᵢ = 0, then B(0, x) = 0 (empty filtered sum), so the value at that level is 0; and for every m, B(m, 0) = 0 (as noted in definition 5, every surviving index has k ≥ 1, and B(0, ·) = 0 anyway). Hence a single 0 entry forces the whole nested value to 0, regardless of q and of the other entries.
• A 1 anywhere in the list: B(1, x) = x, so entries equal to 1 act as the identity and can be inserted or deleted without changing the value.
• q unconstrained: intermediate values are not clamped to [0, 1]; if q lies outside [0, 1], each level is just polynomial evaluation and results may be negative or exceed 1.
• The list length is arbitrary, including length 0; the definition terminates because each recursive call is on the strictly shorter tail.

Dependencies. Uses bestOfWinProb (5). It does not use bestOfTieProb or bestOfFairCoinWinProb — the fair-coin tie handling of definitions 6 and 7 plays no role at any nesting level.

---

9. scoredSetLaw

noncomputable def scoredSetLaw (a b c q : ℝ) : ℤ → ℝ := fun z =>
  if z = 1 then q * a + (1 - q) * c
  else if z = -1 then q * c + (1 - q) * a
  else if z = 0 then b
  else 0

Type. Takes four real numbers a, b, c, q — all completely unconstrained (no nonnegativity, no a + b + c = 1, no q ∈ [0, 1]) — and returns a function ℤ → ℝ.

Computation. A cascade of decidable integer-equality tests, resolved in the written order (z = 1 first, then z = −1, then z = 0):

scoredSetLaw(a,b,c,q)(z) = q·a + (1 − q)·c    if z = 1
                         = q·c + (1 − q)·a    if z = −1
                         = b                  if z = 0
                         = 0                  for every other integer z

The three tested values 1, −1, 0 are pairwise distinct, so the cascade order is not observable: no earlier branch shadows a later one.

Structural observations.

• The value at +1 and the value at −1 are the two "crossed" mixtures of a and c with weights q and 1 − q: the +1 branch is q·a + (1−q)·c and the −1 branch swaps the roles of a and c, giving q·c + (1−q)·a. The parameter b appears only at z = 0, and q does not appear at z = 0 at all.

• Total mass over ℤ: only three integers give nonzero values, and their sum telescopes to

  (q·a + (1−q)·c) + (q·c + (1−q)·a) + b = a + c + b
  

  independently of q. So the returned function sums to 1 exactly when a + b + c = 1 — which is not required by the definition.

• Symmetry: the function is symmetric under z ↦ −z exactly when q·a + (1−q)·c = q·c + (1−q)·a, i.e. when (2q − 1)(a − c) = 0, i.e. when q = 1/2 or a = c.

• With q = 1 the values are (a, b, c) at (+1, 0, −1); with q = 0 they are (c, b, a).

Edge cases.

• Nothing prevents negative values, so the returned function need not be a probability weight.
• Every integer outside {−1, 0, 1} is sent to 0, so the function has finite support of size at most 3.

Dependencies. None, and nothing in this file depends on it. Its result type ℤ → ℝ matches the type of the argument μ of matchScoreLaw (definition 1), and matchScoreLaw consults exactly the three points {−1, 0, 1} on which this function is supported, but the file contains no definition that composes them; the connection is not made anywhere in the code read.

---

Dependency summary

matchScoreLaw ──┬──> strictWinProb ──┐
                │                    ├──> fairCoinWinProb
                └──> tieProb ────────┘

bestOfWinProb ──┬──> bestOfFairCoinWinProb   (with bestOfTieProb)
                └──> nestedBestOfWinProb

bestOfTieProb ─────> bestOfFairCoinWinProb

scoredSetLaw   (isolated: uses nothing, used by nothing)

Two disjoint clusters plus one isolated definition. Cluster A (matchScoreLaw, strictWinProb, tieProb, fairCoinWinProb) is parameterized by an arbitrary weight function μ : ℤ → ℝ and a count N : ℕ. Cluster B (bestOfWinProb, bestOfTieProb, bestOfFairCoinWinProb, nestedBestOfWinProb) is parameterized by a size m or N : ℕ and a real q, and never mentions μ or ℤ. scoredSetLaw produces an object of the type Cluster A consumes, but no declaration in this file links the two.

Cross-cutting notes

1. No hypotheses anywhere. Not one definition carries a side condition. Every parameter (μ, q, a, b, c) ranges over its full type. In particular nothing asserts that any of these functions returns a value in [0, 1], and several of them provably do not for suitable inputs.
2. Only three points of μ matter. matchScoreLaw and everything above it depend on μ solely through the triple (μ(−1), μ(0), μ(1)).
3. Natural-number arithmetic. Two places involve ℕ-specific operations: the exponent m − k in bestOfWinProb (never truncating, since k ≤ m on the index set) and N / 2 in bestOfTieProb (floor division, but used only in the branch where N is even, so exact there). Integer subtraction z − j in matchScoreLaw is ordinary ℤ subtraction.
4. Empty-structure conventions carry real weight. Three values are produced by empty structures rather than by explicit code: strictWinProb(μ, 0) = 0 (empty Finset.Icc 1 0), bestOfWinProb(0, q) = 0 (empty filter), and nestedBestOfWinProb([], q) = q (empty list base case). Combined with the base cases tieProb(μ, 0) = 1 and bestOfTieProb(0, q) = 1, the two "fair coin" definitions both return 1/2 at size 0 for all parameter values.
5. Strict vs. non-strict. strictWinProb sums from z = 1, excluding z = 0. bestOfWinProb uses the strict inequality m < 2k, excluding the exact-half index 2k = m. Both exclusions are then partially compensated by separate half-weighted terms in fairCoinWinProb and bestOfFairCoinWinProb.
6. List orientation. In nestedBestOfWinProb the list head is the outermost application and the list tail is applied nearer to q; the last list element is the first bestOfWinProb applied.