perf: forward and backward borrow propagation is non-forced

[hargoniX]

This PR changes the behavior of forward and backward projection propagation in the context of user defined borrows. The reason to have them be "forced" override (i.e. override user annotations as well) was that a user annotated borrowed value can potentially flow into a reset-reuse transitively through a projection and must thus have accurate reference count. The reasons that this is no longer necessary are:

1. Forward never had to be forced anyways, it can only affect the z in let z := oproj x i which can't be annotated by a user
2. Backward is no longer necessary as the forward propagator for user annotations prevents the reset-reuse insertion from working with values that have user defined borrow annotations entirely.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 040275c against b5036e4 are in. There are no significant changes. @hargoniX

• ✅ build//instructions: -1.9G (-0.02%)

Small changes (3✅)

• ✅ build/profile/interpretation//wall-clock: -307ms (-6.08%)
• ✅ size/compile/.out//bytes: -5MiB (-0.27%)
• ✅ size/libleanshared.so//bytes: -300kiB (-0.21%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b5036e4d81b399447a5c9f684da2d46d84910854 --onto 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-23 21:43:27)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b5036e4d81b399447a5c9f684da2d46d84910854 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-23 21:43:28)