INDEPENDENT ENVIRONMENT/SOURCE AUDIT UTC started: 2026-09-05T22:38:20.492961+00:00 Collector: LEAN_PROJECT\verification\independent-audit-2026-09-05\collect_environment.py Collector SHA256: 79530984ceaf94ed10a06ce1e3a790704482497c55226a52939ca76fa4102a15 No Lean compilation or build is performed by this collector. Dependency source provenance is inspected separately from reused dependency build caches. Git comparisons below compare source checkouts to their own recorded HEAD; no dependency cache was rebuilt or authenticated as part of this collector. DEPENDENCY: plausible MANIFEST URL: https://github.com/leanprover-community/plausible MANIFEST REV: d9598f07b1bc701f1e3aae163d2681c1fd978793 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/plausible STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN d9598f07b1bc701f1e3aae163d2681c1fd978793 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/plausible STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\plausible" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\plausible", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "plausible", "manifest_rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "actual_head": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: LeanSearchClient MANIFEST URL: https://github.com/leanprover-community/LeanSearchClient MANIFEST REV: ba67e212be1197b84c1f1f6299488a10a3002713 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/LeanSearchClient STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN ba67e212be1197b84c1f1f6299488a10a3002713 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/LeanSearchClient STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\LeanSearchClient" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\LeanSearchClient", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "LeanSearchClient", "manifest_rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "actual_head": "ba67e212be1197b84c1f1f6299488a10a3002713", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: importGraph MANIFEST URL: https://github.com/leanprover-community/import-graph MANIFEST REV: 1681d78dd6e65e38b143f9740d829c826673807c COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/importGraph STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN 1681d78dd6e65e38b143f9740d829c826673807c STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/import-graph STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\importGraph" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\importGraph", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "importGraph", "manifest_rev": "1681d78dd6e65e38b143f9740d829c826673807c", "actual_head": "1681d78dd6e65e38b143f9740d829c826673807c", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: proofwidgets MANIFEST URL: https://github.com/leanprover-community/ProofWidgets4 MANIFEST REV: a8acbfd87375ff4abe14ce09db5b7664d383bc7f COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/proofwidgets STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN a8acbfd87375ff4abe14ce09db5b7664d383bc7f STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/ProofWidgets4 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\proofwidgets" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\proofwidgets", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "proofwidgets", "manifest_rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "actual_head": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: aesop MANIFEST URL: https://github.com/leanprover-community/aesop MANIFEST REV: 18889deb9e83ea7420ef51c160d6f88552e744e3 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/aesop STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN 18889deb9e83ea7420ef51c160d6f88552e744e3 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/aesop STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\aesop" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\aesop", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "aesop", "manifest_rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "actual_head": "18889deb9e83ea7420ef51c160d6f88552e744e3", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: Qq MANIFEST URL: https://github.com/leanprover-community/quote4 MANIFEST REV: 507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/Qq STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN 507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/quote4 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Qq" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Qq", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "Qq", "manifest_rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "actual_head": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: batteries MANIFEST URL: https://github.com/leanprover-community/batteries MANIFEST REV: 4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/batteries STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN 4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/batteries STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\batteries" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\batteries", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "batteries", "manifest_rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", "actual_head": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: Cli MANIFEST URL: https://github.com/leanprover/lean4-cli MANIFEST REV: ab3a82db9fea14cf0fd7f5a2de650f4b534640af COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/Cli STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN ab3a82db9fea14cf0fd7f5a2de650f4b534640af STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover/lean4-cli STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\Cli" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\Cli", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "Cli", "manifest_rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "actual_head": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } DEPENDENCY: mathlib MANIFEST URL: https://github.com/leanprover-community/mathlib4.git MANIFEST REV: 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" rev-parse --show-toplevel ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "rev-parse", "--show-toplevel"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN LEAN_PROJECT/.lake/packages/mathlib STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" rev-parse --verify HEAD ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "rev-parse", "--verify", "HEAD"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" remote get-url origin ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "remote", "get-url", "origin"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN https://github.com/leanprover-community/mathlib4.git STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" status --porcelain=v1 --untracked-files=all ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "status", "--porcelain=v1", "--untracked-files=all"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" diff --no-ext-diff --name-status HEAD -- ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "diff", "--no-ext-diff", "--name-status", "HEAD", "--"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" diff --no-ext-diff --name-only HEAD -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "diff", "--no-ext-diff", "--name-only", "HEAD", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" ls-files --others --exclude-standard -- *.lean ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "ls-files", "--others", "--exclude-standard", "--", "*.lean"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 COMMAND (Windows command-line syntax): "C:\Program Files\Git\cmd\git.exe" -C "LEAN_PROJECT\.lake\packages\mathlib" diff --no-ext-diff HEAD -- lakefile.lean lakefile.toml lean-toolchain lake-manifest.json ARGUMENTS (JSON): ["C:\\Program Files\\Git\\cmd\\git.exe", "-C", "LEAN_PROJECT\\.lake\\packages\\mathlib", "diff", "--no-ext-diff", "HEAD", "--", "lakefile.lean", "lakefile.toml", "lean-toolchain", "lake-manifest.json"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0 DEPENDENCY SUMMARY: { "name": "mathlib", "manifest_rev": "4cbb42e75a050e830b7cf0f2ae748d7644f59cf7", "actual_head": "4cbb42e75a050e830b7cf0f2ae748d7644f59cf7", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } ALL DEPENDENCY SUMMARIES: [ { "name": "plausible", "manifest_rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "actual_head": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "LeanSearchClient", "manifest_rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "actual_head": "ba67e212be1197b84c1f1f6299488a10a3002713", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "importGraph", "manifest_rev": "1681d78dd6e65e38b143f9740d829c826673807c", "actual_head": "1681d78dd6e65e38b143f9740d829c826673807c", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "proofwidgets", "manifest_rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "actual_head": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "aesop", "manifest_rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "actual_head": "18889deb9e83ea7420ef51c160d6f88552e744e3", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "Qq", "manifest_rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "actual_head": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "batteries", "manifest_rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", "actual_head": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "Cli", "manifest_rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "actual_head": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] }, { "name": "mathlib", "manifest_rev": "4cbb42e75a050e830b7cf0f2ae748d7644f59cf7", "actual_head": "4cbb42e75a050e830b7cf0f2ae748d7644f59cf7", "head_matches_pin": true, "own_git_repository": true, "status_nonempty": false, "status_exit_code": 0, "changed_tracked_lean_except_lakefile": [], "untracked_lean_except_lakefile": [], "source_check_exit_codes": [ 0, 0 ] } ] ARCHIVE COMPARISON (complete per-file SHA256 evidence follows): COMMAND (Windows command-line syntax): "USER_HOME\.cache\codex-runtimes\codex-primary-runtime\dependencies\python\python.exe" "LEAN_PROJECT\verification\independent-audit-2026-09-05\collect_environment.py" --archive-report ARGUMENTS (JSON): ["USER_HOME\\.cache\\codex-runtimes\\codex-primary-runtime\\dependencies\\python\\python.exe", "LEAN_PROJECT\\verification\\independent-audit-2026-09-05\\collect_environment.py", "--archive-report"] WORKING DIRECTORY: LEAN_PROJECT STDOUT BEGIN { "archive": "WORKSPACE\\output\\Complemented_Subspace_Lean_Verified.zip", "archive_bytes": 598251, "archive_sha256_before": "5fc920bc7bb22592c2170ac72447af563d17ef261e7f39dfd6123ba04b074148", "archive_sha256_after": "5fc920bc7bb22592c2170ac72447af563d17ef261e7f39dfd6123ba04b074148", "archive_unchanged_during_comparison": true, "zip_crc_bad_entry": null, "duplicate_archive_entries": [], "comparison_method": "SHA256 of complete decompressed ZIP entry bytes versus complete workspace file bytes; no normalization", "archive_file_count": 262, "source_or_config_count": 183, "source_or_config_matches": 183, "source_or_config_discrepancies": [], "internal_manifest_entry_count": 261, "internal_manifest_matches": 261, "internal_manifest_discrepancies": [], "archive_paths_not_covered_by_internal_manifest": [ "SOURCE-MANIFEST.sha256" ], "other_file_discrepancies": [ { "relative_path": "SOURCE-MANIFEST.sha256", "source_or_config": false, "archived_bytes": 27838, "archive_sha256": "c9311dda53584927098354931922a12d303fa9cceba4a218c270f868aad82828", "workspace_sha256": null, "status": "MISSING" } ], "workspace_extra_source_or_config_files": [ "AmbientLatticeBoundsAudit.lean", "BasisBoundsAudit.lean", "BasisBoundsCheck.lean", "ComplementedSubspace/ComplexCorollaryAudit.lean", "ComplementedSubspace/ComplexRealDPRAudit.lean", "ComplementedSubspace/FiniteHilbertWitnessAudit.lean", "ComplementedSubspace/FiniteOverlapScaleAudit.lean", "ComplementedSubspace/FiniteParameterAudit.lean", "ComplementedSubspace/LocalHilbertAudit.lean", "ComplementedSubspace/LocalHilbertDualTopAudit.lean", "ComplementedSubspace/LocalHilbertQuotientAudit.lean", "ComplementedSubspace/LocalHilbertRecursiveQuotient.lean", "ComplementedSubspace/ProductFrameTranspose.lean", "ComplementedSubspace/ProjectionAssemblyAudit.lean", "ComplementedSubspace/PureFrameDPRAudit.lean", "ComplementedSubspace/RealMainAudit.lean", "ComplementedSubspace/RealMainConsequencesAudit.lean", "ComplementedSubspace/RecursiveParametersAudit.lean", "ComplementedSubspace/SelectedFrameBasis.lean", "ComplexAmbientAudit.lean", "ComplexFrameRealificationAudit.lean", "ComplexProjectionAudit.lean", "ComplexRecursiveProjectionAudit.lean", "DPRtoGLAudit.lean", "FiniteDualDPRLowerAudit.lean", "FiniteHeadHilbertAudit.lean", "FiniteObstructionAudit.lean", "FiniteSelectedHilbertModelAudit.lean", "GLRetractionAudit.lean", "HilbertComplementAudit.lean", "HilbertOverlapAudit.lean", "LatticeApproximationAudit.lean", "LatticeNonisomorphismAudit.lean", "LocalHilbertEmbeddedRenormAudit.lean", "LocalUnconditionalAudit.lean", "LpUniformEquivAudit.lean", "NormalizedHilbertSynthesisAudit.lean", "ProjectionCorollariesAudit.lean", "ProjectionPerturbationAudit.lean", "RealConstructionAudit.lean", "RecursiveKernelHilbertAudit.lean", "SchauderDPRAudit.lean", "SelectedCoefficientHilbertAudit.lean", "SelectedFrameBasisAudit.lean", "SelectedHilbertReplacementAudit.lean", "SelectedProjectionSetupAudit.lean", "TensorMomentAudit.lean", "TrialAudit.lean", "experiments/unverified/ProjectionPerturbationDraft.lean", "experiments/unverified/ProjectionPerturbationDraftAudit.lean", "verification/independent-audit-2026-09-05/MainIdentity.lean", "verification/independent-audit-2026-09-05/PrintAxioms.lean", "verification/independent-audit-2026-09-05/PrintDefinitions.lean", "verification/independent-audit-2026-09-05/TraceDependencies.lean" ], "extra_scan_excluded_directories": [ ".lake", ".cache", ".git" ], "files": [ { "relative_path": "BUILDING.md", "source_or_config": false, "archived_bytes": 4890, "archive_sha256": "064a170f0b9e2c71f3390724173ef9ee900e23576681c9f733c6e22480295250", "workspace_sha256": "064a170f0b9e2c71f3390724173ef9ee900e23576681c9f733c6e22480295250", "status": "MATCH" }, { "relative_path": "BanLat/Basic.lean", "source_or_config": true, "archived_bytes": 24972, "archive_sha256": "30d3f545bce051b3621a881ae7c374d9d98b37bb14d20ed2ae339668f49dbfed", "workspace_sha256": "30d3f545bce051b3621a881ae7c374d9d98b37bb14d20ed2ae339668f49dbfed", "status": "MATCH" }, { "relative_path": "BanLat/Disjoint.lean", "source_or_config": true, "archived_bytes": 28251, "archive_sha256": "51e351f291a15a8d88d42f17f787dada806f5dccc6e39775173dbe3fde9d54dc", "workspace_sha256": "51e351f291a15a8d88d42f17f787dada806f5dccc6e39775173dbe3fde9d54dc", "status": "MATCH" }, { "relative_path": "BanLat/Dual.lean", "source_or_config": true, "archived_bytes": 22655, "archive_sha256": "9d2254f8c8dab409a223ffa01e7a66cf044278039c82f995c286ad2e38f65cd3", "workspace_sha256": "9d2254f8c8dab409a223ffa01e7a66cf044278039c82f995c286ad2e38f65cd3", "status": "MATCH" }, { "relative_path": "BanLat/LICENSE", "source_or_config": false, "archived_bytes": 11357, "archive_sha256": "b40930bbcf80744c86c46a12bc9da056641d722716c378f5659b9e555ef833e1", "workspace_sha256": "b40930bbcf80744c86c46a12bc9da056641d722716c378f5659b9e555ef833e1", "status": "MATCH" }, { "relative_path": "BanLat/LLexpr.lean", "source_or_config": true, "archived_bytes": 21813, "archive_sha256": "313cc63220e11d1b44a792d1cfa88990a63d90e000b82484bdc80165005d1a4d", "workspace_sha256": "313cc63220e11d1b44a792d1cfa88990a63d90e000b82484bdc80165005d1a4d", "status": "MATCH" }, { "relative_path": "BanLat/Normed.lean", "source_or_config": true, "archived_bytes": 22142, "archive_sha256": "50017cb69948b8e4059c65e502f1ec3f631ce7d92e5104343156e84f6aade33b", "workspace_sha256": "50017cb69948b8e4059c65e502f1ec3f631ce7d92e5104343156e84f6aade33b", "status": "MATCH" }, { "relative_path": "BanLat/Operators/Hom.lean", "source_or_config": true, "archived_bytes": 26230, "archive_sha256": "1a38127619695e2862fb93408bc24272d19a02f72a09783daf32e81b922e2595", "workspace_sha256": "1a38127619695e2862fb93408bc24272d19a02f72a09783daf32e81b922e2595", "status": "MATCH" }, { "relative_path": "BanLat/Operators/OrderBounded.lean", "source_or_config": true, "archived_bytes": 8627, "archive_sha256": "a563efcec03e343455826da46e359b819a39a0b0e53de85d17fb76a6579842d2", "workspace_sha256": "a563efcec03e343455826da46e359b819a39a0b0e53de85d17fb76a6579842d2", "status": "MATCH" }, { "relative_path": "BanLat/Operators/Positive.lean", "source_or_config": true, "archived_bytes": 14782, "archive_sha256": "ff39c2e000bdd315c914a68708d2fd3854a74accbe0ed5ec3901c331347dfe7d", "workspace_sha256": "ff39c2e000bdd315c914a68708d2fd3854a74accbe0ed5ec3901c331347dfe7d", "status": "MATCH" }, { "relative_path": "BanLat/Operators/Regular.lean", "source_or_config": true, "archived_bytes": 1044, "archive_sha256": "67f3f9dff27a45c5c3b914051a69c45b5af8c23efa1154ac33e8609af74828fb", "workspace_sha256": "67f3f9dff27a45c5c3b914051a69c45b5af8c23efa1154ac33e8609af74828fb", "status": "MATCH" }, { "relative_path": "BanLat/Operators/RieszKantorovich.lean", "source_or_config": true, "archived_bytes": 58201, "archive_sha256": "51846724ccfe2955e7ed2f584237c107e08356f2bdb2ec62ca5638090afab92b", "workspace_sha256": "51846724ccfe2955e7ed2f584237c107e08356f2bdb2ec62ca5638090afab92b", "status": "MATCH" }, { "relative_path": "BanLat/OrderComplete.lean", "source_or_config": true, "archived_bytes": 16988, "archive_sha256": "5e55e5876b0141ceeaa11d075b8048311eef9b5c2c314f8011e4c557f3696ff4", "workspace_sha256": "5e55e5876b0141ceeaa11d075b8048311eef9b5c2c314f8011e4c557f3696ff4", "status": "MATCH" }, { "relative_path": "BanLat/OrderUnit.lean", "source_or_config": true, "archived_bytes": 2472, "archive_sha256": "93ed97cca155d8bf0a69bed4cffe229e0cb9183a809d8088855f1ccf399fdd30", "workspace_sha256": "93ed97cca155d8bf0a69bed4cffe229e0cb9183a809d8088855f1ccf399fdd30", "status": "MATCH" }, { "relative_path": "BanLat/PORTING.md", "source_or_config": false, "archived_bytes": 1681, "archive_sha256": "f6595bab0897b486542f09eb20a4ed553e1578ad64fff6480512a4fff645f78e", "workspace_sha256": "f6595bab0897b486542f09eb20a4ed553e1578ad64fff6480512a4fff645f78e", "status": "MATCH" }, { "relative_path": "BanLat/RieszDec.lean", "source_or_config": true, "archived_bytes": 12491, "archive_sha256": "c6c50461b12c0243b9ebf8efef0a4ad8ffa44e85f0d99148e4257168921da5fa", "workspace_sha256": "c6c50461b12c0243b9ebf8efef0a4ad8ffa44e85f0d99148e4257168921da5fa", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/Basic.lean", "source_or_config": true, "archived_bytes": 7784, "archive_sha256": "d2b215633f9ab3b5327e8648fa0674a281f3598ad565260b2f5c02312f6b4231", "workspace_sha256": "d2b215633f9ab3b5327e8648fa0674a281f3598ad565260b2f5c02312f6b4231", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/DisjointComplement.lean", "source_or_config": true, "archived_bytes": 5600, "archive_sha256": "fb0087e729830d65c7f668a28cb9273abf7d39d52b39c07122096843c46ae1c9", "workspace_sha256": "fb0087e729830d65c7f668a28cb9273abf7d39d52b39c07122096843c46ae1c9", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/Generated.lean", "source_or_config": true, "archived_bytes": 20560, "archive_sha256": "6bad98d67759be2f88047dfaf9192864ce60bb7790e659eba1cd844ce152273d", "workspace_sha256": "6bad98d67759be2f88047dfaf9192864ce60bb7790e659eba1cd844ce152273d", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/Lattice.lean", "source_or_config": true, "archived_bytes": 4123, "archive_sha256": "8a9f48e31362404d21f04fc4a43ed10de79e08ec5f37cf890132ae7ac48d8290", "workspace_sha256": "8a9f48e31362404d21f04fc4a43ed10de79e08ec5f37cf890132ae7ac48d8290", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/PPP.lean", "source_or_config": true, "archived_bytes": 17832, "archive_sha256": "d7d5fa1abe3602a7d56333de5818d4c2c1aa232047e95b4bc756e63b78328779", "workspace_sha256": "d7d5fa1abe3602a7d56333de5818d4c2c1aa232047e95b4bc756e63b78328779", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Band/Projection.lean", "source_or_config": true, "archived_bytes": 51891, "archive_sha256": "5400e8d1efbbfda77ccc00e0f8a00e93030960f9325ac5541044686b58469127", "workspace_sha256": "5400e8d1efbbfda77ccc00e0f8a00e93030960f9325ac5541044686b58469127", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Ideal.lean", "source_or_config": true, "archived_bytes": 51545, "archive_sha256": "a2c95d09b57d04eb5ac12b20ae852d5e31ca35ed6437aefcccbc5a90bcd72c33", "workspace_sha256": "a2c95d09b57d04eb5ac12b20ae852d5e31ca35ed6437aefcccbc5a90bcd72c33", "status": "MATCH" }, { "relative_path": "BanLat/Substructures/Sublattice.lean", "source_or_config": true, "archived_bytes": 42813, "archive_sha256": "e2df596909a94e153be31e04957c4e218d2d763ceeb97a3fec016e18de8c3ea6", "workspace_sha256": "e2df596909a94e153be31e04957c4e218d2d763ceeb97a3fec016e18de8c3ea6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace.lean", "source_or_config": true, "archived_bytes": 3594, "archive_sha256": "542170589de08b05402d4f9e2570cd70169c5378efe5748ba3565352714ab7e1", "workspace_sha256": "542170589de08b05402d4f9e2570cd70169c5378efe5748ba3565352714ab7e1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ActualProjectionBidualDPR.lean", "source_or_config": true, "archived_bytes": 2155, "archive_sha256": "b131350879249514eb6eb47b46cdafdbc8ad1e465483f32047ebd86ef2e72c9c", "workspace_sha256": "b131350879249514eb6eb47b46cdafdbc8ad1e465483f32047ebd86ef2e72c9c", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ActualProjectionDPR.lean", "source_or_config": true, "archived_bytes": 2047, "archive_sha256": "a3385b8565d37f4e49491bbd8cfdc1bff2cb42c3ad530690ca3ca7ea0e4cbd85", "workspace_sha256": "a3385b8565d37f4e49491bbd8cfdc1bff2cb42c3ad530690ca3ca7ea0e4cbd85", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ActualProjectionDualDPR.lean", "source_or_config": true, "archived_bytes": 2151, "archive_sha256": "9f7b62844c96bf17bc6cf7be1b3798aff60c52a3cd533995aa285a39ec50c1f8", "workspace_sha256": "9f7b62844c96bf17bc6cf7be1b3798aff60c52a3cd533995aa285a39ec50c1f8", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/Ambient.lean", "source_or_config": true, "archived_bytes": 3741, "archive_sha256": "cf65a5aa2da2262f84695696283cda9f3b918215ce12fd777b2e0e70c355f347", "workspace_sha256": "cf65a5aa2da2262f84695696283cda9f3b918215ce12fd777b2e0e70c355f347", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientBasis.lean", "source_or_config": true, "archived_bytes": 7404, "archive_sha256": "c43668cfe5263a64c711faef86de4372206b6b84f37a66515d3e9a38d865db1d", "workspace_sha256": "c43668cfe5263a64c711faef86de4372206b6b84f37a66515d3e9a38d865db1d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientFiniteApproximation.lean", "source_or_config": true, "archived_bytes": 4822, "archive_sha256": "5f674f8cb28d0d1d36b8e720c19a947868605c04521122567b677747b3e6f209", "workspace_sha256": "5f674f8cb28d0d1d36b8e720c19a947868605c04521122567b677747b3e6f209", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientLattice.lean", "source_or_config": true, "archived_bytes": 4768, "archive_sha256": "15a495e3b9e2d0cc724f267b8818d9e718119fbeb43ccb374c46975a533ba2ab", "workspace_sha256": "15a495e3b9e2d0cc724f267b8818d9e718119fbeb43ccb374c46975a533ba2ab", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientProjection.lean", "source_or_config": true, "archived_bytes": 5257, "archive_sha256": "30fecdacb0b7f245923efc245bf369e56211664b1cdebe2d458e1346f8d16155", "workspace_sha256": "30fecdacb0b7f245923efc245bf369e56211664b1cdebe2d458e1346f8d16155", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientSchauder.lean", "source_or_config": true, "archived_bytes": 2139, "archive_sha256": "3879a418f8a2f6f6fde013b939695d88f46656b297ad4260d573178c53a123c3", "workspace_sha256": "3879a418f8a2f6f6fde013b939695d88f46656b297ad4260d573178c53a123c3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientSeparable.lean", "source_or_config": true, "archived_bytes": 1243, "archive_sha256": "50191618fbda12052d9eed73e99850acc880bbf74423d89589e725dc0ea8bd82", "workspace_sha256": "50191618fbda12052d9eed73e99850acc880bbf74423d89589e725dc0ea8bd82", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/AmbientUniformConvex.lean", "source_or_config": true, "archived_bytes": 1385, "archive_sha256": "bcf3ad915f3defb4ff941c898b02ba9ce0395c1332fc40eae8db59013c58381a", "workspace_sha256": "bcf3ad915f3defb4ff941c898b02ba9ce0395c1332fc40eae8db59013c58381a", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/BasisBounds.lean", "source_or_config": true, "archived_bytes": 5137, "archive_sha256": "c047aa5f7c27973de4a07f8b3146bead52603dbb6cca9c6894828d9ddeebcbce", "workspace_sha256": "c047aa5f7c27973de4a07f8b3146bead52603dbb6cca9c6894828d9ddeebcbce", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/BasisRestriction.lean", "source_or_config": true, "archived_bytes": 2658, "archive_sha256": "c8521ad7ba31f01bf0c0a7634e9b4c5f5a9a65de600ae216374628b5f4c710ca", "workspace_sha256": "c8521ad7ba31f01bf0c0a7634e9b4c5f5a9a65de600ae216374628b5f4c710ca", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/BasisTransport.lean", "source_or_config": true, "archived_bytes": 3202, "archive_sha256": "8a28498807724e83e59b714bfad51c191f405e4cadbc76bba54844bc378565a7", "workspace_sha256": "8a28498807724e83e59b714bfad51c191f405e4cadbc76bba54844bc378565a7", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexAmbient.lean", "source_or_config": true, "archived_bytes": 5379, "archive_sha256": "b4d53b895cfabb37bd96cdcd90ce3c5796fd0e977a91513c6c7051877cb36af7", "workspace_sha256": "b4d53b895cfabb37bd96cdcd90ce3c5796fd0e977a91513c6c7051877cb36af7", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexAmbientSchauder.lean", "source_or_config": true, "archived_bytes": 10939, "archive_sha256": "bb39557df190b8f970dcfc7a6b3ed58ca80fdb7957fc1b0906bcb8182965fcbe", "workspace_sha256": "bb39557df190b8f970dcfc7a6b3ed58ca80fdb7957fc1b0906bcb8182965fcbe", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexCorollary.lean", "source_or_config": true, "archived_bytes": 960, "archive_sha256": "ba3689e116cced5d2c40ca0823bcd549f9693929a19f1300c7c23d1a5aa71e88", "workspace_sha256": "ba3689e116cced5d2c40ca0823bcd549f9693929a19f1300c7c23d1a5aa71e88", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexCorollaryAssembly.lean", "source_or_config": true, "archived_bytes": 2312, "archive_sha256": "621ef045c17dc3c26dda85c241e2dd5846233f87ab4c6a2d4282cf2abc8f6462", "workspace_sha256": "621ef045c17dc3c26dda85c241e2dd5846233f87ab4c6a2d4282cf2abc8f6462", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexFrameCoefficient.lean", "source_or_config": true, "archived_bytes": 6937, "archive_sha256": "17c6880f4a3b6dbf03428338354ac759b362a7c00d871c49d3bc36f27d7d7866", "workspace_sha256": "17c6880f4a3b6dbf03428338354ac759b362a7c00d871c49d3bc36f27d7d7866", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexFrameCoefficientRange.lean", "source_or_config": true, "archived_bytes": 4660, "archive_sha256": "d7625763107dc031fc00531d701110197245a971ef85ed4d3e5cd86a970f7e26", "workspace_sha256": "d7625763107dc031fc00531d701110197245a971ef85ed4d3e5cd86a970f7e26", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexFrameProjection.lean", "source_or_config": true, "archived_bytes": 7225, "archive_sha256": "25d9d67bbebe6e0707772e05d0eeda01e40fc851de9b7e85092c5382a333050c", "workspace_sha256": "25d9d67bbebe6e0707772e05d0eeda01e40fc851de9b7e85092c5382a333050c", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexFrameRealification.lean", "source_or_config": true, "archived_bytes": 7561, "archive_sha256": "05bc816e8cd4090627918e60da48c497eb83511c03432f63320e21a7edbe973b", "workspace_sha256": "05bc816e8cd4090627918e60da48c497eb83511c03432f63320e21a7edbe973b", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexProjectionEnergy.lean", "source_or_config": true, "archived_bytes": 5654, "archive_sha256": "0580204035bc2ae8ede703d7988c58b485bc36e6fd635d97790bc0713e833ba3", "workspace_sha256": "0580204035bc2ae8ede703d7988c58b485bc36e6fd635d97790bc0713e833ba3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexProjectionRealEquiv.lean", "source_or_config": true, "archived_bytes": 5175, "archive_sha256": "16e855f4a09d8fd4efc8c52c412bcdf183468fc1d9d8b5312f41d4bc812b7948", "workspace_sha256": "16e855f4a09d8fd4efc8c52c412bcdf183468fc1d9d8b5312f41d4bc812b7948", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexRealDPR.lean", "source_or_config": true, "archived_bytes": 8697, "archive_sha256": "e7f51b27f5ad9812cc3fe10d01eebf85c6f1220529f7531b8256846bc649414e", "workspace_sha256": "e7f51b27f5ad9812cc3fe10d01eebf85c6f1220529f7531b8256846bc649414e", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexRecursiveProjection.lean", "source_or_config": true, "archived_bytes": 5314, "archive_sha256": "e0aa95ebd0f414be5c305d4930327c9460d10d75ec4e4d4b4ecff4f39b1a1e97", "workspace_sha256": "e0aa95ebd0f414be5c305d4930327c9460d10d75ec4e4d4b4ecff4f39b1a1e97", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexReindexedFrameProjection.lean", "source_or_config": true, "archived_bytes": 3906, "archive_sha256": "b4830bda1298b214d2bf817c40466ac6fd92cce1c53933e1623374d84b42699a", "workspace_sha256": "b4830bda1298b214d2bf817c40466ac6fd92cce1c53933e1623374d84b42699a", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ComplexTensorProjection.lean", "source_or_config": true, "archived_bytes": 8573, "archive_sha256": "50888e94422317ee745edb59b251a5268ab3bbb443eb8caf0b9c81c51388eeb6", "workspace_sha256": "50888e94422317ee745edb59b251a5268ab3bbb443eb8caf0b9c81c51388eeb6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/CorollaryStatement.lean", "source_or_config": true, "archived_bytes": 5279, "archive_sha256": "b8dd0e1b53e1da5078218af1bc03093dc7c44d618cdc3f3bc068eaa02598bf2a", "workspace_sha256": "b8dd0e1b53e1da5078218af1bc03093dc7c44d618cdc3f3bc068eaa02598bf2a", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DPRIsomorphism.lean", "source_or_config": true, "archived_bytes": 3376, "archive_sha256": "f2c1cd77e22f742ef21465dd646a440e3cc49ac2d52985d82e79d3f3e0f3df4d", "workspace_sha256": "f2c1cd77e22f742ef21465dd646a440e3cc49ac2d52985d82e79d3f3e0f3df4d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DPRObstruction.lean", "source_or_config": true, "archived_bytes": 2149, "archive_sha256": "0bfd5269c89cf507ce09dec97a573d364b426c636dd2068d9f1494c84cf3e140", "workspace_sha256": "0bfd5269c89cf507ce09dec97a573d364b426c636dd2068d9f1494c84cf3e140", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DPRPredicates.lean", "source_or_config": true, "archived_bytes": 462, "archive_sha256": "47d7940cc1fb78fff4cacdefe7faf2abe1b1af72566cf7f6aa57ddad4e7abdb1", "workspace_sha256": "47d7940cc1fb78fff4cacdefe7faf2abe1b1af72566cf7f6aa57ddad4e7abdb1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DPRtoGL.lean", "source_or_config": true, "archived_bytes": 9304, "archive_sha256": "fd61437d513847bfe98421764fe725bc8096d8cf0ca04a64c91d0dbb39b4305a", "workspace_sha256": "fd61437d513847bfe98421764fe725bc8096d8cf0ca04a64c91d0dbb39b4305a", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DenseContractions.lean", "source_or_config": true, "archived_bytes": 1211, "archive_sha256": "6317ffc9b98877a90d9b3bf21a9adaeb82ca5d8827865d89ff43efb0632d10ed", "workspace_sha256": "6317ffc9b98877a90d9b3bf21a9adaeb82ca5d8827865d89ff43efb0632d10ed", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DenseContractionsScalar.lean", "source_or_config": true, "archived_bytes": 1266, "archive_sha256": "44689723e948fb2a5cbfcd99f62e2b1c706388646104cdea81182353aefd6cb6", "workspace_sha256": "44689723e948fb2a5cbfcd99f62e2b1c706388646104cdea81182353aefd6cb6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DiagonalFrameProduct.lean", "source_or_config": true, "archived_bytes": 2060, "archive_sha256": "aeaccf496f84a3b414561604cbbb2982c296b97ae21d46d47aee2f4a60e808ea", "workspace_sha256": "aeaccf496f84a3b414561604cbbb2982c296b97ae21d46d47aee2f4a60e808ea", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/DiagonalFrameSummand.lean", "source_or_config": true, "archived_bytes": 4293, "archive_sha256": "8fc4567967139882a6fb87e30485765b3a93178a5d810a45615078b0e238ae0b", "workspace_sha256": "8fc4567967139882a6fb87e30485765b3a93178a5d810a45615078b0e238ae0b", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteApproximation.lean", "source_or_config": true, "archived_bytes": 7342, "archive_sha256": "6c8c0840aa83c40b24423d1f8b2ba0978cdf526d4b13196d00f7d710d36a81de", "workspace_sha256": "6c8c0840aa83c40b24423d1f8b2ba0978cdf526d4b13196d00f7d710d36a81de", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteBasisTraceBound.lean", "source_or_config": true, "archived_bytes": 5104, "archive_sha256": "2947c81b8f0d42034fbd75562c3c83cb0b771564ef098433ab7d39e556b3913c", "workspace_sha256": "2947c81b8f0d42034fbd75562c3c83cb0b771564ef098433ab7d39e556b3913c", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteBidual.lean", "source_or_config": true, "archived_bytes": 2205, "archive_sha256": "4c748407a3541edd5c6b288ddac4ebd5f9f11b1953b811bb06bda183c00af45e", "workspace_sha256": "4c748407a3541edd5c6b288ddac4ebd5f9f11b1953b811bb06bda183c00af45e", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteBidualDPRLower.lean", "source_or_config": true, "archived_bytes": 1577, "archive_sha256": "bcb31f688538327f3782ef71ed2efebb1b852ffeed7ffbfefc2ffe71d041c022", "workspace_sha256": "bcb31f688538327f3782ef71ed2efebb1b852ffeed7ffbfefc2ffe71d041c022", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteBlockDPRLower.lean", "source_or_config": true, "archived_bytes": 2958, "archive_sha256": "c20708a337c386fb120a3a35a3190ccec5f5ecddaf17ad08e16f60aa966c76f1", "workspace_sha256": "c20708a337c386fb120a3a35a3190ccec5f5ecddaf17ad08e16f60aa966c76f1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteBlockObstruction.lean", "source_or_config": true, "archived_bytes": 5139, "archive_sha256": "a8a14d7ee79cfcef0eef1e8b7dd090765b2c695e6a2c34ff257985ff24841abc", "workspace_sha256": "a8a14d7ee79cfcef0eef1e8b7dd090765b2c695e6a2c34ff257985ff24841abc", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteCoordinateSelection.lean", "source_or_config": true, "archived_bytes": 4395, "archive_sha256": "58ddbd8fd95a378b40badde0fd4ceb1dab4a6be8fea7265f5137f35188eb4378", "workspace_sha256": "58ddbd8fd95a378b40badde0fd4ceb1dab4a6be8fea7265f5137f35188eb4378", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteCorrection.lean", "source_or_config": true, "archived_bytes": 5540, "archive_sha256": "94742aea3304bd769f6b552e1ca0416d3328cdd6ee6e274031722159aec2f813", "workspace_sha256": "94742aea3304bd769f6b552e1ca0416d3328cdd6ee6e274031722159aec2f813", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteCubeBound.lean", "source_or_config": true, "archived_bytes": 2347, "archive_sha256": "5c2f69a2ec8729c8cc571d1a94a3a0f626cb06c0e6fb9d413158eadb5463c8a6", "workspace_sha256": "5c2f69a2ec8729c8cc571d1a94a3a0f626cb06c0e6fb9d413158eadb5463c8a6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteDualBasis.lean", "source_or_config": true, "archived_bytes": 2385, "archive_sha256": "eb484185924f9d14a10afef2d70862873585ddc14b28a1b5456a9f95dc320398", "workspace_sha256": "eb484185924f9d14a10afef2d70862873585ddc14b28a1b5456a9f95dc320398", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteDualDPRLower.lean", "source_or_config": true, "archived_bytes": 3343, "archive_sha256": "6e4f469b111c39ae14b273169e93510c2dc9a67da34ec4a5932234ccf533bfe6", "workspace_sha256": "6e4f469b111c39ae14b273169e93510c2dc9a67da34ec4a5932234ccf533bfe6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteDualSuperspace.lean", "source_or_config": true, "archived_bytes": 2366, "archive_sha256": "7e7a9c409ffe5d6d71a3159626dfce2368b08a1061ba7c6ade5b2edd11845467", "workspace_sha256": "7e7a9c409ffe5d6d71a3159626dfce2368b08a1061ba7c6ade5b2edd11845467", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteFrame.lean", "source_or_config": true, "archived_bytes": 2504, "archive_sha256": "379b3135d2ab8675e3b9240a3fd1cb6c8de424f4f67ac7d0c301ea55d5b93725", "workspace_sha256": "379b3135d2ab8675e3b9240a3fd1cb6c8de424f4f67ac7d0c301ea55d5b93725", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteHeadHilbert.lean", "source_or_config": true, "archived_bytes": 5895, "archive_sha256": "32bff88599b6fc6671342176eb0c2ab1e5adb33a8762e1e49a97d9c0bc0a9cfb", "workspace_sha256": "32bff88599b6fc6671342176eb0c2ab1e5adb33a8762e1e49a97d9c0bc0a9cfb", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteHilbertAverage.lean", "source_or_config": true, "archived_bytes": 2986, "archive_sha256": "6fc8cfe97b6aeedeb36e64a835ab3040fc2b1430ea8be166169edbe9147ef531", "workspace_sha256": "6fc8cfe97b6aeedeb36e64a835ab3040fc2b1430ea8be166169edbe9147ef531", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteLpGeometry.lean", "source_or_config": true, "archived_bytes": 10468, "archive_sha256": "d3504078f5ad9966735841a01a97e509566673abc9b8842606ede7e763a6a309", "workspace_sha256": "d3504078f5ad9966735841a01a97e509566673abc9b8842606ede7e763a6a309", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapBasisColumns.lean", "source_or_config": true, "archived_bytes": 5180, "archive_sha256": "23b4e1a891e849f4b178b0fb07b43adf75c3fb9f24a7792fb85db4c48ab89fd8", "workspace_sha256": "23b4e1a891e849f4b178b0fb07b43adf75c3fb9f24a7792fb85db4c48ab89fd8", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapBound.lean", "source_or_config": true, "archived_bytes": 4152, "archive_sha256": "0f11567d750cb9c3f5d2802bc6a29b72ceb85611d13a1340689aebe55477027a", "workspace_sha256": "0f11567d750cb9c3f5d2802bc6a29b72ceb85611d13a1340689aebe55477027a", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapConclusion.lean", "source_or_config": true, "archived_bytes": 2154, "archive_sha256": "98236aa39ec4de97587f365a4eaa857c9cef06f0857625189de8885406c33a40", "workspace_sha256": "98236aa39ec4de97587f365a4eaa857c9cef06f0857625189de8885406c33a40", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapDualScale.lean", "source_or_config": true, "archived_bytes": 1574, "archive_sha256": "879da90d3515e12c823da4647517bab6542316b316dde4daacf0edde27f8e380", "workspace_sha256": "879da90d3515e12c823da4647517bab6542316b316dde4daacf0edde27f8e380", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapGoodSecond.lean", "source_or_config": true, "archived_bytes": 6484, "archive_sha256": "f9cfd7b0d164e73f5e1de02ce03003087054b9b70c62238cbd7b69eff22df402", "workspace_sha256": "f9cfd7b0d164e73f5e1de02ce03003087054b9b70c62238cbd7b69eff22df402", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapLp.lean", "source_or_config": true, "archived_bytes": 5524, "archive_sha256": "a816942918033a1d448fa102dd168c65a0dab68fc7645cd4d83899a438638af4", "workspace_sha256": "a816942918033a1d448fa102dd168c65a0dab68fc7645cd4d83899a438638af4", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapMatrixNorms.lean", "source_or_config": true, "archived_bytes": 4181, "archive_sha256": "6d6bafa7eb67b68309f4817542bf625334bb6c22667dba964c0350dd5bc0fed0", "workspace_sha256": "6d6bafa7eb67b68309f4817542bf625334bb6c22667dba964c0350dd5bc0fed0", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapMoments.lean", "source_or_config": true, "archived_bytes": 3682, "archive_sha256": "b153ccc3a4e51b5f8689b02aaeeb9828fba6ac59f29a30f27936b4fd621f5b26", "workspace_sha256": "b153ccc3a4e51b5f8689b02aaeeb9828fba6ac59f29a30f27936b4fd621f5b26", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapObstruction.lean", "source_or_config": true, "archived_bytes": 7976, "archive_sha256": "5c1c86fc03e56139cbaf6f5cafa764b07bf1c534938153ad8bb7241c19d96c07", "workspace_sha256": "5c1c86fc03e56139cbaf6f5cafa764b07bf1c534938153ad8bb7241c19d96c07", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapRandomization.lean", "source_or_config": true, "archived_bytes": 5861, "archive_sha256": "2b19be87a99d4b1ac528c80cf9beb8a40072cdf116d647d406cd4b5d9126409f", "workspace_sha256": "2b19be87a99d4b1ac528c80cf9beb8a40072cdf116d647d406cd4b5d9126409f", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapScale.lean", "source_or_config": true, "archived_bytes": 12773, "archive_sha256": "a60c1c2c544051b57cdc3a55652f26b0b38f1fc213cf859708408b32b6c78769", "workspace_sha256": "a60c1c2c544051b57cdc3a55652f26b0b38f1fc213cf859708408b32b6c78769", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteOverlapUpper.lean", "source_or_config": true, "archived_bytes": 9043, "archive_sha256": "6f51f4cbf868e4e3bf26a13fb8a0557086fbdbe92baa692e850fd75dd75ec3e7", "workspace_sha256": "6f51f4cbf868e4e3bf26a13fb8a0557086fbdbe92baa692e850fd75dd75ec3e7", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteParameterBounds.lean", "source_or_config": true, "archived_bytes": 5383, "archive_sha256": "c28ac1eead96655022591993083ffa1a55e8b3ae8ecc5331afeb83ba265e5692", "workspace_sha256": "c28ac1eead96655022591993083ffa1a55e8b3ae8ecc5331afeb83ba265e5692", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteParameterGap.lean", "source_or_config": true, "archived_bytes": 11369, "archive_sha256": "3eb14759310d2d9d44a5fc3cad4f3c34ad1defc50deb787d7a397bf4eabb8dc1", "workspace_sha256": "3eb14759310d2d9d44a5fc3cad4f3c34ad1defc50deb787d7a397bf4eabb8dc1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteProductObstruction.lean", "source_or_config": true, "archived_bytes": 1842, "archive_sha256": "efe6e44207e493b4a4f96256d8ba6b649acb308acf839d56dbf958bc4f209276", "workspace_sha256": "efe6e44207e493b4a4f96256d8ba6b649acb308acf839d56dbf958bc4f209276", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteProjectionTrace.lean", "source_or_config": true, "archived_bytes": 9057, "archive_sha256": "2809bca2d08a5a4497b447116651a83fc894eff2c8d365d5ffa7b4f686d1ac4f", "workspace_sha256": "2809bca2d08a5a4497b447116651a83fc894eff2c8d365d5ffa7b4f686d1ac4f", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSelectedHilbertModel.lean", "source_or_config": true, "archived_bytes": 5423, "archive_sha256": "bf66a07267b955e5f27e7044957b9a2f7e7271a0acd1d783c545618a2466f9c3", "workspace_sha256": "bf66a07267b955e5f27e7044957b9a2f7e7271a0acd1d783c545618a2466f9c3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSelectionCoordinates.lean", "source_or_config": true, "archived_bytes": 4137, "archive_sha256": "5e92e926e345daec8931dab8ac21c8ed37ab8d1ba50cd6034b0f3042fbd57245", "workspace_sha256": "5e92e926e345daec8931dab8ac21c8ed37ab8d1ba50cd6034b0f3042fbd57245", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSigns.lean", "source_or_config": true, "archived_bytes": 10082, "archive_sha256": "5e5d5c44960df9c65ef60d3b8575cc62cd9b3a984473e0579cd23512862b515d", "workspace_sha256": "5e5d5c44960df9c65ef60d3b8575cc62cd9b3a984473e0579cd23512862b515d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSignsComplex.lean", "source_or_config": true, "archived_bytes": 2418, "archive_sha256": "a921891bdb41b6dd57c95947b4e53886ca57a0ab4b9ba2c3798fec8b59baf7b2", "workspace_sha256": "a921891bdb41b6dd57c95947b4e53886ca57a0ab4b9ba2c3798fec8b59baf7b2", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSignsInterpolation.lean", "source_or_config": true, "archived_bytes": 5593, "archive_sha256": "11629847ce860774366c41c37883126d52c02e4a0e2668a2ed26a5cd464598d0", "workspace_sha256": "11629847ce860774366c41c37883126d52c02e4a0e2668a2ed26a5cd464598d0", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteSuperspaceSplitting.lean", "source_or_config": true, "archived_bytes": 3008, "archive_sha256": "4156ce51dbb60a5270821b30de9c66aab560fb026105fa99e796d9d20112f340", "workspace_sha256": "4156ce51dbb60a5270821b30de9c66aab560fb026105fa99e796d9d20112f340", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteTraceOverlap.lean", "source_or_config": true, "archived_bytes": 6291, "archive_sha256": "157741f05ccc26cb8733884edfe8f7a027225bd126c1a5df93a8fa2514647c15", "workspace_sha256": "157741f05ccc26cb8733884edfe8f7a027225bd126c1a5df93a8fa2514647c15", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FiniteTraceSelection.lean", "source_or_config": true, "archived_bytes": 3126, "archive_sha256": "8654e1c06f1e452acdceaf2dfc57a6711156515bd73d548b2dfa1e185ddb5e70", "workspace_sha256": "8654e1c06f1e452acdceaf2dfc57a6711156515bd73d548b2dfa1e185ddb5e70", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameCoefficient.lean", "source_or_config": true, "archived_bytes": 4085, "archive_sha256": "70ca3d68efc108d054db4f2bba99a3d53f9184cf8bb0b57abacc7b8046163d46", "workspace_sha256": "70ca3d68efc108d054db4f2bba99a3d53f9184cf8bb0b57abacc7b8046163d46", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameCoefficientHilbert.lean", "source_or_config": true, "archived_bytes": 4152, "archive_sha256": "25beaa201d06a38d2ee2f36a2ea9232e3f6843a9146589f356cdb78cb387a330", "workspace_sha256": "25beaa201d06a38d2ee2f36a2ea9232e3f6843a9146589f356cdb78cb387a330", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameCoefficientNorm.lean", "source_or_config": true, "archived_bytes": 2357, "archive_sha256": "25f6b0cd76a139583221fc2110a08dff83ecb137d640fb1b086ddb3d840d7b39", "workspace_sha256": "25f6b0cd76a139583221fc2110a08dff83ecb137d640fb1b086ddb3d840d7b39", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameCoefficientRange.lean", "source_or_config": true, "archived_bytes": 2042, "archive_sha256": "a0b417aa6b29cd50ece756e906c750305221ff100c37a4ca84cb5059926b38c4", "workspace_sha256": "a0b417aa6b29cd50ece756e906c750305221ff100c37a4ca84cb5059926b38c4", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameCoefficientReindexedRange.lean", "source_or_config": true, "archived_bytes": 2538, "archive_sha256": "66aa1ab2eeda8cb80adce4cc9999432780b1382be1c9217da3608c419a3dc87d", "workspace_sha256": "66aa1ab2eeda8cb80adce4cc9999432780b1382be1c9217da3608c419a3dc87d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameProjectionNorm.lean", "source_or_config": true, "archived_bytes": 9891, "archive_sha256": "c99edfd191546d4bc79d93f38a69df1db9abbb5abc0c145c044fc60a977a4450", "workspace_sha256": "c99edfd191546d4bc79d93f38a69df1db9abbb5abc0c145c044fc60a977a4450", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/FrameProjectionRange.lean", "source_or_config": true, "archived_bytes": 4681, "archive_sha256": "328058fd2da0542b217b62d7f993ab32596eda6db83b7f56d04dda601d919c03", "workspace_sha256": "328058fd2da0542b217b62d7f993ab32596eda6db83b7f56d04dda601d919c03", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/GLDualRetraction.lean", "source_or_config": true, "archived_bytes": 4323, "archive_sha256": "1b86a0368a10ba5859e478280e5535063ddcbf2a0ea7fdc276fe9d16e209f83d", "workspace_sha256": "1b86a0368a10ba5859e478280e5535063ddcbf2a0ea7fdc276fe9d16e209f83d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/GLRetraction.lean", "source_or_config": true, "archived_bytes": 9551, "archive_sha256": "73b7e706f0223634c3aac87d8c9d8bd4127206fde355d047f58490b537bb36d3", "workspace_sha256": "73b7e706f0223634c3aac87d8c9d8bd4127206fde355d047f58490b537bb36d3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/HilbertComplement.lean", "source_or_config": true, "archived_bytes": 4882, "archive_sha256": "cd6dae85d346023abee70c67bd72b30bc1226d227433f2e01d307d1724f10dc5", "workspace_sha256": "cd6dae85d346023abee70c67bd72b30bc1226d227433f2e01d307d1724f10dc5", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/HilbertOverlap.lean", "source_or_config": true, "archived_bytes": 11058, "archive_sha256": "25f47937d625f6b360dbbf0ff9eb6a33372aa39a56caae8cc4ef261fbf162bf1", "workspace_sha256": "25f47937d625f6b360dbbf0ff9eb6a33372aa39a56caae8cc4ef261fbf162bf1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/HilbertTraceTransfer.lean", "source_or_config": true, "archived_bytes": 1569, "archive_sha256": "e5f209811f9eff3ee3f3ecacccb0e77abed6dc30ff31c2411a5bea15d16b2423", "workspace_sha256": "e5f209811f9eff3ee3f3ecacccb0e77abed6dc30ff31c2411a5bea15d16b2423", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/InfiniteFrameObstruction.lean", "source_or_config": true, "archived_bytes": 1945, "archive_sha256": "0acddd6eb16a34d8346a5f0cacb9df65da66481c1d5a5e7e0511f289a1b7a9bd", "workspace_sha256": "0acddd6eb16a34d8346a5f0cacb9df65da66481c1d5a5e7e0511f289a1b7a9bd", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/IsometricProductDPRLower.lean", "source_or_config": true, "archived_bytes": 3320, "archive_sha256": "0488f204843bfdca70793d677b2dcc4884ffe41a60339ee637d0d000449db6f9", "workspace_sha256": "0488f204843bfdca70793d677b2dcc4884ffe41a60339ee637d0d000449db6f9", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/IsometricProductSplitting.lean", "source_or_config": true, "archived_bytes": 3332, "archive_sha256": "f2572af0e42e05ec5e9cc86ea70adffe937b050e09f50a7a17572d64c9b6c1b6", "workspace_sha256": "f2572af0e42e05ec5e9cc86ea70adffe937b050e09f50a7a17572d64c9b6c1b6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LatticeApproximation.lean", "source_or_config": true, "archived_bytes": 2261, "archive_sha256": "ac38f607840630954fca0dcaac3301940bffaf4f6285e1a0bc03aacf7b0ea336", "workspace_sha256": "ac38f607840630954fca0dcaac3301940bffaf4f6285e1a0bc03aacf7b0ea336", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LatticeBasis.lean", "source_or_config": true, "archived_bytes": 3908, "archive_sha256": "37e06710226e0d05f30d653bc265042f639aa45218fc603f316196a2482307c6", "workspace_sha256": "37e06710226e0d05f30d653bc265042f639aa45218fc603f316196a2482307c6", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LatticeNonisomorphism.lean", "source_or_config": true, "archived_bytes": 1860, "archive_sha256": "81762cd605274f44c248531445c850c7f27e7b78e1c88e5e9f073674ddd84731", "workspace_sha256": "81762cd605274f44c248531445c850c7f27e7b78e1c88e5e9f073674ddd84731", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LatticeSpectral.lean", "source_or_config": true, "archived_bytes": 18057, "archive_sha256": "55ec903b3a24186808f817d0e32d920cff93c24bb85e046e3a225195c2be64cd", "workspace_sha256": "55ec903b3a24186808f817d0e32d920cff93c24bb85e046e3a225195c2be64cd", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbert.lean", "source_or_config": true, "archived_bytes": 9259, "archive_sha256": "16c8f562a11de1e24c58690321777ecb91429a9a9073c154ee1ea653a98da085", "workspace_sha256": "16c8f562a11de1e24c58690321777ecb91429a9a9073c154ee1ea653a98da085", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertCompactness.lean", "source_or_config": true, "archived_bytes": 12650, "archive_sha256": "64f421fe7ef04fd95dece8ad2c9b3f63b723f22bd7e60c11891c5e8b7d20fc3e", "workspace_sha256": "64f421fe7ef04fd95dece8ad2c9b3f63b723f22bd7e60c11891c5e8b7d20fc3e", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertCoordinates.lean", "source_or_config": true, "archived_bytes": 5735, "archive_sha256": "cb6da170830cb2c51267d2d0ae29f6bbf43893b66e82950a16918a374f0bdd1e", "workspace_sha256": "cb6da170830cb2c51267d2d0ae29f6bbf43893b66e82950a16918a374f0bdd1e", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertDual.lean", "source_or_config": true, "archived_bytes": 6424, "archive_sha256": "be507a3181bc331ee337e22b69ed0a5166a0dd78b528cf22ffd4b852238f941f", "workspace_sha256": "be507a3181bc331ee337e22b69ed0a5166a0dd78b528cf22ffd4b852238f941f", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertDualTop.lean", "source_or_config": true, "archived_bytes": 1098, "archive_sha256": "fce82710e2ec9c4ff98b920aee9194156ff35878f378ba0ac55546e6ac452dc0", "workspace_sha256": "fce82710e2ec9c4ff98b920aee9194156ff35878f378ba0ac55546e6ac452dc0", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertEmbeddedRenorm.lean", "source_or_config": true, "archived_bytes": 3466, "archive_sha256": "873d9a7c348c34ccee16fe66300f55eeb76c0dafaa6a57e017186e649f639188", "workspace_sha256": "873d9a7c348c34ccee16fe66300f55eeb76c0dafaa6a57e017186e649f639188", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertFactorization.lean", "source_or_config": true, "archived_bytes": 4662, "archive_sha256": "006bbe89c5d7df3fda5b2385bf04806665aa2ec47ef5e372acfa2d9a59afeda3", "workspace_sha256": "006bbe89c5d7df3fda5b2385bf04806665aa2ec47ef5e372acfa2d9a59afeda3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertHeadRenorm.lean", "source_or_config": true, "archived_bytes": 6264, "archive_sha256": "833de74e88964c3d46da39d56487db4a15409f4f59db50a0d5708613b3724363", "workspace_sha256": "833de74e88964c3d46da39d56487db4a15409f4f59db50a0d5708613b3724363", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertProjection.lean", "source_or_config": true, "archived_bytes": 6489, "archive_sha256": "5a19771c61d2c83bc171c19c24d36128b40a9c50b1792e00162de9f2cf7d6425", "workspace_sha256": "5a19771c61d2c83bc171c19c24d36128b40a9c50b1792e00162de9f2cf7d6425", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertProperty.lean", "source_or_config": true, "archived_bytes": 1158, "archive_sha256": "b228acf4ebc9580be43a0a87a1cc1e27fc05431c5218fa7f39be2cb9207c8925", "workspace_sha256": "b228acf4ebc9580be43a0a87a1cc1e27fc05431c5218fa7f39be2cb9207c8925", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertQuotient.lean", "source_or_config": true, "archived_bytes": 8115, "archive_sha256": "98ed8ff7cd6228438d765be36d58b0a4d368a4e3f8819adc39f288682d4ea482", "workspace_sha256": "98ed8ff7cd6228438d765be36d58b0a4d368a4e3f8819adc39f288682d4ea482", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertRecursiveKernelDual.lean", "source_or_config": true, "archived_bytes": 3698, "archive_sha256": "f1d73206e02676f82e59f1c0c2607a19e44717b2c35176720f0274edf3809146", "workspace_sha256": "f1d73206e02676f82e59f1c0c2607a19e44717b2c35176720f0274edf3809146", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertSum.lean", "source_or_config": true, "archived_bytes": 9350, "archive_sha256": "33f2c71af9bef3545221e68053477588799f922de43ea930f75971e1e5e5644d", "workspace_sha256": "33f2c71af9bef3545221e68053477588799f922de43ea930f75971e1e5e5644d", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertSumDual.lean", "source_or_config": true, "archived_bytes": 13593, "archive_sha256": "b8b9d994b5981c951b5e3bbd3b70694df36e50ec0eafefa826243ecc29ac49c4", "workspace_sha256": "b8b9d994b5981c951b5e3bbd3b70694df36e50ec0eafefa826243ecc29ac49c4", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalHilbertTransport.lean", "source_or_config": true, "archived_bytes": 2029, "archive_sha256": "35c6df1f513e10dabd05d102af49c089ec34445648d65d8142f9d26a7828e592", "workspace_sha256": "35c6df1f513e10dabd05d102af49c089ec34445648d65d8142f9d26a7828e592", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LocalUnconditional.lean", "source_or_config": true, "archived_bytes": 16438, "archive_sha256": "3ca23f64e18fcc14e9ee4a2a535acb40305acd9edc2862b6101f897f7bb14857", "workspace_sha256": "3ca23f64e18fcc14e9ee4a2a535acb40305acd9edc2862b6101f897f7bb14857", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpHeadTail.lean", "source_or_config": true, "archived_bytes": 6528, "archive_sha256": "1845df35a6a98c0611213c4c6e8dc3ec5c09061a7123556ff25e9b2e0edcaa44", "workspace_sha256": "1845df35a6a98c0611213c4c6e8dc3ec5c09061a7123556ff25e9b2e0edcaa44", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpSubmodule.lean", "source_or_config": true, "archived_bytes": 6988, "archive_sha256": "a776dfab72af942512150da9c0db55db30ac05c9ed6e940d21f98660ddbe1b34", "workspace_sha256": "a776dfab72af942512150da9c0db55db30ac05c9ed6e940d21f98660ddbe1b34", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpSubmoduleScalar.lean", "source_or_config": true, "archived_bytes": 2546, "archive_sha256": "a5ad7b44fa3d31b2caf86cfe1df7980799e2428e3dcb13696412e3a0e9d431a5", "workspace_sha256": "a5ad7b44fa3d31b2caf86cfe1df7980799e2428e3dcb13696412e3a0e9d431a5", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpTwoParallelogram.lean", "source_or_config": true, "archived_bytes": 3610, "archive_sha256": "3e4804fee62e5dd9a4628f3e322b3b40a946f721fa83951b587ae713eaba937c", "workspace_sha256": "3e4804fee62e5dd9a4628f3e322b3b40a946f721fa83951b587ae713eaba937c", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpTwoUniformConvex.lean", "source_or_config": true, "archived_bytes": 8910, "archive_sha256": "5da989db4b1fff92a3526515308d09e7f9aacff96ef5842a558e3db6d9327d64", "workspace_sha256": "5da989db4b1fff92a3526515308d09e7f9aacff96ef5842a558e3db6d9327d64", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/LpUniformEquiv.lean", "source_or_config": true, "archived_bytes": 3750, "archive_sha256": "f219d389f0edfbb905126735b2bd90fd8083a5cf7ed17aa785ad53308a5cb465", "workspace_sha256": "f219d389f0edfbb905126735b2bd90fd8083a5cf7ed17aa785ad53308a5cb465", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/NormSqSplitting.lean", "source_or_config": true, "archived_bytes": 3143, "archive_sha256": "aea063fb3a4feac48ca51eb9f2e5234221032d21a2a67f459f495a96233211f3", "workspace_sha256": "aea063fb3a4feac48ca51eb9f2e5234221032d21a2a67f459f495a96233211f3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/NormalizedHilbertSynthesis.lean", "source_or_config": true, "archived_bytes": 7864, "archive_sha256": "f0f5be10a561733c77c8a4c54f2f2954fdd154f10d0ab31b51c1688efbca0116", "workspace_sha256": "f0f5be10a561733c77c8a4c54f2f2954fdd154f10d0ab31b51c1688efbca0116", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/Parameters.lean", "source_or_config": true, "archived_bytes": 2633, "archive_sha256": "378a293532f31438920433805add44964399da5d0b8237cf562237ea3044d8d9", "workspace_sha256": "378a293532f31438920433805add44964399da5d0b8237cf562237ea3044d8d9", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrame.lean", "source_or_config": true, "archived_bytes": 5379, "archive_sha256": "883201e285b25218140363d24a6d5ae057908ae197f127cf686dc980b7a10734", "workspace_sha256": "883201e285b25218140363d24a6d5ae057908ae197f127cf686dc980b7a10734", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameIndex.lean", "source_or_config": true, "archived_bytes": 1184, "archive_sha256": "7a6a8a1988ef3d9bfaad74acaeb8b135eafb2219f631c0531167fc2ffb7caad3", "workspace_sha256": "7a6a8a1988ef3d9bfaad74acaeb8b135eafb2219f631c0531167fc2ffb7caad3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameLp.lean", "source_or_config": true, "archived_bytes": 2748, "archive_sha256": "230f65d3c7b8fb56e9a7aefc97667b21073d35aae94c89740736cd02d253772f", "workspace_sha256": "230f65d3c7b8fb56e9a7aefc97667b21073d35aae94c89740736cd02d253772f", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameMoments.lean", "source_or_config": true, "archived_bytes": 8570, "archive_sha256": "cbf741b32f8185450e96af0bd516f9cc7aee6c2c671126fbb9c677e2d226ecd1", "workspace_sha256": "cbf741b32f8185450e96af0bd516f9cc7aee6c2c671126fbb9c677e2d226ecd1", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameRowWitness.lean", "source_or_config": true, "archived_bytes": 10494, "archive_sha256": "daa22a2952060f29e2be1bc4a5801d0dfd643a89b4baf00649367c9e8f1cbf14", "workspace_sha256": "daa22a2952060f29e2be1bc4a5801d0dfd643a89b4baf00649367c9e8f1cbf14", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameSignContraction.lean", "source_or_config": true, "archived_bytes": 5679, "archive_sha256": "28e17de55f8094bddf6b06286c09ec49a54db675ec01c7b5ab9c569a4da02009", "workspace_sha256": "28e17de55f8094bddf6b06286c09ec49a54db675ec01c7b5ab9c569a4da02009", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameSignSample.lean", "source_or_config": true, "archived_bytes": 6405, "archive_sha256": "63a21e262596c7cdc6b0832de2f7b56bedb784177f0084fb1df8dba9f349a5ce", "workspace_sha256": "63a21e262596c7cdc6b0832de2f7b56bedb784177f0084fb1df8dba9f349a5ce", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameSymmetry.lean", "source_or_config": true, "archived_bytes": 7798, "archive_sha256": "3a22dee4034e1f35e3cc2b199dc557fcd675c7b2414a39e1514ede3b05eb20be", "workspace_sha256": "3a22dee4034e1f35e3cc2b199dc557fcd675c7b2414a39e1514ede3b05eb20be", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameTrace.lean", "source_or_config": true, "archived_bytes": 6426, "archive_sha256": "ceb640e3af666b3912844befa09a6e6f9fa61e07e2ac852e099cf0220aeff377", "workspace_sha256": "ceb640e3af666b3912844befa09a6e6f9fa61e07e2ac852e099cf0220aeff377", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameTraceBound.lean", "source_or_config": true, "archived_bytes": 7886, "archive_sha256": "dac30fd7fe2c091cdd7620c50a8725bd8f07b219743f3aff0f83f38d2212d026", "workspace_sha256": "dac30fd7fe2c091cdd7620c50a8725bd8f07b219743f3aff0f83f38d2212d026", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProductFrameWitness.lean", "source_or_config": true, "archived_bytes": 3481, "archive_sha256": "da712d68eb3a96c1dfc1e3cccea0c6ffbda604c35462ee91efdbd4f75121bd36", "workspace_sha256": "da712d68eb3a96c1dfc1e3cccea0c6ffbda604c35462ee91efdbd4f75121bd36", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProjectionCorollaries.lean", "source_or_config": true, "archived_bytes": 2316, "archive_sha256": "360a3c53aaa91561097a4d9f52003c9ea1f8a1977f5887b97b855e65f007fdb8", "workspace_sha256": "360a3c53aaa91561097a4d9f52003c9ea1f8a1977f5887b97b855e65f007fdb8", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProjectionOverlapLower.lean", "source_or_config": true, "archived_bytes": 4265, "archive_sha256": "6e44903deac25ba95e259440c849e51717ec603f8535424d610a75c88a645ca2", "workspace_sha256": "6e44903deac25ba95e259440c849e51717ec603f8535424d610a75c88a645ca2", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ProjectionPerturbation.lean", "source_or_config": true, "archived_bytes": 4456, "archive_sha256": "5b57cfefd0652d7f9a9e9c9d3fc91fbcbe9ff19b6726d68adf6ac6eece240009", "workspace_sha256": "5b57cfefd0652d7f9a9e9c9d3fc91fbcbe9ff19b6726d68adf6ac6eece240009", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/PureFrameDPR.lean", "source_or_config": true, "archived_bytes": 4594, "archive_sha256": "fd347d414686f23890eea36e21a286dd7077c0eaa85ee36c9baee6f1dac78af5", "workspace_sha256": "fd347d414686f23890eea36e21a286dd7077c0eaa85ee36c9baee6f1dac78af5", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RealMainConsequences.lean", "source_or_config": true, "archived_bytes": 2518, "archive_sha256": "095527a9d9f356f483ddc28b96c59fabbd781d2042f696d43ec0be1dc91759ee", "workspace_sha256": "095527a9d9f356f483ddc28b96c59fabbd781d2042f696d43ec0be1dc91759ee", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RealMainTheorem.lean", "source_or_config": true, "archived_bytes": 1550, "archive_sha256": "c08eb5568448a4908d5f90afd8da3ee5fdac8ee0e34e01824dc03ac6a3221917", "workspace_sha256": "c08eb5568448a4908d5f90afd8da3ee5fdac8ee0e34e01824dc03ac6a3221917", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveDiagonalBidualDPR.lean", "source_or_config": true, "archived_bytes": 2556, "archive_sha256": "e4e786bac003a667d8edb34d9eefd89f90709c3be3373527470bcd3e52823d78", "workspace_sha256": "e4e786bac003a667d8edb34d9eefd89f90709c3be3373527470bcd3e52823d78", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveDiagonalDPR.lean", "source_or_config": true, "archived_bytes": 3472, "archive_sha256": "f1c6dfb5e0ea4bf97af0c5ae66ea99e74059ccd5ef1b2584f2d144229cafdbd5", "workspace_sha256": "f1c6dfb5e0ea4bf97af0c5ae66ea99e74059ccd5ef1b2584f2d144229cafdbd5", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveDiagonalDualDPR.lean", "source_or_config": true, "archived_bytes": 2507, "archive_sha256": "ba91acf6624716006ed51206585e29cd5a3e56d9709293830d87b565ea996956", "workspace_sha256": "ba91acf6624716006ed51206585e29cd5a3e56d9709293830d87b565ea996956", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveHeadHilbert.lean", "source_or_config": true, "archived_bytes": 3562, "archive_sha256": "daa62e75b85090c6cc1716ca8e24cc47710aac7cbe9931d4f8f9c9e926da1cd7", "workspace_sha256": "daa62e75b85090c6cc1716ca8e24cc47710aac7cbe9931d4f8f9c9e926da1cd7", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveKernelHilbert.lean", "source_or_config": true, "archived_bytes": 2843, "archive_sha256": "b1eaa41d636df5c947a4802e817f0a0f21374008d3f4c1a4d8570bd4f1293942", "workspace_sha256": "b1eaa41d636df5c947a4802e817f0a0f21374008d3f4c1a4d8570bd4f1293942", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveParameters.lean", "source_or_config": true, "archived_bytes": 13500, "archive_sha256": "f8853a154ff22c5719c782f68031bafe8d5c84fd8724b53db5945fa9d35f7b5c", "workspace_sha256": "f8853a154ff22c5719c782f68031bafe8d5c84fd8724b53db5945fa9d35f7b5c", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveProjection.lean", "source_or_config": true, "archived_bytes": 9767, "archive_sha256": "a6bd8d6ac7310f8083ac2e63472a330dd8ca4ae953506866b73cf465c554b516", "workspace_sha256": "a6bd8d6ac7310f8083ac2e63472a330dd8ca4ae953506866b73cf465c554b516", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/RecursiveTailHilbert.lean", "source_or_config": true, "archived_bytes": 2176, "archive_sha256": "028c16f70a05efcb6db95137d0a1d2014523880f980cc88d51c3d333c5002901", "workspace_sha256": "028c16f70a05efcb6db95137d0a1d2014523880f980cc88d51c3d333c5002901", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/ReindexedFrameProjection.lean", "source_or_config": true, "archived_bytes": 7919, "archive_sha256": "500e79de37d725f26f55bae55b59a545bee1886614fb6ad1363721dbc97fcaa3", "workspace_sha256": "500e79de37d725f26f55bae55b59a545bee1886614fb6ad1363721dbc97fcaa3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/SchauderDPR.lean", "source_or_config": true, "archived_bytes": 5645, "archive_sha256": "e8bc5f58a504b0360dac97e49cf7dc56fa08ea74ffd3699a3c1ac4ba7aa9cadf", "workspace_sha256": "e8bc5f58a504b0360dac97e49cf7dc56fa08ea74ffd3699a3c1ac4ba7aa9cadf", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/SelectedCoefficientHilbert.lean", "source_or_config": true, "archived_bytes": 5955, "archive_sha256": "e196841bc3ac504cd6e80acd6c23471f129e3941add191b55127e04569186b4f", "workspace_sha256": "e196841bc3ac504cd6e80acd6c23471f129e3941add191b55127e04569186b4f", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/SelectedHilbertReplacement.lean", "source_or_config": true, "archived_bytes": 10879, "archive_sha256": "8548ed455ac4675872d9aa5acc4b771a6ef5c61f911f15d13fe7ec6b76dd37c3", "workspace_sha256": "8548ed455ac4675872d9aa5acc4b771a6ef5c61f911f15d13fe7ec6b76dd37c3", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/SelectedProjectionSetup.lean", "source_or_config": true, "archived_bytes": 9590, "archive_sha256": "138b176c395ca17fc9c440ce8d8df655269fc2d7ac9037285f7ace5fedeaca53", "workspace_sha256": "138b176c395ca17fc9c440ce8d8df655269fc2d7ac9037285f7ace5fedeaca53", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/TensorMoment.lean", "source_or_config": true, "archived_bytes": 10985, "archive_sha256": "8eeb17225fd0da439e2530f8fa503d596e8bbe8b25024ef78400593dc87f6648", "workspace_sha256": "8eeb17225fd0da439e2530f8fa503d596e8bbe8b25024ef78400593dc87f6648", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/TensorProjection.lean", "source_or_config": true, "archived_bytes": 9174, "archive_sha256": "e5f33e5a9bb60bdd5ec99cc09d719ee62c29e9f5ef3dc1dceec496b9f4faa5a7", "workspace_sha256": "e5f33e5a9bb60bdd5ec99cc09d719ee62c29e9f5ef3dc1dceec496b9f4faa5a7", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/TheoremStatement.lean", "source_or_config": true, "archived_bytes": 2912, "archive_sha256": "8bae1822f09c36532811144dfad0faefd1724ac184c0167745fae48f0af4cd97", "workspace_sha256": "8bae1822f09c36532811144dfad0faefd1724ac184c0167745fae48f0af4cd97", "status": "MATCH" }, { "relative_path": "ComplementedSubspace/UnconditionalHilbertSynthesis.lean", "source_or_config": true, "archived_bytes": 5811, "archive_sha256": "af4c40800fe8c7aeefcc1f0da019743694ad886b5462bf542958d6d2415358cd", "workspace_sha256": "af4c40800fe8c7aeefcc1f0da019743694ad886b5462bf542958d6d2415358cd", "status": "MATCH" }, { "relative_path": "MainRealTheoremDefinitions.lean", "source_or_config": true, "archived_bytes": 4923, "archive_sha256": "4819a6b830d5d35c955a1ff237387a68c7edaa14e93b21710c198113287a552c", "workspace_sha256": "4819a6b830d5d35c955a1ff237387a68c7edaa14e93b21710c198113287a552c", "status": "MATCH" }, { "relative_path": "MainTheoremReview.lean", "source_or_config": true, "archived_bytes": 4991, "archive_sha256": "28d39562ae38377baecfcce15bc7162f44abafc8bea2fb3350b0442ad3c91feb", "workspace_sha256": "28d39562ae38377baecfcce15bc7162f44abafc8bea2fb3350b0442ad3c91feb", "status": "MATCH" }, { "relative_path": "README.md", "source_or_config": false, "archived_bytes": 40109, "archive_sha256": "9f8dd7574c9d4c66e19d3e58f2bd7faf786c31b10fa7cca8ac27e86134ab9fc8", "workspace_sha256": "9f8dd7574c9d4c66e19d3e58f2bd7faf786c31b10fa7cca8ac27e86134ab9fc8", "status": "MATCH" }, { "relative_path": "WholeProjectAudit.lean", "source_or_config": true, "archived_bytes": 973, "archive_sha256": "25fd7072add542713a48f5ea3c2185b059820ea930adb285a770fa7971f45f43", "workspace_sha256": "25fd7072add542713a48f5ea3c2185b059820ea930adb285a770fa7971f45f43", "status": "MATCH" }, { "relative_path": "acceleration-assessment.md", "source_or_config": false, "archived_bytes": 3544, "archive_sha256": "9d4d6429665a1b53b5b898dc1e26c417a465c821ccbb7822a71c7c24da5df735", "workspace_sha256": "9d4d6429665a1b53b5b898dc1e26c417a465c821ccbb7822a71c7c24da5df735", "status": "MATCH" }, { "relative_path": "check-lattice-dependencies.ps1", "source_or_config": false, "archived_bytes": 1594, "archive_sha256": "bb78f149bdbe37969a3fea98323b5fc07796e1d0152d7211aa1f787ba68f4b8b", "workspace_sha256": "bb78f149bdbe37969a3fea98323b5fc07796e1d0152d7211aa1f787ba68f4b8b", "status": "MATCH" }, { "relative_path": "check-lean-direct.ps1", "source_or_config": false, "archived_bytes": 2244, "archive_sha256": "ef667d86a327eb9b6e9ad127d46e6429d8b94b4fed77bf43f42baf19179d8ffb", "workspace_sha256": "ef667d86a327eb9b6e9ad127d46e6429d8b94b4fed77bf43f42baf19179d8ffb", "status": "MATCH" }, { "relative_path": "complex-realification-shortcut.md", "source_or_config": false, "archived_bytes": 6172, "archive_sha256": "58b03da37388b6d3e0462464380dd10d9e2c1697e985ed52c6f1ca115cf95e93", "workspace_sha256": "58b03da37388b6d3e0462464380dd10d9e2c1697e985ed52c6f1ca115cf95e93", "status": "MATCH" }, { "relative_path": "complex-semantic-review.md", "source_or_config": false, "archived_bytes": 4897, "archive_sha256": "e5be536aade60afd6cbc7435f7f00e4827b1f63d721c6ba27c73251a72eefde3", "workspace_sha256": "e5be536aade60afd6cbc7435f7f00e4827b1f63d721c6ba27c73251a72eefde3", "status": "MATCH" }, { "relative_path": "corollary-scope-assessment.md", "source_or_config": false, "archived_bytes": 19305, "archive_sha256": "536b36e3db0978f77a77ab2724b9854afcb8c48de8c1c51a5136519beaa35efd", "workspace_sha256": "536b36e3db0978f77a77ab2724b9854afcb8c48de8c1c51a5136519beaa35efd", "status": "MATCH" }, { "relative_path": "finite-analytic-shortcuts.md", "source_or_config": false, "archived_bytes": 10337, "archive_sha256": "322fd5168da0f4e5e38f0c6726ba0b18b930d65f04428ace4bfd31a76696c0ed", "workspace_sha256": "322fd5168da0f4e5e38f0c6726ba0b18b930d65f04428ace4bfd31a76696c0ed", "status": "MATCH" }, { "relative_path": "finite-correction-progress.md", "source_or_config": false, "archived_bytes": 3447, "archive_sha256": "c9121a33fbe398e2d500c883456bafb2304c31e499be8deb66ccbe490834a112", "workspace_sha256": "c9121a33fbe398e2d500c883456bafb2304c31e499be8deb66ccbe490834a112", "status": "MATCH" }, { "relative_path": "finite-obstruction-progress.md", "source_or_config": false, "archived_bytes": 14953, "archive_sha256": "d2a0d5929535b5e8459cf6d6cdee80b0a5f1b7c2b4f9319317b9a3d4a41f1163", "workspace_sha256": "d2a0d5929535b5e8459cf6d6cdee80b0a5f1b7c2b4f9319317b9a3d4a41f1163", "status": "MATCH" }, { "relative_path": "finite-parameter-progress.md", "source_or_config": false, "archived_bytes": 7360, "archive_sha256": "836fd2027e9374375c0a86f1cb4bd07ef06d3b0be8e9adb8ce503d0d9b5b799f", "workspace_sha256": "836fd2027e9374375c0a86f1cb4bd07ef06d3b0be8e9adb8ce503d0d9b5b799f", "status": "MATCH" }, { "relative_path": "geometry-shortcut-assessment.md", "source_or_config": false, "archived_bytes": 9338, "archive_sha256": "dfea3748abecb27995244d3bfba9118ebfcf0471d69047a10b1e3e52ad323ebb", "workspace_sha256": "dfea3748abecb27995244d3bfba9118ebfcf0471d69047a10b1e3e52ad323ebb", "status": "MATCH" }, { "relative_path": "get-mathlib-cache.ps1", "source_or_config": false, "archived_bytes": 743, "archive_sha256": "26f674aa8f0de91940f008809d767a5939a433d2eeaa3c03f04a20eb6bb77a3d", "workspace_sha256": "26f674aa8f0de91940f008809d767a5939a433d2eeaa3c03f04a20eb6bb77a3d", "status": "MATCH" }, { "relative_path": "lake-manifest.json", "source_or_config": true, "archived_bytes": 3681, "archive_sha256": "5a1a4b9a38d977d11c668216238f135a975d4ee757f2b4c25bfd9e0f588324e8", "workspace_sha256": "5a1a4b9a38d977d11c668216238f135a975d4ee757f2b4c25bfd9e0f588324e8", "status": "MATCH" }, { "relative_path": "lakefile.toml", "source_or_config": true, "archived_bytes": 377, "archive_sha256": "2d6217379e267956a128d7bf9026e3a84fb6d699e5a941172901c4c37f0d1863", "workspace_sha256": "2d6217379e267956a128d7bf9026e3a84fb6d699e5a941172901c4c37f0d1863", "status": "MATCH" }, { "relative_path": "lattice-progress.md", "source_or_config": false, "archived_bytes": 17097, "archive_sha256": "412dd82afe2d4a863e88442e59ca30e22afedf6f52a349faf631a42333f89a56", "workspace_sha256": "412dd82afe2d4a863e88442e59ca30e22afedf6f52a349faf631a42333f89a56", "status": "MATCH" }, { "relative_path": "lean-toolchain", "source_or_config": true, "archived_bytes": 30, "archive_sha256": "3a3b72fe5a9f28230ef800828bfd48d585b2f493a3f66c86a2913f87e7ff0ccc", "workspace_sha256": "3a3b72fe5a9f28230ef800828bfd48d585b2f493a3f66c86a2913f87e7ff0ccc", "status": "MATCH" }, { "relative_path": "local-hilbert-progress.md", "source_or_config": false, "archived_bytes": 14415, "archive_sha256": "d4b7ace1d638efdcd61a01fe2d3363007e77a029a34af2375c9104708e338198", "workspace_sha256": "d4b7ace1d638efdcd61a01fe2d3363007e77a029a34af2375c9104708e338198", "status": "MATCH" }, { "relative_path": "manuscript/1-Introduction.tex", "source_or_config": false, "archived_bytes": 12093, "archive_sha256": "5a6e6b5bd26e9e0154be5f8b35f1b493e91c8f0410bfa707084edf5f2be152d9", "workspace_sha256": "5a6e6b5bd26e9e0154be5f8b35f1b493e91c8f0410bfa707084edf5f2be152d9", "status": "MATCH" }, { "relative_path": "manuscript/1a-Preliminaries.tex", "source_or_config": false, "archived_bytes": 10299, "archive_sha256": "0c11065e4802725ac75ec6cd0631f62a4f71a8be7277da9450c35b734d5c5895", "workspace_sha256": "0c11065e4802725ac75ec6cd0631f62a4f71a8be7277da9450c35b734d5c5895", "status": "MATCH" }, { "relative_path": "manuscript/2-Circle-tensors.tex", "source_or_config": false, "archived_bytes": 6027, "archive_sha256": "46f1b3d53b3789c3c7e967d8ed8f3f50baf3980084b443153abd164bf2ffa197", "workspace_sha256": "46f1b3d53b3789c3c7e967d8ed8f3f50baf3980084b443153abd164bf2ffa197", "status": "MATCH" }, { "relative_path": "manuscript/2-Construction.tex", "source_or_config": false, "archived_bytes": 605, "archive_sha256": "43910666f6e385963ae921c4caaa6f0ddf94bd875dda0d33693b7a5a4356c847", "workspace_sha256": "43910666f6e385963ae921c4caaa6f0ddf94bd875dda0d33693b7a5a4356c847", "status": "MATCH" }, { "relative_path": "manuscript/3-Fourth-moments.tex", "source_or_config": false, "archived_bytes": 4922, "archive_sha256": "0ede59904c9317f4d3fbb0658860da7f9573c74bb5e50b326109e00197af9886", "workspace_sha256": "0ede59904c9317f4d3fbb0658860da7f9573c74bb5e50b326109e00197af9886", "status": "MATCH" }, { "relative_path": "manuscript/4-Overlap.tex", "source_or_config": false, "archived_bytes": 5342, "archive_sha256": "4f9373b4cc06bf595355daeaa55ecee13e545d8200761ce7bad090b0add0b9ec", "workspace_sha256": "4f9373b4cc06bf595355daeaa55ecee13e545d8200761ce7bad090b0add0b9ec", "status": "MATCH" }, { "relative_path": "manuscript/5-Parameters.tex", "source_or_config": false, "archived_bytes": 3558, "archive_sha256": "a4fb95577e3a5d1889e5cb8e5d5240d670c2e8ac7c2957976afa2c9c7a2b64aa", "workspace_sha256": "a4fb95577e3a5d1889e5cb8e5d5240d670c2e8ac7c2957976afa2c9c7a2b64aa", "status": "MATCH" }, { "relative_path": "manuscript/6-Infinite-sum.tex", "source_or_config": false, "archived_bytes": 12748, "archive_sha256": "7d95d2b380fdbf3fc84e63afa1f27904f877dee68a328f3a4d67f1eb7340f90f", "workspace_sha256": "7d95d2b380fdbf3fc84e63afa1f27904f877dee68a328f3a4d67f1eb7340f90f", "status": "MATCH" }, { "relative_path": "manuscript/7-Explicit-embedding.tex", "source_or_config": false, "archived_bytes": 6159, "archive_sha256": "3f16818e4480e6f717d7b49bd81c43fe5fd6712dbd11f1c63dcec966ed3bfe03", "workspace_sha256": "3f16818e4480e6f717d7b49bd81c43fe5fd6712dbd11f1c63dcec966ed3bfe03", "status": "MATCH" }, { "relative_path": "manuscript/7a-Banach-lattices.tex", "source_or_config": false, "archived_bytes": 15052, "archive_sha256": "6d103dcace388aa4e4cf46e83ef38d65d70de2ef7ff8540082eeb421ebfeef57", "workspace_sha256": "6d103dcace388aa4e4cf46e83ef38d65d70de2ef7ff8540082eeb421ebfeef57", "status": "MATCH" }, { "relative_path": "manuscript/9-Geometry.tex", "source_or_config": false, "archived_bytes": 242, "archive_sha256": "a5ff4d86107a6385a307a13402ee73967ac5c871481a4f8cd906f85701c4e87d", "workspace_sha256": "a5ff4d86107a6385a307a13402ee73967ac5c871481a4f8cd906f85701c4e87d", "status": "MATCH" }, { "relative_path": "manuscript/9a-Schauder-bases.tex", "source_or_config": false, "archived_bytes": 7330, "archive_sha256": "07ab8283bc43bd0c88edf18c5953f0ca1bdbd333f5f4759a06f269a0f2dd925c", "workspace_sha256": "07ab8283bc43bd0c88edf18c5953f0ca1bdbd333f5f4759a06f269a0f2dd925c", "status": "MATCH" }, { "relative_path": "manuscript/9b-Geometric-remark.tex", "source_or_config": false, "archived_bytes": 606, "archive_sha256": "b61a6c84131aff94a217cc26618a496ac8b5620ae6f4b7bbbde5de448c2be7b5", "workspace_sha256": "b61a6c84131aff94a217cc26618a496ac8b5620ae6f4b7bbbde5de448c2be7b5", "status": "MATCH" }, { "relative_path": "manuscript/README.md", "source_or_config": false, "archived_bytes": 815, "archive_sha256": "34f191867cfb4885f4171c1c7fb985a1591b632e1762603c70f450e57e32a615", "workspace_sha256": "34f191867cfb4885f4171c1c7fb985a1591b632e1762603c70f450e57e32a615", "status": "MATCH" }, { "relative_path": "manuscript/bibliography.tex", "source_or_config": false, "archived_bytes": 6021, "archive_sha256": "c6f5955ce9d1f3d4eb54a8c23afb49e724d6fdaf263d86928769ee802f817aee", "workspace_sha256": "c6f5955ce9d1f3d4eb54a8c23afb49e724d6fdaf263d86928769ee802f817aee", "status": "MATCH" }, { "relative_path": "manuscript/main.tex", "source_or_config": false, "archived_bytes": 4803, "archive_sha256": "82b3c7f240dccc379d831c6d6c2904a44bdf28a16c7d1c529d819fdcbaa68375", "workspace_sha256": "82b3c7f240dccc379d831c6d6c2904a44bdf28a16c7d1c529d819fdcbaa68375", "status": "MATCH" }, { "relative_path": "package-verified.ps1", "source_or_config": false, "archived_bytes": 12426, "archive_sha256": "f3963da6edfbf5690b5ed55c8b4438168e9fc1bb5a7c9250efc3241610ab11c7", "workspace_sha256": "f3963da6edfbf5690b5ed55c8b4438168e9fc1bb5a7c9250efc3241610ab11c7", "status": "MATCH" }, { "relative_path": "projection-progress.md", "source_or_config": false, "archived_bytes": 11113, "archive_sha256": "fbfc6c5fef40c20ebf201cd5b1c832c2f1a0fd4b62e67ad2fa6039391ec0ce83", "workspace_sha256": "fbfc6c5fef40c20ebf201cd5b1c832c2f1a0fd4b62e67ad2fa6039391ec0ce83", "status": "MATCH" }, { "relative_path": "real-main-semantic-review.md", "source_or_config": false, "archived_bytes": 4406, "archive_sha256": "f17ff0023890bb6bfbe22d1fa4db322d973a07b975da42b43fe77dc210944be9", "workspace_sha256": "f17ff0023890bb6bfbe22d1fa4db322d973a07b975da42b43fe77dc210944be9", "status": "MATCH" }, { "relative_path": "rebuild-verified.ps1", "source_or_config": false, "archived_bytes": 5571, "archive_sha256": "3ef05bacd6a284da2eb00622b7c7e37239a9f8d04a6c91fceea3dcb35640665e", "workspace_sha256": "3ef05bacd6a284da2eb00622b7c7e37239a9f8d04a6c91fceea3dcb35640665e", "status": "MATCH" }, { "relative_path": "recursive-parameter-progress.md", "source_or_config": false, "archived_bytes": 2690, "archive_sha256": "4886b80d37cbefabb6089707bd109b77e4d3618f3b1b1f63c5fc43a846fb1acc", "workspace_sha256": "4886b80d37cbefabb6089707bd109b77e4d3618f3b1b1f63c5fc43a846fb1acc", "status": "MATCH" }, { "relative_path": "run-lean.ps1", "source_or_config": false, "archived_bytes": 521, "archive_sha256": "829e31726c7fe28107c8a2b9437f40efdd27d81caac5c73b4e59aca12c256cff", "workspace_sha256": "829e31726c7fe28107c8a2b9437f40efdd27d81caac5c73b4e59aca12c256cff", "status": "MATCH" }, { "relative_path": "shortcut-plan.md", "source_or_config": false, "archived_bytes": 12035, "archive_sha256": "ffc36bb25e122a5b4bee023325da276c35870245f06402441634d04babf2a781", "workspace_sha256": "ffc36bb25e122a5b4bee023325da276c35870245f06402441634d04babf2a781", "status": "MATCH" }, { "relative_path": "statement-review.md", "source_or_config": false, "archived_bytes": 12311, "archive_sha256": "e06b2c082222eaa13b0635e62c0d087726858a40bcdadc978babad484bea3df7", "workspace_sha256": "e06b2c082222eaa13b0635e62c0d087726858a40bcdadc978babad484bea3df7", "status": "MATCH" }, { "relative_path": "verification/ambient-lattice-bounds-axioms.log", "source_or_config": false, "archived_bytes": 803, "archive_sha256": "cb75046a20d40d1cb3406b84085bb4873076fb010eab46c4028fffcbd491e5f4", "workspace_sha256": "cb75046a20d40d1cb3406b84085bb4873076fb010eab46c4028fffcbd491e5f4", "status": "MATCH" }, { "relative_path": "verification/axioms.log", "source_or_config": false, "archived_bytes": 1835, "archive_sha256": "2cbe3be82744c6e8fc4c305934f748eb9224772687d090e9e585ea7de98f1e2c", "workspace_sha256": "2cbe3be82744c6e8fc4c305934f748eb9224772687d090e9e585ea7de98f1e2c", "status": "MATCH" }, { "relative_path": "verification/build.log", "source_or_config": false, "archived_bytes": 4058, "archive_sha256": "72a8e260d052541568dba40eed6a82548e6efdf385da139a1e26a0ba31c5e650", "workspace_sha256": "72a8e260d052541568dba40eed6a82548e6efdf385da139a1e26a0ba31c5e650", "status": "MATCH" }, { "relative_path": "verification/complex-ambient-axioms.log", "source_or_config": false, "archived_bytes": 602, "archive_sha256": "d108dcb4c46dbe088564457f0c5bf8c78dd2ca24ccf417ca290eb53266f7270a", "workspace_sha256": "d108dcb4c46dbe088564457f0c5bf8c78dd2ca24ccf417ca290eb53266f7270a", "status": "MATCH" }, { "relative_path": "verification/complex-corollary-axioms.log", "source_or_config": false, "archived_bytes": 100, "archive_sha256": "28fb90b054f63d8472f51f14a89b7704231be558f3519b40f493ec4b58bfa4b8", "workspace_sha256": "28fb90b054f63d8472f51f14a89b7704231be558f3519b40f493ec4b58bfa4b8", "status": "MATCH" }, { "relative_path": "verification/complex-projection-axioms.log", "source_or_config": false, "archived_bytes": 858, "archive_sha256": "24e77e84841462cf13324af550ed43148783b4eddc6ffd4d0138755cf53460ba", "workspace_sha256": "24e77e84841462cf13324af550ed43148783b4eddc6ffd4d0138755cf53460ba", "status": "MATCH" }, { "relative_path": "verification/complex-recursive-projection-axioms.log", "source_or_config": false, "archived_bytes": 1367, "archive_sha256": "05456ac1ef780d0a62d7475289e5314fbb2531c9697cec05fd081b708e0115ef", "workspace_sha256": "05456ac1ef780d0a62d7475289e5314fbb2531c9697cec05fd081b708e0115ef", "status": "MATCH" }, { "relative_path": "verification/final-axioms.log", "source_or_config": false, "archived_bytes": 732, "archive_sha256": "414ce4a65cb4a27fffd4e2a8a719d58826ca8eab9009b70a7f2f148fd6421dc4", "workspace_sha256": "414ce4a65cb4a27fffd4e2a8a719d58826ca8eab9009b70a7f2f148fd6421dc4", "status": "MATCH" }, { "relative_path": "verification/finite-dual-dpr-lower-axioms.log", "source_or_config": false, "archived_bytes": 241, "archive_sha256": "98f397dfae84514e8cb7639db7b026a1f491509e4fc45de8be61ad60b25f5c56", "workspace_sha256": "98f397dfae84514e8cb7639db7b026a1f491509e4fc45de8be61ad60b25f5c56", "status": "MATCH" }, { "relative_path": "verification/finite-head-hilbert-axioms.log", "source_or_config": false, "archived_bytes": 1128, "archive_sha256": "1c870370d1b90b7fbd9024c6e36b6318c5528145e683355274a8e010030beb8e", "workspace_sha256": "1c870370d1b90b7fbd9024c6e36b6318c5528145e683355274a8e010030beb8e", "status": "MATCH" }, { "relative_path": "verification/finite-selected-hilbert-model-axioms.log", "source_or_config": false, "archived_bytes": 264, "archive_sha256": "62cca4dac83f2c4dee48d3ccc5746f153e95baf0cb534fec52fcf36d8e25a862", "workspace_sha256": "62cca4dac83f2c4dee48d3ccc5746f153e95baf0cb534fec52fcf36d8e25a862", "status": "MATCH" }, { "relative_path": "verification/fresh-root-build-before-finite-basis-fix.log", "source_or_config": false, "archived_bytes": 19240, "archive_sha256": "7a8f7f22bbc0650f7cb781f09fc5227b40f1f5862e95e910b9fc1a1f6526efca", "workspace_sha256": "7a8f7f22bbc0650f7cb781f09fc5227b40f1f5862e95e910b9fc1a1f6526efca", "status": "MATCH" }, { "relative_path": "verification/fresh-root-build.log", "source_or_config": false, "archived_bytes": 168941, "archive_sha256": "cee1b3f4042562d4bd1f674280e83f3d0bbeaa9eded783d660165602dd149cb2", "workspace_sha256": "cee1b3f4042562d4bd1f674280e83f3d0bbeaa9eded783d660165602dd149cb2", "status": "MATCH" }, { "relative_path": "verification/implementation-checkpoint-1.log", "source_or_config": false, "archived_bytes": 988, "archive_sha256": "ffb26d10a1f9d5c6bccaf9c2e4f8632ddd807be1189bf8698c89581b6946effa", "workspace_sha256": "ffb26d10a1f9d5c6bccaf9c2e4f8632ddd807be1189bf8698c89581b6946effa", "status": "MATCH" }, { "relative_path": "verification/implementation-checkpoint-2.log", "source_or_config": false, "archived_bytes": 969, "archive_sha256": "5a9d8c28eed45066e5dce5a8c0ea999f99a4bb2438afdb5178af21d81ed654e9", "workspace_sha256": "5a9d8c28eed45066e5dce5a8c0ea999f99a4bb2438afdb5178af21d81ed654e9", "status": "MATCH" }, { "relative_path": "verification/implementation-checkpoint-3.log", "source_or_config": false, "archived_bytes": 135, "archive_sha256": "d56782d8238136789d0d4dbea7c9caff7c7ab01e2ed7cae5e8fc3cfcbcf022fb", "workspace_sha256": "d56782d8238136789d0d4dbea7c9caff7c7ab01e2ed7cae5e8fc3cfcbcf022fb", "status": "MATCH" }, { "relative_path": "verification/lattice-axioms.log", "source_or_config": false, "archived_bytes": 627, "archive_sha256": "5839d22d9d8ec3a289f0ddc7ec99c47d748f97bcbe49515a5341f851de375b80", "workspace_sha256": "5839d22d9d8ec3a289f0ddc7ec99c47d748f97bcbe49515a5341f851de375b80", "status": "MATCH" }, { "relative_path": "verification/lattice-isomorphism-axioms.log", "source_or_config": false, "archived_bytes": 506, "archive_sha256": "a1d64e4595cfcec7b68566a6258d859a726b7bcf1bbdade31c6a6272c46018a9", "workspace_sha256": "a1d64e4595cfcec7b68566a6258d859a726b7bcf1bbdade31c6a6272c46018a9", "status": "MATCH" }, { "relative_path": "verification/local-hilbert-embedded-renorm-axioms.log", "source_or_config": false, "archived_bytes": 489, "archive_sha256": "8ae4fdcf869a20e900b8d1e5fdb8d3074df13197ec15661ea406b23960d45eb6", "workspace_sha256": "8ae4fdcf869a20e900b8d1e5fdb8d3074df13197ec15661ea406b23960d45eb6", "status": "MATCH" }, { "relative_path": "verification/lp-uniform-equiv-axioms.log", "source_or_config": false, "archived_bytes": 638, "archive_sha256": "04509f9e2266a61b0e549680db927624c61776a7c84f2391b46f73f9d7f8bec8", "workspace_sha256": "04509f9e2266a61b0e549680db927624c61776a7c84f2391b46f73f9d7f8bec8", "status": "MATCH" }, { "relative_path": "verification/normalized-hilbert-synthesis-axioms.log", "source_or_config": false, "archived_bytes": 600, "archive_sha256": "b844bd2734d897b2850a8895cf3aef74647ebffd1c79801918397ad7924fee47", "workspace_sha256": "b844bd2734d897b2850a8895cf3aef74647ebffd1c79801918397ad7924fee47", "status": "MATCH" }, { "relative_path": "verification/projection-corollaries-axioms.log", "source_or_config": false, "archived_bytes": 362, "archive_sha256": "cf62169ed9e5fccf4aa1d57a8dfc6ba4030e1a8727bc441e5f6eee5645e61251", "workspace_sha256": "cf62169ed9e5fccf4aa1d57a8dfc6ba4030e1a8727bc441e5f6eee5645e61251", "status": "MATCH" }, { "relative_path": "verification/pure-frame-dpr-axioms.log", "source_or_config": false, "archived_bytes": 1130, "archive_sha256": "22a92a01c764abd9d7874ca1c7a5a1a96540adfe64666879eef34e8d4cf560be", "workspace_sha256": "22a92a01c764abd9d7874ca1c7a5a1a96540adfe64666879eef34e8d4cf560be", "status": "MATCH" }, { "relative_path": "verification/real-construction-axioms.log", "source_or_config": false, "archived_bytes": 680, "archive_sha256": "272d380e56f19e95c01f0f164a449313d4c1654c39eee5fd6c733fa81b925e1a", "workspace_sha256": "272d380e56f19e95c01f0f164a449313d4c1654c39eee5fd6c733fa81b925e1a", "status": "MATCH" }, { "relative_path": "verification/real-main-axioms.log", "source_or_config": false, "archived_bytes": 613, "archive_sha256": "b7014967fa884fb4f5ab4dea148046b67543ac1f54171b68d166063a4fcdd5a5", "workspace_sha256": "b7014967fa884fb4f5ab4dea148046b67543ac1f54171b68d166063a4fcdd5a5", "status": "MATCH" }, { "relative_path": "verification/real-main-consequences-axioms.log", "source_or_config": false, "archived_bytes": 679, "archive_sha256": "e4efbb48935a0e9aedd60ce63d0c82c9e044ac1cd45bdb386dc9cb41103db787", "workspace_sha256": "e4efbb48935a0e9aedd60ce63d0c82c9e044ac1cd45bdb386dc9cb41103db787", "status": "MATCH" }, { "relative_path": "verification/recursive-kernel-hilbert-axioms.log", "source_or_config": false, "archived_bytes": 632, "archive_sha256": "a8919fb3d9641cd9a4f9be37d1abf14ae9118233eb02157a8d5fe5c5e7f06e15", "workspace_sha256": "a8919fb3d9641cd9a4f9be37d1abf14ae9118233eb02157a8d5fe5c5e7f06e15", "status": "MATCH" }, { "relative_path": "verification/root-local-source-files.txt", "source_or_config": false, "archived_bytes": 8033, "archive_sha256": "b9bbcfc2e06165a18063c479261ad6a55d5cd72687dad695af5b17ce10762c15", "workspace_sha256": "b9bbcfc2e06165a18063c479261ad6a55d5cd72687dad695af5b17ce10762c15", "status": "MATCH" }, { "relative_path": "verification/schauder-dpr-axioms.log", "source_or_config": false, "archived_bytes": 632, "archive_sha256": "9a0ae0a17cdd0af6d2ead9ca5033e0cf71f7cb76a6058099c0821b3a289bbe09", "workspace_sha256": "9a0ae0a17cdd0af6d2ead9ca5033e0cf71f7cb76a6058099c0821b3a289bbe09", "status": "MATCH" }, { "relative_path": "verification/selected-coefficient-hilbert-axioms.log", "source_or_config": false, "archived_bytes": 643, "archive_sha256": "4ffe89814588ad268eec0a49e505542b0d7ba763063747a9972b0f7a6841d6d1", "workspace_sha256": "4ffe89814588ad268eec0a49e505542b0d7ba763063747a9972b0f7a6841d6d1", "status": "MATCH" }, { "relative_path": "verification/selected-frame-basis-axioms.log", "source_or_config": false, "archived_bytes": 359, "archive_sha256": "1c2301f3bb63f1d569e865c2d5abe32e20358b891d232a4acb71eb0b42165a5b", "workspace_sha256": "1c2301f3bb63f1d569e865c2d5abe32e20358b891d232a4acb71eb0b42165a5b", "status": "MATCH" }, { "relative_path": "verification/selected-hilbert-replacement-axioms.log", "source_or_config": false, "archived_bytes": 690, "archive_sha256": "e62ab1af44cedc412cfeb29a69fa4c829943306d840ce2a29f839be5c4271f90", "workspace_sha256": "e62ab1af44cedc412cfeb29a69fa4c829943306d840ce2a29f839be5c4271f90", "status": "MATCH" }, { "relative_path": "verification/selected-projection-setup-axioms.log", "source_or_config": false, "archived_bytes": 987, "archive_sha256": "3ad424d83053c769e2322ac3e85392057ef857aa8522367c0728bfc6dfefbddd", "workspace_sha256": "3ad424d83053c769e2322ac3e85392057ef857aa8522367c0728bfc6dfefbddd", "status": "MATCH" }, { "relative_path": "verification/shortcut-axioms.log", "source_or_config": false, "archived_bytes": 134, "archive_sha256": "9499cbc437490898873c8945f907291a4be034ef9ad6da3c1fc0a22136e21a17", "workspace_sha256": "9499cbc437490898873c8945f907291a4be034ef9ad6da3c1fc0a22136e21a17", "status": "MATCH" }, { "relative_path": "verification/shortcut-build.log", "source_or_config": false, "archived_bytes": 8436, "archive_sha256": "fa3eab89216c8f038746eaee6a96ee39c044d1a8dd7e16898dcb0d2e8f44a54c", "workspace_sha256": "fa3eab89216c8f038746eaee6a96ee39c044d1a8dd7e16898dcb0d2e8f44a54c", "status": "MATCH" }, { "relative_path": "verification/whole-project-axioms.log", "source_or_config": false, "archived_bytes": 134, "archive_sha256": "c8acfda60e99a503e44bc910ac390ca44786c1de777f93c2fb7778b2b061e22c", "workspace_sha256": "c8acfda60e99a503e44bc910ac390ca44786c1de777f93c2fb7778b2b061e22c", "status": "MATCH" }, { "relative_path": "SOURCE-MANIFEST.sha256", "source_or_config": false, "archived_bytes": 27838, "archive_sha256": "c9311dda53584927098354931922a12d303fa9cceba4a218c270f868aad82828", "workspace_sha256": null, "status": "MISSING" } ] } STDOUT END STDERR BEGIN STDERR END EXIT CODE: 0