diff --git a/.github/workflows/ym-c333-first-cumulant-color-cancellation.yml b/.github/workflows/ym-c333-first-cumulant-color-cancellation.yml new file mode 100644 index 000000000..fa393c743 --- /dev/null +++ b/.github/workflows/ym-c333-first-cumulant-color-cancellation.yml @@ -0,0 +1,52 @@ +name: YM C333 first-cumulant color cancellation + +on: + push: + branches: + - verification/ym-c333-first-cumulant-color-cancellation-20260820 + paths: + - verification/ym-c333-first-cumulant-color-cancellation/*.lean + - .github/workflows/ym-c333-first-cumulant-color-cancellation.yml + pull_request: + paths: + - verification/ym-c333-first-cumulant-color-cancellation/*.lean + - .github/workflows/ym-c333-first-cumulant-color-cancellation.yml + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-22.04 + timeout-minutes: 20 + steps: + - uses: actions/checkout@v4 + - name: Verify flattened Lean theorem source + shell: bash + run: | + set -euo pipefail + SRC=verification/ym-c333-first-cumulant-color-cancellation/FaizalShabirFirstCumulantColorCancellation.lean + if grep -nE '\b(sorry|admit|sorryAx|axiom|opaque|unsafe|native_decide|Lean\.ofReduceBool)\b' "$SRC"; then exit 1; fi + SRC="$SRC" python3 - <<'PY' + import hashlib, json, os, pathlib, urllib.request + path = pathlib.Path(os.environ['SRC']) + source = path.read_text() + payload = json.dumps({'content': source,'environment':'lean-4.30.0','ignore_imports':True,'mathlib_options':False,'timeout_seconds':900}).encode() + req = urllib.request.Request('https://axle.axiommath.ai/api/v1/check', data=payload, headers={'Content-Type':'application/json'}, method='POST') + with urllib.request.urlopen(req, timeout=960) as response: + result = json.load(response) + receipt={'source_path':str(path),'source_sha256':hashlib.sha256(source.encode()).hexdigest(),'axle_environment':'lean-4.30.0','axle_result':result} + pathlib.Path('/tmp/ym-c333-axle-receipt.json').write_text(json.dumps(receipt,indent=2)) + print(json.dumps(receipt,indent=2)) + lean=result.get('lean_messages',{}); tool=result.get('tool_messages',{}) + bad=(not result.get('okay') or bool(result.get('failed_declarations',[])) or bool(lean.get('errors',[])) or bool(lean.get('warnings',[])) or bool(tool.get('errors',[])) or bool(tool.get('warnings',[])) or 'sorryAx' in json.dumps(result)) + if bad: raise SystemExit(1) + PY + - uses: actions/upload-artifact@v4 + if: always() + with: + name: ym-c333-first-cumulant-color-cancellation-axle-receipt + if-no-files-found: warn + retention-days: 30 + path: /tmp/ym-c333-axle-receipt.json diff --git a/verification/ym-c333-first-cumulant-color-cancellation/FaizalShabirFirstCumulantColorCancellation.lean b/verification/ym-c333-first-cumulant-color-cancellation/FaizalShabirFirstCumulantColorCancellation.lean new file mode 100644 index 000000000..3251f3af0 --- /dev/null +++ b/verification/ym-c333-first-cumulant-color-cancellation/FaizalShabirFirstCumulantColorCancellation.lean @@ -0,0 +1,30 @@ +import Mathlib + +namespace Millennium.YangMills.FaizalShabirFirstCumulantColorCancellation + +theorem odd_two_point_average_zero + (f x : ℝ) + (hodd : f (-x) = -f x) : + (f x + f (-x)) / 2 = 0 := by + rw [hodd] + ring + +theorem antisymmetric_symmetric_pair_cancels + (fij fji cij cji : ℝ) + (hf : fji = -fij) + (hc : cji = cij) : + fij * cij + fji * cji = 0 := by + rw [hf, hc] + ring + +theorem antisymmetric_diagonal_zero + (fii : ℝ) + (h : fii = -fii) : + fii = 0 := by + linarith + +#print axioms odd_two_point_average_zero +#print axioms antisymmetric_symmetric_pair_cancels +#print axioms antisymmetric_diagonal_zero + +end Millennium.YangMills.FaizalShabirFirstCumulantColorCancellation