Lean statement register: statement-only Mathlib specifications of the registered claims (171 claims, 150 declarations, zero theorems)

.github/workflows/lean-specifications.yml

@@ -0,0 +1,60 @@
+name: Lean statement specifications (statements only, no proof, no scientific promotion)
+
+'on':
+  pull_request:
+    paths:
+      - 'specifications/lean_statements_20261010/**'
+      - '.github/workflows/lean-specifications.yml'
+      - 'formal/lake-manifest.json'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  statement-evidence:
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    env:
+      LEAN_NUM_THREADS: 2
+      PYTHONDONTWRITEBYTECODE: '1'
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+          fetch-depth: 0
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.11.16'
+      - name: Unit tests in both Python modes and the source check (no Lean)
+        run: |
+          set -euo pipefail
+          P=specifications/lean_statements_20261010
+          python -B -S "$P/test_check.py"
+          python -B -O -S "$P/test_check.py"
+          python -B -S "$P/check.py"
+      - name: Install pinned Lean and retrieve the Mathlib cache
+        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865
+        with:
+          lake-package-directory: specifications/lean_statements_20261010
+          auto-config: 'false'
+          build: 'false'
+          test: 'false'
+          lint: 'false'
+          use-mathlib-cache: 'true'
+          use-github-cache: 'false'
+      - name: Lean-driving unit tests on dependency-free fixture packages (environment audit and its controls, autoImplicit off)
+        run: python -B -S specifications/lean_statements_20261010/test_check.py LeanHelpers
+      - name: "Fresh build, leanchecker, #check and #print axioms of every registered statement, environment audit, negative controls, receipt"
+        run: python -B -S specifications/lean_statements_20261010/check.py --execute
+      - name: Tracked tree unchanged
+        run: git diff --exit-code
+      - name: Preserve logs and receipt
+        if: always()
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
+        with:
+          name: lean-specifications-${{ github.run_id }}-${{ github.run_attempt }}
+          path: specifications/lean_statements_20261010/.lake/evidence/
+          include-hidden-files: true
+          if-no-files-found: error
+          retention-days: 14

specifications/lean_statements_20261010/.gitignore

@@ -0,0 +1,2 @@
+.lake/
+__pycache__/

specifications/lean_statements_20261010/Specifications.lean

@@ -0,0 +1,5 @@
+import Specifications.Field
+import Specifications.Lifetime
+import Specifications.Side24
+import Specifications.RN
+import Specifications.P15

specifications/lean_statements_20261010/lake-manifest.json

@@ -0,0 +1,117 @@
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "name": "plausible",
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "LeanSearchClient",
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "importGraph",
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "e928b72544873815af278d38681b31c0293588e3",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "proofwidgets",
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "name": "aesop",
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "Qq",
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "batteries",
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "Cli",
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.34.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "name": "mathlib",
+      "url": "https://github.com/leanprover-community/mathlib4.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    }
+  ],
+  "name": "universal_law_specifications",
+  "lakeDir": ".lake",
+  "fixedToolchain": true
+}

specifications/lean_statements_20261010/lakefile.toml

@@ -0,0 +1,12 @@
+name = "universal_law_specifications"
+version = "0.1.0"
+defaultTargets = ["Specifications"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "d13f23b723b8a846827a245b89c10fc7d3f11612"
+
+[[lean_lib]]
+name = "Specifications"
+leanOptions = { autoImplicit = false }

specifications/lean_statements_20261010/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1

specifications/lean_statements_20261010/replay.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+# Local replay of the statement-only package check. Scientific effect: NONE.
+# Order: source check (fails closed before any Lean), unit tests in both Python modes, then the
+# Lean execution (fresh lake build, leanchecker, #check / #print axioms of every registered
+# declaration, the environment audit of every constant the modules add, the negative controls,
+# receipt under .lake/evidence/).
+# Extra arguments are passed to check.py (local development: --allow-dirty; a receipt produced
+# that way records the worktree as unverified and is not evidence about any commit).
+set -euo pipefail
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+P="$ROOT/specifications/lean_statements_20261010"
+cd "$ROOT"
+export PATH="$HOME/.elan/bin:$PATH"
+export PYTHONDONTWRITEBYTECODE=1
+mkdir -p "$P/.lake"
+python3 -B -S "$P/check.py" "$@"
+python3 -B -S "$P/test_check.py" 2>&1 | tee "$P/.lake/tests.log"
+python3 -B -O -S "$P/test_check.py" 2>&1 | tee "$P/.lake/tests-optimized.log"
+python3 -B -S "$P/check.py" --execute "$@"
+echo 'PASS: statements elaborated and inventoried; formal progress specified; alignment PENDING_INDEPENDENT_REVIEW; scientific effect NONE.'