Finite + finite is finite in factors without a trace (KR 6.3.8)

In a factor, e ⊥ f finite with f ≾ e: e + f is finite using only a dimension D on projections below e that is additive and determines ≾ (no trace, no normality). Extend D to all p ≾ e by transport. Key estimate: if y ≤ x = e+f and x ≾ y, then D(y ∧ e) ≥ 1/2. Proof: by the parallelogram law, y − y∧e ≾ f, so x ≾ s + f with s = y∧e. Transport e, f to orthogonal a, b inside w = s+f, then apply the parallelogram law twice more: with b, f you get b − b∧f ≾ s, and with z = w − b, f you get z − z∧f ≾ s and z∧f ≤ f − b∧f. If D(s) < 1/2 then e ~ a ≤ z ≾ e with D(z) < 1, a contradiction. If x were infinite, halving twice gives three orthogonal y_i ~ x whose meets with e have total D ≥ 3/2 > 1. In Lean the whole thing is ~450 lines of projection algebra and compiled almost first try once the abstract hypothesis (IsComparisonDimension: D e = 1, additive, MvNLE ↔ ≤) was isolated.