Gate proof leaves with Lean theorem signatures

[FluffyAIcode]

Summary

• require a single safe Lean theorem signature for every proposed minimum leaf
• typecheck signatures against pinned Lean 4.32.0-rc1 and mathlib before ledger persistence
• record FORMALIZED status and signature hash while reserving PROVED for no-sorry/no-axiom proofs
• install and build the pinned Lean gate in CI

Test plan

• 51 Python/Lean gate tests passed
• 8582-job Lean/mathlib build passed
• invalid identifiers, executable commands, axioms, and duplicate signatures are rejected

The uncommitted candidate.py file is active runtime state and is excluded.

Made with Cursor

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.