diff --git a/.github/workflows/beal_global_audit.yml b/.github/workflows/beal_global_audit.yml new file mode 100644 index 0000000..f92bf5d --- /dev/null +++ b/.github/workflows/beal_global_audit.yml @@ -0,0 +1,47 @@ +name: Beal global audit mirror + +on: + push: + branches: + - research/beal-signature357-probe + workflow_dispatch: + +permissions: + contents: read + +jobs: + replay: + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 97b776a728b66942912a564d47b09e84078e2b1e + - name: Replay corrected global certificates + run: | + python3 scripts/check_global_beal_prime_exponent_reduction.py --self-test + python3 scripts/check_global_beal_prime_exponent_reduction.py + python3 scripts/check_global_beal_repeated_exponent_audit.py --self-test + python3 scripts/check_global_beal_repeated_exponent_audit.py + python3 scripts/check_global_beal_one_four_core.py --self-test + python3 scripts/check_global_beal_one_four_core.py + python3 scripts/check_global_beal_signature457_power_residue.py --self-test + python3 scripts/check_global_beal_signature457_power_residue.py + + lean: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 97b776a728b66942912a564d47b09e84078e2b1e + - uses: leanprover/lean-action@v1 + - name: Compile new global modules + run: | + lake env lean BealUnified/ExponentReduction.lean + lake env lean BealUnified/Research/CyclotomicAudit.lean + lake env lean BealUnified/Research/Signature457.lean + +# This mirror is intentionally pinned to one research commit. diff --git a/.github/workflows/beal_signature357_decisive.yml b/.github/workflows/beal_signature357_decisive.yml new file mode 100644 index 0000000..dcb4e31 --- /dev/null +++ b/.github/workflows/beal_signature357_decisive.yml @@ -0,0 +1,58 @@ +name: Beal global canonical audit + +on: + push: + branches: + - research/beal-signature357-probe + pull_request: + paths: + - ".github/workflows/beal_signature357_decisive.yml" + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: beal-global-canonical-audit-${{ github.ref }} + cancel-in-progress: true + +jobs: + replay: + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 97b776a728b66942912a564d47b09e84078e2b1e + path: beal + - name: Replay corrected global certificates + working-directory: beal + run: | + python3 scripts/check_global_beal_prime_exponent_reduction.py --self-test + python3 scripts/check_global_beal_prime_exponent_reduction.py + python3 scripts/check_global_beal_repeated_exponent_audit.py --self-test + python3 scripts/check_global_beal_repeated_exponent_audit.py + python3 scripts/check_global_beal_one_four_core.py --self-test + python3 scripts/check_global_beal_one_four_core.py + python3 scripts/check_global_beal_signature457_power_residue.py --self-test + python3 scripts/check_global_beal_signature457_power_residue.py + + lean: + runs-on: ubuntu-latest + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 97b776a728b66942912a564d47b09e84078e2b1e + path: beal + - uses: leanprover/lean-action@v1 + with: + lake-package-directory: beal + - name: Compile global research modules + working-directory: beal + run: | + lake env lean BealUnified/ExponentReduction.lean + lake env lean BealUnified/Research/CyclotomicAudit.lean + lake env lean BealUnified/Research/Signature457.lean diff --git a/.github/workflows/beal_signature357_mod5_137781_prime13.yml b/.github/workflows/beal_signature357_mod5_137781_prime13.yml new file mode 100644 index 0000000..49360ba --- /dev/null +++ b/.github/workflows/beal_signature357_mod5_137781_prime13.yml @@ -0,0 +1,36 @@ +name: Beal signature 357 level 137781 prime 13 filter + +on: + push: + branches: + - research/beal-signature357-probe + paths: + - ".github/workflows/beal_signature357_mod5_137781_prime13.yml" + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: beal-signature357-mod5-137781-prime13 + cancel-in-progress: false + +jobs: + prime13: + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 76cec47d35dfc38bda15b2370844bc3534af8a13 + path: beal + - name: Apply the complete prime-13 local union to both parity spaces + run: >- + python3 beal/scripts/run_signature_357_magma_mod5_137781_prime13_parity.py + > mod5-137781-prime13-parity.json + - uses: actions/upload-artifact@v4 + with: + name: signature357-mod5-137781-prime13-parity + path: mod5-137781-prime13-parity.json + if-no-files-found: error diff --git a/.github/workflows/beal_signature357_mod5_19683_raw.yml b/.github/workflows/beal_signature357_mod5_19683_raw.yml new file mode 100644 index 0000000..e2504b9 --- /dev/null +++ b/.github/workflows/beal_signature357_mod5_19683_raw.yml @@ -0,0 +1,36 @@ +name: Beal signature 357 level 19683 raw Brandt filter + +on: + push: + branches: + - research/beal-signature357-probe + paths: + - ".github/workflows/beal_signature357_mod5_19683_raw.yml" + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: beal-signature357-mod5-19683-raw + cancel-in-progress: false + +jobs: + raw: + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 72b19b2e27141c2cfe94bf2727a8c18a0392ea3c + path: beal + - name: Apply parity and removed-prime filters on the raw Brandt module + run: >- + python3 beal/scripts/run_signature_357_magma_mod5_19683_raw.py + > mod5-19683-raw.json + - uses: actions/upload-artifact@v4 + with: + name: signature357-mod5-19683-raw + path: mod5-19683-raw.json + if-no-files-found: error diff --git a/.github/workflows/beal_signature357_raw_restriction_probe.yml b/.github/workflows/beal_signature357_raw_restriction_probe.yml new file mode 100644 index 0000000..8bf0bd4 --- /dev/null +++ b/.github/workflows/beal_signature357_raw_restriction_probe.yml @@ -0,0 +1,36 @@ +name: Beal signature 357 raw Hecke restriction probe + +on: + push: + branches: + - research/beal-signature357-probe + paths: + - ".github/workflows/beal_signature357_raw_restriction_probe.yml" + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: beal-signature357-raw-restriction + cancel-in-progress: false + +jobs: + probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@v5 + with: + repository: Th0rgal/beal-conjecture-lean + ref: 767d4aadc25eac4dd4493c53c1accd30f8e7503e + path: beal + - name: Compare raw and ordinary Hecke restrictions + run: >- + python3 beal/scripts/run_signature_357_magma_hecke_raw_restriction_probe.py + > magma-hecke-raw-restriction.json + - uses: actions/upload-artifact@v4 + with: + name: signature357-magma-hecke-raw-restriction + path: magma-hecke-raw-restriction.json + if-no-files-found: error