Skip to content

Add paper_nucleon_binding Lean modules and Lake build target#13

Open
disregardfiat wants to merge 1 commit into
mainfrom
paper/nucleon_binding_support
Open

Add paper_nucleon_binding Lean modules and Lake build target#13
disregardfiat wants to merge 1 commit into
mainfrom
paper/nucleon_binding_support

Conversation

@disregardfiat
Copy link
Copy Markdown
Collaborator

Summary

  • Adds Lean import closure for the nucleon-binding Tier-2 note (papers/nucleon_binding/hqiv_nucleon_binding_from_composite_trace.tex): binding ledger, three-ledger β decay, outside-curvature environment, and H₂O phase geometry/response modules.
  • New Lake target paper_nucleon_binding (146 modules); regenerate globs with python3 scripts/paper_nucleon_binding_globs.py.
  • Adds scripts/paper_nucleon_binding_globs.py and scripts/bundle_nucleon_binding_scripts.py (Zenodo scripts bundle helper in the private papers repo).

Test plan

  • lake build paper_nucleon_binding (3347 jobs, green locally)
  • lake build HQIVLeptonResonance (default CI target, green locally)
  • CI Lean Action on this PR

Paper linkage

Tier-2 #7 nucleon binding; upstream TUFT+SM: Zenodo 10.5281/zenodo.20517172. Companion reproducer bundle: papers/nucleon_binding/scripts.zip + MANIFEST.sha256 in the HQIV-LEAN papers tree.

Made with Cursor

Sync import closure for the nucleon-binding Tier-2 note (binding ledger,
beta-decay slots, H2O phase geometry/response). Build verified locally:
lake build paper_nucleon_binding && lake build HQIVLeptonResonance.

Co-authored-by: Cursor <cursoragent@cursor.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant