lean_workbook_plus_8676

⚠️ 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.

If you round after each day $4 \cdot 130\%$ is around 5. $5 \cdot 130\%$ is around 7. $7 \cdot 130\%$ is around 9. $9 \cdot 130\%$ is around 12. $12 \cdot 130\%$ is around 16. $16 \cdot 130\%$ is around 21. $21 \cdot 130\%$ is around 27. $27 \cdot 130\%$ is around 35. $35 \cdot 130\%$ is around 46. $46 \cdot 130\%$ is around 60. $60 \cdot 130\%$ is around 78. $78 \cdot 130\%$ is around 101. $101 \cdot 130\%$ is around $\boxed{131}$

Why this node was retired

The posted statement is

theorem lean_workbook_plus_8676 :
  Int.floor ((4 : ℝ) * 1.30) = 5 ∧ Int.floor ((5 : ℝ) * 1.30) = 7 ∧ Int.floor ((7 : ℝ) * 1.30) = 9 ∧ Int.floor ((9 : ℝ) * 1.30) = 12 ∧ Int.floor ((12 : ℝ) * 1.30) = 16 ∧ Int.floor ((16 : ℝ) * 1.30) = 21 ∧ Int.floor ((21 : ℝ) * 1.30) = 27 ∧ Int.floor ((27 : ℝ) * 1.30) = 35 ∧ Int.floor ((35 : ℝ) * 1.30) = 46 ∧ Int.floor ((46 : ℝ) * 1.30) = 60 ∧ Int.floor ((60 : ℝ) * 1.30) = 78 ∧ Int.floor ((78 : ℝ) * 1.30) = 101 ∧ Int.floor ((101 : ℝ) * 1.30) = 131   :=  by sorry

Nearest-integer rounding is translated as floor, which already gives floor(6.5)=6 rather than 7.

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

Proposed corrected statement

Define the chosen nearest-integer rule (ties upward for the stated chain), recursively round each 30% increase, and verify the final value 131.

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.