Add reproducible Lean formal verification workflow

[quzhenghao]

Summary

• Add a Lean 4 formal-verification project for 20 public GeoPi data-mining contracts.
• Add a Python runtime probe and a bidirectional Python/Lean checking bridge over real classification data and production functions.
• Preserve row identity, fitted preprocessing state, label decoding state, and model-registry immutability with minimal changes to the business path.
• Add a root-level Windows and macOS reproduction and extension guide.

Paper-consistency boundary

The historical audit baseline is kept separate from the current rerun:

• First round: 13/20 passed; the seven failed checks remain D04, D05, P02, P03, L03, A02, and E02.
• The documented causes and minimal fixes for those seven checks are preserved.
• The Lean predicates, Python mirror checks, and isolated counterexamples are unchanged across rounds.
• Second round and the post-merge rerun: all 20 checks pass.
• The paper's original bridge run contained 14 pytest tests. The current branch contains 15 because one portability regression test was added for Windows/macOS log handling; this does not change the 20 propositions or either audit conclusion.

Upstream synchronization

• Merge upstream main at feeb8a53125a524c2fcaac2eaa01666b4c7fc577 before refreshing the formal evidence.
• Preserve upstream multiclass, time-series, CLI, and server-wrapper behavior while retaining the seven formal-fix semantics.
• Adapt label-codec persistence to the current label_config interface without weakening L03.
• Reject row-identity mismatches, explicitly realign reorder-only cases, and avoid mutating caller-owned row identities.
• Refresh CLI golden interactions and output manifests for split-before-fit preprocessing and the persisted codec artifact.

Validation

• Lean/Python bridge: 20/20 production checks passed; 0 failed.
• Counterexamples: 20/20 checks covered by isolated failures; all 21 suite cases matched expectations.
• Python and Lean JSON reports: semantically identical for production and counterexample suites.
• Lean 4.32.2: both builds and the fresh kernel check passed.
• Formal bridge pytest suite: 15 passed.
• Installed production wheel under Python 3.9: 107 passed.
• Cross-platform wrapper suite: 247 passed, 6 platform-specific tests skipped as designed.
• Real installed-CLI parity suite: 10 passed, 66 non-parity tests deselected.
• Black 22.10, isort 5.12, and the repository's Python 3.9 flake8 gate passed.
• Runtime evidence retained the expected 1608/403 train/test split, one fitted preprocessing state reused for inference, a two-entry persisted codec, explicit three-pair role guards, mismatch rejection, and an unchanged model registry.

Exclusions

Research-paper source materials, local graph/tool state, rendered working documents, and temporary build output are intentionally not part of this branch.