Bring SoPlex presolve into the verified path

The current design (PLAN.md) forces Options.presolve := false whenever the verification layer runs (solveVerified). This keeps the bridge simple — certificates returned by SoPlex describe the original LP, so the Lean-side checker runs against the same Problem value the user passed in — at the cost of disabling SoPlex's most impactful speed optimization.

This issue tracks the alternative (option B in the plan's open-questions discussion): keep presolve enabled, and reconstruct an original-problem certificate from SoPlex's presolve transcript inside the bridge.

What it would take

• Capture SoPlex's presolve operations (substitutions, scaling, redundant-constraint removal, bound tightening) as a transcript per solve.
• Invert each operation when translating the returned primal / dual / Farkas / ray vectors into the canonical lower/upper-split form for the original problem.
• Treat the inversion code as untrusted: the Lean-side checker remains the source of truth, so a buggy inversion surfaces as Verified.unchecked rather than silently wrong math. New CI golden tests per presolve operation type.

When to revisit

Only worth doing if profiling on a real verified workload (e.g. exact polyhedral preprocessing for SOS at scale, an exact LP relaxation loop in a future MILP backend) shows presolve-disabled wall-clock is the actual bottleneck. Small LPs see no meaningful difference; this exists for sparse / structured LPs where SoPlex's presolve removes most of the work.

Risks

• Inversion logic is non-trivial and SoPlex-version-sensitive: each release that touches presolve risks silent breakage. Mitigation: pinned SoPlex release + golden tests.
• Big bridge attack surface for what is essentially a performance optimization. The whole design is "trusted oracle, untrusted bridge, pure-Lean checker"; this option grows the bridge significantly.

References

• PLAN.md § Verification layer / Decisions
• PLAN.md § What this catches (presolve leakage bullet)

Start with PLAN.md sections “Verification layer / Decisions” and “What this catches,” then profile a real verified workload to confirm presolve is the bottleneck. Done means presolve stays enabled, its operations are captured and inverted for original-problem certificates, and CI golden tests cover each presolve operation type while the Lean checker rejects incorrect translations.