Preserve active options around extracted syntax context

[kim-em]

Summary

• preserve active, unscoped set_option commands in source order with extracted variables and syntax declarations
• keep declaration-scoped set_option ... in commands from leaking onto the generated target theorem
• add Lean regression coverage for option ordering, ended sections, and scoped-option non-leakage

Why

Formal Conjectures' Erdos125.erdos_125.variants.positive_unequal_density declares set_option quotPrecheck false before two local set-builder notations. The generator copied the notations into Challenge.lean, Submission.lean, and Solution.lean without the active option, so quotation precheck rejected the generated files.

Verification

• lake build
• lake env lean --run tests/Context.lean
• python3 tests/scripts/contract.py
• python3 -m py_compile tests/scripts/*.py
• git diff --check
• generated the real Erdos 125 workspace from google-deepmind/formal-conjectures#4951 at 54abfe518d4484b74bba5470589841bb37e927c6 using this binary
• built that generated workspace successfully at its pinned Lean 4.33 / Mathlib revision; only the expected sorry warnings in Challenge.lean and Submission.lean remained

[kim-em]

Full integration evidence with #2 applied after this PR on a fresh a726789 base:

• FC PR Generate a LeanEval workspace for a Formal Conjectures declaration google-deepmind/formal-conjectures#4951 at exact head 54abfe518d4484b74bba5470589841bb37e927c6
• 100/100 FC100 declarations imported, --verify passed, and generated (92 open + 8 solved)
• 98/100 generated Challenges compiled at LeanEval's exact target pins
• Erdos125_erdos_125_variants_positive_unequal_density now compiles
• the only failures are the two already documented FC/target Mathlib-drift cases: Erdos1092 and EllipticCurveRank

The two generator commits cherry-pick without conflict and their combined generator/contract/golden suite is green. Source report SHA-256: cb85aaa1c8bed7932a449d12bcdfc7ab57a8d6d3261e17121348c0adc6517fac; target report SHA-256: cd2d41e6ad72685f2d88c70f9fc39ecd10014bad3140c4b13876488f51aa0086.

[kim-em]

Pre-review edge-case fix 988eafe: Lean permits set_option ... in <declaration> with the declaration on the same line. The previous detector only rejected scoped commands whose final token was in, so the inline form could be hoisted into generated context despite this PR’s invariant. The shared detector now recognizes the in token anywhere in the command block, with an exact inline regression. Sequential lake build, the context executable, strict contract suite, Python bytecode check, actionlint, and diff check pass without warnings.