Formally audit the selected BIT stopped-recurrence implication

.github/workflows/lean-stopped-recurrence-audit.yml

@@ -0,0 +1,41 @@
+name: Lean stopped recurrence audit
+on:
+  pull_request:
+    paths:
+      - 'research/lean-stopped-recurrence-audit/**'
+      - '.github/workflows/lean-stopped-recurrence-audit.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'research/lean-stopped-recurrence-audit/**'
+      - '.github/workflows/lean-stopped-recurrence-audit.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.12'
+      - name: Download checksum-pinned official Lean
+        shell: bash
+        run: |
+          curl --fail --location --retry 3 https://github.com/leanprover/lean4/releases/download/v4.33.0-rc1/lean-4.33.0-rc1-linux.tar.zst -o "$RUNNER_TEMP/lean.tar.zst"
+          echo "25e7b3e18ec75a4e2529fc23194be8e3cc3183df99b553f870d8a111c7488210  $RUNNER_TEMP/lean.tar.zst" | sha256sum --check
+          tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP"
+      - name: Build local proofs and check actual Lean rejection controls
+        shell: bash
+        run: |
+          python -I -O -B research/lean-stopped-recurrence-audit/verify.py \
+            --lake "$RUNNER_TEMP/lean-4.33.0-rc1-linux/bin/lake" \
+            --work-dir "$RUNNER_TEMP/stopped-recurrence-build" \
+            --fetch-cache --out "$RUNNER_TEMP/stopped-recurrence-result.json"
+      - name: Source and receipt failure controls
+        run: python -I -O -B research/lean-stopped-recurrence-audit/test_package.py
+      - run: git diff --exit-code

research/lean-stopped-recurrence-audit/FINITE.json

@@ -0,0 +1,69 @@
+{
+  "bad_coefficient": "4713/11291503906250",
+  "countermodel_widths": 4097,
+  "expanding_child_witness": {
+    "C": 2,
+    "coefficient": "1/4",
+    "cost": 416200801,
+    "exponent": "9983/10000",
+    "m": 2,
+    "n": 20401,
+    "potential_upper": 416180400,
+    "rank": 4,
+    "w": 1
+  },
+  "fallback_calls": 118606528512,
+  "finite_recurrences": [
+    {
+      "finite_bound": "200*n+10000*w*floor(sqrt(n))",
+      "last_cost": "1882507489417698836809734954358942575972903095507/203065218429807812500000000000000000000000000",
+      "trace_sha256": "e027ef6c44b0204fd52ac63e3f109385a1d89ddf371c5fd2767b536f31646eb8",
+      "w": 1,
+      "widths": 4097
+    },
+    {
+      "finite_bound": "200*n+10000*w*floor(sqrt(n))",
+      "last_cost": "2312541713567156292124835933907840574598396786521/203065218429807812500000000000000000000000000",
+      "trace_sha256": "d872a80cd429985236f054dbb12de79e59a883f6d95e0260c439151bdce8aa5b",
+      "w": 3,
+      "widths": 4097
+    },
+    {
+      "finite_bound": "200*n+10000*w*floor(sqrt(n))",
+      "last_cost": "5322781282613358479330542790750126564976852623619/203065218429807812500000000000000000000000000",
+      "trace_sha256": "f31cc65d81ef4f9a0f9b26330a5e9d944aeaa222e8bd819a447525e981b18f30",
+      "w": 17,
+      "widths": 4097
+    },
+    {
+      "finite_bound": "200*n+10000*w*floor(sqrt(n))",
+      "last_cost": "216684602452071697766702674239033492889407001757/203065218429807812500000000000000000000000",
+      "trace_sha256": "f1be7426196233f6f49417529e59a9d4a91f730544d286ab30a38f046aa14f87",
+      "w": 1000,
+      "widths": 4097
+    }
+  ],
+  "fractional_margin": "417108429696410808529/45166015625000000000000000",
+  "fractional_moment_upper": "45161081915007803589191471/45166015625000000000000000",
+  "linear_moment": "2874298095721977/2890625000000000",
+  "live": 28416,
+  "maximum_rank": 42,
+  "nonmonotone_costs": [
+    0,
+    1,
+    0
+  ],
+  "power_enclosures": 8,
+  "profile": {
+    "1": 381024,
+    "2": 400416,
+    "3": 22752,
+    "4": 26880,
+    "42": 288,
+    "5": 29376,
+    "6": 17376,
+    "7": 26784
+  },
+  "schema": "stopped-recurrence-audit/1",
+  "scope": "Exact source/moment binding and finite checks only. Fractional moment is an explicit Lean hypothesis; no kernel execution or full-machine uniform cost is inferred."
+}

research/lean-stopped-recurrence-audit/POWER-BOUNDS.json

@@ -0,0 +1,18 @@
+{
+  "base_denominator": 64,
+  "denominator": 1000000000000,
+  "generation": "Decimal proposes the grid points; exact integer power comparisons certify every bound during replay.",
+  "power_denominator": 10000,
+  "power_numerator": 9983,
+  "schema": "stopped-recurrence-power-bounds/1",
+  "upper_numerators": {
+    "1": 15735861773,
+    "2": 31434660674,
+    "3": 47119500781,
+    "4": 62795282899,
+    "42": 656720084557,
+    "5": 78464333000,
+    "6": 94128020414,
+    "7": 109787249622
+  }
+}

research/lean-stopped-recurrence-audit/PROOF-SOURCES.json

@@ -0,0 +1,86 @@
+{
+  "axiom_targets": [
+    "StoppedRecurrence.worst_eq_positive",
+    "StoppedRecurrence.stopped_bound",
+    "SelectedStoppedRecurrence.exact_linear_moment",
+    "SelectedStoppedRecurrence.selected_bound",
+    "SelectedStoppedRecurrence.selected_positive_bound",
+    "SelectedStoppedRecurrence.selected_uniform_bound",
+    "RecurrenceCounterexamples.omitted_leaf_fails",
+    "RecurrenceCounterexamples.omitted_leaf_all_other_widths",
+    "RecurrenceCounterexamples.expanding_child_recurrence",
+    "RecurrenceCounterexamples.expanding_child_moments",
+    "RecurrenceCounterexamples.expanding_child_fails",
+    "RecurrenceCounterexamples.width_dependent_charge",
+    "RecurrenceCounterexamples.no_uniform_constant",
+    "RecurrenceCounterexamples.endpoint_is_not_maximum"
+  ],
+  "dependencies": {
+    "Cli": {
+      "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
+      "url": "https://github.com/leanprover/lean4-cli"
+    },
+    "LeanSearchClient": {
+      "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715",
+      "url": "https://github.com/leanprover-community/LeanSearchClient"
+    },
+    "Qq": {
+      "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
+      "url": "https://github.com/leanprover-community/quote4"
+    },
+    "aesop": {
+      "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
+      "url": "https://github.com/leanprover-community/aesop"
+    },
+    "batteries": {
+      "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366",
+      "url": "https://github.com/leanprover-community/batteries"
+    },
+    "importGraph": {
+      "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
+      "url": "https://github.com/leanprover-community/import-graph"
+    },
+    "mathlib": {
+      "rev": "55b7917b472489c7c56a0fa6393af05cfd536599",
+      "url": "https://github.com/leanprover-community/mathlib4.git"
+    },
+    "plausible": {
+      "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+      "url": "https://github.com/leanprover-community/plausible"
+    },
+    "proofwidgets": {
+      "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
+      "url": "https://github.com/leanprover-community/ProofWidgets4"
+    }
+  },
+  "files": {
+    "POWER-BOUNDS.json": "3da6cc472848ab7486968750653cc58c0d92e7b3ca1de071a9238fb4f53dd914",
+    "lean/Counterexamples.lean": "9b195d48062eeffc3147227bf8a260a2b2a035102b494f0e15159dbcdaa9a0cf",
+    "lean/Selected.lean": "1d63b79d222e3518c90a9018ee8116397361ec34bd3cba85a921bc3850a8cf45",
+    "lean/StoppedRecurrence.lean": "c6092eb394d2f97ca6cb701fc59cf79e6bcfc63e40e126e67c3b1021ca2abb95",
+    "lean/lake-manifest.json": "d15034efffe21744b6338258cb5779d73b62c81488658a81f1a0be4b46beb053",
+    "lean/lakefile.toml": "5b4ee60567128df2496dcb65608cd3a3bc4658f4ea40d3f077212b5647d9f9ce",
+    "lean/lean-toolchain": "62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef",
+    "sources/pr2234/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4",
+    "sources/pr2234/NOTICE.md": "c144e34c24470ca53df77527b9687ae9b345a4d88a506d839312ca26584cfe79",
+    "sources/pr2234/PROOF.md": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344",
+    "sources/pr2234/check_recursion.py": "6fd6504b196ad2cdcdc6bf424b268ea8c8778eb32e3c2775718f60a01f06a05e",
+    "sources/selected/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045",
+    "sources/selected/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4",
+    "sources/selected/GLOBAL.json": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819"
+  },
+  "lean_commit": "62eed1db4d67327ec8120be05f1a1b0847d74561",
+  "lean_version": "4.33.0-rc1",
+  "predecessor": {
+    "author": "Jose Manuel / jmbarrancoml",
+    "commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f",
+    "formalized_scope": "Conditional stopped-recurrence implication in section7; the full-machine local charge and fractional moment remain explicit formal hypotheses.",
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/2234"
+  },
+  "schema": "stopped-recurrence-proof-sources/1",
+  "toolchain": "leanprover/lean4:v4.33.0-rc1",
+  "toolchain_archive": {
+    "sha256": "25e7b3e18ec75a4e2529fc23194be8e3cc3183df99b553f870d8a111c7488210",
+    "url": "https://github.com/leanprover/lean4/releases/download/v4.33.0-rc1/lean-4.33.0-rc1-linux.tar.zst"
+  }
+}