[Lean] PR442 level model, phase 1: literal entrance projector has range span(q)

.github/workflows/pr442-integration.yml

@@ -0,0 +1,47 @@
+name: PR442 inherited invocation integration
+
+on:
+  push:
+    branches: [lean/pr442-level-model]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: pr442-inherited-integration-${{ github.ref }}
+  cancel-in-progress: false
+
+jobs:
+  invocation:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
+        with:
+          python-version: '3.13'
+      - name: Install the pinned Lean toolchain manager
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Install pinned extraction dependencies
+        run: python3 -m pip install -r research/lean-external-review/requirements.txt
+      - name: Fetch the pinned Mathlib cache
+        working-directory: research/lean-multi-host-source
+        run: >-
+          lake exe cache get Mathlib.Data.Matrix.Mul
+          Mathlib.Algebra.BigOperators.Fin Mathlib.Tactic.FieldSimp
+          Mathlib.Tactic.Ring Mathlib.Tactic.NormNum
+      - name: Reconstruct inputs, build modules and audit axioms
+        run: make formal-pr442-verify
+      - name: Preserve the exact-commit invocation receipt
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: pr442-inherited-invocation
+          path: /tmp/pr442-lean421-fresh.json
+          if-no-files-found: warn

.github/workflows/pr442-level-model.yml

@@ -0,0 +1,45 @@
+name: PR442 level model Phase 1
+
+on:
+  push:
+    branches: [lean/pr442-level-model]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  phase1:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
+        with:
+          python-version: '3.13'
+      - name: Install elan with the package's pinned toolchain
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Fetch the pinned Mathlib cache
+        working-directory: research/lean-pr442-level-model
+        run: >-
+          lake exe cache get Mathlib.Data.Matrix.Mul
+          Mathlib.Algebra.BigOperators.Fin Mathlib.Tactic.FieldSimp
+          Mathlib.Tactic.Ring Mathlib.Tactic.NormNum
+          Mathlib.LinearAlgebra.Span.Defs
+      - name: Build, audit and reject mutated inputs
+        working-directory: research/lean-pr442-level-model
+        run: python3 verify.py --receipt /tmp/pr442-level-model-phase1.json
+      - name: Require unchanged predecessor and package files
+        run: git diff --exit-code
+      - name: Preserve the exact build and audit receipt
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: pr442-level-model-phase1
+          path: /tmp/pr442-level-model-phase1.json
+          if-no-files-found: warn

.github/workflows/verify.yml

@@ -79,7 +79,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        package: [historical, gaussian, matrix]
+        package: [historical, gaussian, matrix, pr442]
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
@@ -96,5 +96,22 @@ jobs:
         if: matrix.package == 'historical'
         working-directory: formal/lean
         run: lake exe cache get
+      - name: Install pinned PR442 extraction dependencies
+        if: matrix.package == 'pr442'
+        run: python3 -m pip install -r research/lean-external-review/requirements.txt
+      - name: Fetch pinned PR442 Mathlib build cache
+        if: matrix.package == 'pr442'
+        working-directory: research/lean-multi-host-source
+        run: >-
+          lake exe cache get Mathlib.Data.Matrix.Mul
+          Mathlib.Algebra.BigOperators.Fin Mathlib.Tactic.FieldSimp
+          Mathlib.Tactic.Ring Mathlib.Tactic.NormNum
       - name: Check formal package and theorem axiom dependencies
         run: make formal-${{ matrix.package }}-verify
+      - name: Preserve PR442 build receipt
+        if: always() && matrix.package == 'pr442'
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: pr442-lean421-receipt
+          path: /tmp/pr442-lean421-fresh.json
+          if-no-files-found: warn

Makefile

@@ -564,6 +564,16 @@ recycled-bit-full-verify:
 verify-recycled-bit: recycled-bit-full-verify
 	python3 -m unittest discover -s tests -p 'test_recycled_bit_integration.py' -v
 
+# Literal PR442 invocation: ordinary pinned Lake build, source checks and audits.
+.PHONY: formal-pr442-verify
+LAKE ?= lake
+formal-pr442-verify:
+	python3 research/lean-multi-host-source/check_sources.py
+	python3 research/lean-multi-host-source/test_flat_data.py
+	python3 research/lean-multi-host-source/test_verifier_stack.py
+	python3 research/lean-multi-host-source/verify.py --lake "$(LAKE)" --receipt /tmp/pr442-lean421-fresh.json
+	python3 research/lean-external-review/verify_package.py --build-receipt /tmp/pr442-lean421-fresh.json
+	git diff --exit-code
 .PHONY: frontier596-verify
 frontier596-verify: selected-record-check
 	@work=$$(mktemp -d "$${TMPDIR:-/tmp}/integer-mult-frontier596.XXXXXX"); \