Fock_SPR

This branch contains a compact proof-checking layout for two formalization tracks in Lean 4.

The public Lean entry points were carefully human-curated, and are deliberately small:

• Constant.lean: the one-dimensional explicitly quantitative Fock-space local stability.
• DimdPoly.lean: the d-dimensional Hermite-Fock stable phase retrieval theorem.

Each top-level proof folder (Constant/ and DimdPoly/) follows the same basic organization:

• ScaffoldingNotes/: LLM-generated mathematical notes used to generate Lean scaffolding.
• Internal/: proof Lean modules used by the public entry point (autoformalization output).
• ProofSketch/: LLM-generated natural-language proof notes and source documents.
• Comparator/: standalone challenge, solution wrapper, and comparator config.

Build

Use Lake from the repository root:

lake build Constant
lake build DimdPoly
lake build

The default target in lakefile.toml is DimdPoly.

Comparator Checks

The repository includes comparator setups for both public proof tracks:

• Constant/Comparator/config.json
• DimdPoly/Comparator/config.json

The challenge files import only Mathlib and restate the public theorem types. The solution files are thin wrappers around Constant.lean and DimdPoly.lean, so the checked solution stays synchronized with the reviewer-facing entry points.

Run both comparator checks with:

./scripts/run_local_comparator.sh

If the comparator tools are not installed locally, use:

./scripts/setup_local_comparator_linux.sh

See Comparator.md for the short comparator setup note.

Reading Order

For a quick audit, start with the public entry point, then move to the matching scaffolding notes and proof sketch:

d-dimensional hermite case

1. DimdPoly.lean
2. DimdPoly/README.md
3. DimdPoly/Comparator/Challenge.lean
4. DimdPoly/ScaffoldingNotes/00_overview.md

Constant case

1. Constant.lean
2. Constant/README.md
3. Constant/Comparator/Challenge.lean
4. Constant/ScaffoldingNotes/00_overview.md

The Internal/ folders are intended for detailed Lean proof inspection rather than as first-pass reading material.