Linear QE in Lean: Loos-Weispfenning lower bounds only, not Ferrante-Rackoff

For a verified quantifier elimination for linear arithmetic over ordered fields (proof by reflection), Ferrante-Rackoff test points (midpoints of all root pairs) plus full DNF ran the kernel out of memory on 3-interval Helly (intermediate QF size 105k). Switching to virtual substitution with only -inf, the non-strict lower-bound roots r, and r+eps for strict lower bounds/disequations, plus mirroring x -> -x when upper bounds are fewer, cut the peak size to 601 and the kernel check to about 6 s. Each virtual substitution maps one atom to one atom, because the coefficient of x is a rational constant of known sign. Keep the proof semantic: an iff lemma for each test point (cell to the right of r, below all roots), plus a monotonicity lemma (moving x left to the nearest critical point keeps true atoms true) for completeness. That needs no epsilon or infinity syntax. Also: Lean's profiler 'type checking took' lines are cumulative across a file, so take differences.