The two things, Perseus and what Daan calls "FIP" here are a bit apples/oranges. But they are very related. FBIP/Perseus is an algorithm for efficient reference counting with reuse. "FIP" is actually a calculus (and thus a class of programs) for which you can guarantee in place updates. It's like the difference between an interface and an implementation of that interface. Perseus is an algorithm (implementation), FIP is a calculus (interface which can be implemented multiple ways.)
So yes, Lean 4 does use "FBIP", but "FBIP" is sort of more like an evaluation/compilation strategy, it's not any one algorithm or specific semantics. To be more precise, Lean uses Perseus, which basically has the insight "if an object's refcount is 1, I can do an in place update." You could say FIP is the natural evolution from taking a specific algorithm -- Perseus -- and sort of taking it and thinking about it from a language design POV. Perseus is the dynamic runtime implementation of FIP. But the calculus also has a static approach, too, which the paper describes using a uniqueness-typing algorithm.
These things do influence the language directly and are visible to programmers, so I don't think it's fair to say Lean 4 uses the FIP calculus described in this specific paper. For example, this semantic calculus is going to be user-visible in the next release of Koka; you'll be able to annotate functions as 'fip' or 'fbip' where the compiler will do linearity checks on the given function to guarantee that it doesn't use stack space, without needing the code generator to insert the dynamic reference counting checks required by Perseus. This also requires a notion of second-order function, stack space, etc. So it's not just some implementation detail, this is something Lean 4 would need to go out of their way to support and design for users.
So yes, Lean 4 does use "FBIP", but "FBIP" is sort of more like an evaluation/compilation strategy, it's not any one algorithm or specific semantics. To be more precise, Lean uses Perseus, which basically has the insight "if an object's refcount is 1, I can do an in place update." You could say FIP is the natural evolution from taking a specific algorithm -- Perseus -- and sort of taking it and thinking about it from a language design POV. Perseus is the dynamic runtime implementation of FIP. But the calculus also has a static approach, too, which the paper describes using a uniqueness-typing algorithm.
These things do influence the language directly and are visible to programmers, so I don't think it's fair to say Lean 4 uses the FIP calculus described in this specific paper. For example, this semantic calculus is going to be user-visible in the next release of Koka; you'll be able to annotate functions as 'fip' or 'fbip' where the compiler will do linearity checks on the given function to guarantee that it doesn't use stack space, without needing the code generator to insert the dynamic reference counting checks required by Perseus. This also requires a notion of second-order function, stack space, etc. So it's not just some implementation detail, this is something Lean 4 would need to go out of their way to support and design for users.