diff --git a/.github/workflows/ym-c308-entry-reference-center-decay.yml b/.github/workflows/ym-c308-entry-reference-center-decay.yml new file mode 100644 index 00000000..e07146bb --- /dev/null +++ b/.github/workflows/ym-c308-entry-reference-center-decay.yml @@ -0,0 +1,52 @@ +name: YM C308 entry reference center decay + +on: + push: + branches: + - verification/ym-c308-entry-reference-center-decay-20260820 + paths: + - verification/ym-c308-entry-reference-center-decay/*.lean + - .github/workflows/ym-c308-entry-reference-center-decay.yml + pull_request: + paths: + - verification/ym-c308-entry-reference-center-decay/*.lean + - .github/workflows/ym-c308-entry-reference-center-decay.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-c308-entry-reference-center-decay/FaizalShabirEntryReferenceCenterFirewall.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-c308-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-c308-entry-reference-center-decay-axle-receipt + if-no-files-found: warn + retention-days: 30 + path: /tmp/ym-c308-axle-receipt.json diff --git a/verification/ym-c308-entry-reference-center-decay/FaizalShabirEntryReferenceCenterFirewall.lean b/verification/ym-c308-entry-reference-center-decay/FaizalShabirEntryReferenceCenterFirewall.lean new file mode 100644 index 00000000..1f3b06f8 --- /dev/null +++ b/verification/ym-c308-entry-reference-center-decay/FaizalShabirEntryReferenceCenterFirewall.lean @@ -0,0 +1,33 @@ +import Mathlib + +namespace Millennium.YangMills.FaizalShabirEntryReferenceCenterFirewall + +theorem identity_center_recurrence_constant + (g : ℕ → ℝ) + (hg0 : g 0 = 1) + (hrec : ∀ n, g (n + 1) = g n) : + ∀ n, g n = 1 := by + intro n + induction n with + | zero => exact hg0 + | succ n ih => + rw [hrec n, ih] + +theorem identity_center_not_quarter_at_two + (g : ℕ → ℝ) + (hg0 : g 0 = 1) + (hrec : ∀ n, g (n + 1) = g n) : + ¬ (|g 2| ≤ (1 : ℝ) / 4) := by + have hconst := identity_center_recurrence_constant g hg0 hrec 2 + rw [hconst, abs_one] + norm_num + +theorem nonzero_multiplier_product_does_not_imply_center_decay : + (1 : ℝ) ≠ 0 ∧ ¬ ((1 : ℝ) ≤ (1 : ℝ) / 4) := by + constructor <;> norm_num + +#print axioms identity_center_recurrence_constant +#print axioms identity_center_not_quarter_at_two +#print axioms nonzero_multiplier_product_does_not_imply_center_decay + +end Millennium.YangMills.FaizalShabirEntryReferenceCenterFirewall