Repository navigation
Reduce the finite exceptional interval in actual survival count bounds #164
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| pull_request: | |
| jobs: | |
| lean: | |
| name: Lean CI | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Test proof-escape scanner | |
| run: python3 scripts/test_check_proof_escapes.py | |
| - name: Check generated first-crossing certificates | |
| run: python3 scripts/generate_first_light_1024.py --check | |
| - name: Build and setup Lean | |
| id: lean-action | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| # The project has no Lake test target, so keep testing disabled. | |
| auto-config: false | |
| build: true | |
| # Build the library before lean-action saves the Lake cache. | |
| build-args: Collatz | |
| test: false | |
| # lean-action caches the .lake directory by default; make it explicit. | |
| use-github-cache: true | |
| - name: Check integrity | |
| run: ./scripts/check_integrity.sh | |
| - name: Check anchored barriers and finite cycle certificates | |
| run: | | |
| python3 scripts/audit_barrier_kernel.py | |
| python3 scripts/audit_interval_capacity.py | |
| python3 scripts/audit_floor_excursion.py | |
| python3 scripts/audit_five_band_clock.py | |
| python3 scripts/audit_rational_band_obstruction.py | |
| python3 scripts/audit_wider_band_clock.py | |
| python3 scripts/audit_six_band_prefixes.py | |
| python3 scripts/audit_balanced_offset.py | |
| python3 scripts/audit_balanced_near_six.py | |
| python3 scripts/audit_coefficient_band.py | |
| python3 scripts/audit_floor_affine_error.py | |
| python3 scripts/audit_floor_product_error.py | |
| python3 scripts/audit_product_spread_obstruction.py | |
| python3 scripts/audit_floor_budget_comparison.py | |
| python3 scripts/audit_exact_trace_product.py | |
| python3 scripts/audit_floor_product_descent.py | |
| python3 scripts/audit_product_delay_certificates.py | |
| python3 scripts/audit_product_thresholds.py | |
| python3 scripts/audit_coefficient_gap_threshold.py | |
| python3 scripts/audit_sharp_finite_survival.py | |
| python3 scripts/audit_sharp_survival_counts.py | |
| python3 scripts/audit_eleven_halves_clock.py | |
| - name: Check exact first-descent intervals | |
| run: | | |
| python3 scripts/descent_intervals.py --check | |
| python3 scripts/test_descent_intervals.py | |
| python3 scripts/audit_descent_intervals.py | |
| - name: Check coefficient crossing and interval transfer | |
| run: python3 scripts/audit_coefficient_descent.py | |
| - name: Check stopping atlas and horizon extension | |
| run: python3 scripts/audit_stopping_atlas.py | |
| - name: Check depth-fifteen passage atlas and horizon 2592 | |
| run: python3 scripts/audit_passage_atlas.py |