lean_workbook_plus_3777

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Over the next two points, the probability that the score becomes Y: 11, J: 9 (Yizheng Wins) = $\frac{9}{100}$ , the probability that the score becomes Y: 9, J: 11 (Jennifer wins) is $\frac{49}{100}$ , and the probability that the score becomes Y: 10 J: 10 is $\frac{42}{100}$ . Given it becomes tied again, the probabilities for each player winning stay the same because the game is win-by-two. So the probability that yizheng wins 12:10 the probability that the game becomes tied at 10 times the probability that yizheng wins at the tie = $\frac{42}{100} \times \frac{9}{100}$ . We can see that the probability that he wins with each successife score is a geometric sequence. So the probability that Yizheng wins can be expressed as: $\left(\frac{9}{100}\right) + \left(\frac{42}{100}\right)*\left(\frac{9}{100}\right) + \left(\frac{42}{100}\right)*\left(\frac{42}{100}\right)*\left(\frac{9}{100}\right) \cdots = \frac{9/100}{1-(42/100)}=\frac{9/100}{58/100}=\boxed{\frac{9}{58}}$

Why this node was retired

The posted statement is

theorem lean_workbook_plus_3777  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a + b + c = 1)
  (h₂ : a = 9 / 100)
  (h₃ : b = 49 / 100)
  (h₄ : c = 42 / 100) :
  a / (1 - b) = 9 / 58   :=  by sorry

The geometric return probability c=42/100 was replaced by opponent-win probability b=49/100 in the denominator.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Prove the winning probability a/(1−c)=9/58, with a=9/100,c=42/100, and use a genuine geometric-series/probability model if claiming the game result.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.