Add optional structured verification results

[williamjblair]

Adds --result-json FILE so callers can distinguish proof rejection from execution failure without parsing logs. The ordinary CLI and M.run calling convention remain available.

• Versioned JSON records outcome, stopped stage, reason, parsed configuration and Lean version.
• Target/axiom/builtin-kernel rejection is distinct from build, export, parse and external-process errors.
• Output files must be new. Missing, partial or malformed results never establish acceptance.
• Callers still own input/executable bindings, containment and authenticated receipts; this does not change sandbox guarantees.

Validation: pinned Lean 4.34.0-rc2 builds with --wfail on Linux. Seven real-fixture/result scenarios cover pass/rejection/errors, legacy exit behavior and refusal to overwrite results. Eight existing fixtures pass. These local tests used the upstream development launcher, not a production sandbox qualification. The pinned macOS Lake runtime crashed before elaboration; Linux validation is recorded instead.

Supports the FC review/verification architecture alongside google-deepmind/formal-conjectures#4899 and #5337. It does not require LeanEval changes.