Guardat en:
| Autor principal: | |
|---|---|
| Format: | Recurso digital |
| Idioma: | |
| Publicat: |
Zenodo
2026
|
| Accés en línia: | https://doi.org/10.5281/zenodo.19652939 |
| Etiquetes: |
Afegir etiqueta
Sense etiquetes, Sigues el primer a etiquetar aquest registre!
|
Taula de continguts:
- <p>Yang--Mills Full Native Package Boundary Standalone Lean snapshot for the Yang--Mills slice of the wider MaleyLean project, aligned with the current manuscript-facing native package boundary.</p> <p>Main result The main win in this repository is not just a theorem register or a packaging cleanup. The real advance is that the four highest-risk analytic seams in the current Yang--Mills manuscript-facing route are now mechanized much more explicitly and much more locally than before.</p> <p>Those four critical seams are:</p> <p>the QE3 density / graph-core handoff the dyadic-to-continuous-time OS upgrade the continuum transport / sharp-gap bridge the Section 8 endpoint / admissibility bridge In the current export, those seams are no longer left as vague route-level transitions. They are exposed through reduced payloads, source-grounded projections, proof-home projections, route recoveries, and theorem-level reconstructions inside the standalone Lean package.</p> <p>That is the central human-facing message of this repo: the decisive seam logic is now isolated, named, crosswalked back to source ownership, and compiled into an axiom-free manuscript-facing package boundary.</p> <p>Start here If you are new to this repository, the naming split is:</p> <p>MaleyLean is the Lean package name YangMills is the paper/topic packaged in this standalone export The main entry points are:</p> <p>Main.lean the single canonical standalone entry point; it loads MaleyLean.YangMillsFullManuscriptNativePackage BundleMain.lean optional broader bundle that loads the full native package and its summary surface together If you want one file to inspect first, start with Main.lean.</p> <p>Contents MaleyLean/ standalone Lean dependency closure for the current Yang--Mills manuscript package boundary Checks/Axiom/YangMillsFullManuscriptNativePackageAxiomCheck.lean dedicated top-package axiom audit entry point paper/ bundled manuscript source tree, source archive, and supplied PDFs reports/audits/yang_mills_submission_layer_audit_2026-04-15.md referee-facing audit note for the current top package boundary reports/support_maps/yang_mills_support_map.txt manuscript-to-Lean support map reports/status/yang_mills_status.md human-readable status note reports/submission/ editor/referee-facing submission support notes Build This project uses Lean v4.28.0 via lean-toolchain.</p> <p>Build the extracted project with:</p> <p>lake build Build the single canonical paper entry point with:</p> <p>lake env lean Main.lean Run the dedicated top-package axiom check with:</p> <p>lake env lean Checks\Axiom\YangMillsFullManuscriptNativePackageAxiomCheck.lean Scope This repo packages the current strongest manuscript-facing Yang--Mills native boundary available in the source development: the constructive, vacuum-gap, and endpoint theorem-object, proof-home, law-atom, primitive, certificate, trace, and construction-stage layers tied together in YangMillsFullManuscriptNativePackageExportStatement.</p> <p>Most importantly, that package now foregrounds the analytical mechanization of the four critical seams listed above, so the hardest manuscript transitions are not only asserted globally but tracked through explicit local bridge objects and reconstruction paths.</p> <p>It also bundles the current manuscript tree rooted in core.tex, companion1.tex, companion2.tex, and companion3.tex, together with the anonymized source archive, anonymized companion PDFs, and the proof-kernel extraction materials.</p> <p>This repository should be read as a strong manuscript-facing formal companion to the current Yang--Mills submission boundary. It is not yet a claim that every underlying analytic Yang--Mills argument has already been fully internalized as foundational Lean analysis.</p> <p>About Lean4 formalization, no axiom support</p> <p>Resources <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net#readme-ov-file"> Readme</a> License <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net#Apache-2.0-1-ov-file"> Apache-2.0 license</a> <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/activity"> Activity</a> Stars <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/stargazers"> 0 stars</a> Watchers <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/watchers"> 0 watching</a> Forks <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/forks"> 0 forks</a> <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/releases">Releases 3</a> ym-paper-v1.1.0: Hardened manuscript-facing Lean verification boundary Latest 4 days ago <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/releases">+ 2 releases</a> <a href="https://github.com/users/somamaley-ux/packages?repo_name=Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net">Packages</a> No packages published <a href="https://github.com/somamaley-ux/Vacuum-sector-mass-gap-for-the-local-gauge-invariant-sharp-local-Yang-Mills-net/packages">Publish your first package</a> Contributors 1 @<a href="https://github.com/somamaley-ux">somamaley-ux</a> somamaley-ux Languages Lean 57.9%</p> <p>TeX 42.1% Footer © 2026 GitHub, Inc. Footer navigation <a href="https://docs.github.com/site-policy/github-terms/github-terms-of-service">Terms</a> <a href="https://docs.github.com/site-policy/privacy-policies/github-privacy-statement">Privacy</a> <a href="https://github.com/security">Security</a></p>