Proof of `Decoding the actual registered LP solver output`
groundedproofs/Lax263307Proofs/RegisteredLP.lean · lax-263307
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The registered solver returns exactly the encoding of a valid certificate. Parsing that encoding reconstructs the same certificate, so the total fallback branch is unreachable on these outputs.