Commit 2026-10-17 13:25 f2e1ddd9

feat(Algebra/Order/Floor): floor-of-sum dichotomy via fractional parts (#41861) This PR adds four lemmas in Mathlib/Algebra/Order/Floor/Ring.lean, placed in the fractional-part section, complementing the existing one-sided bounds le_floor_add and le_floor_add_floor. Here are the lemmas:

• floor_add_eq — writes ⌊a + b⌋ exactly as ⌊a⌋ + ⌊b⌋ + ⌊fract a + fract b⌋
• floor_add_eq_add_iff — the floors add exactly ⟺ the fractional parts sum below 1
• floor_add_eq_add_add_one_iff — the +1 case ⟺ the fractional parts sum to at least 1
• floor_add_eq_or — the dichotomy: it's always one or the other The library has the two inequalities but not the exact case analysis, and this closes that small gap. In addition, these are the lemmas for the mechanical/Beatty-word development proposed here --https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Sturmian.20.28mechanical.29.20words/near/610836902. Claude helped draft the Lean code; I reviewed the code, built the module locally, and it compiled.