Inspection time: 2026-07-23 10:39:24 -07:00.
| Tool | Status | Exact evidence |
|---|---|---|
| Windows | installed | Microsoft Windows NT 10.0.26200.0; PowerShell 5.1.26100.8875 |
| Git | installed | 2.48.1.windows.1 |
| Python | installed | C:\Users\Gzw19\miniconda3\python.exe; CPython 3.13.9, Anaconda build |
| SymPy | installed | 1.14.0 |
| pytest | installed | 8.4.2 |
| SageMath | installed in Docker | official SageMath 10.9 image, pinned as sagemath/sagemath@sha256:e068670ae5863b54b2550e72437ec637b0283acb0dc712c8584c124dbf44e667; release 2026-05-04 |
| Singular | installed in the Sage container | Singular 4.4.1, January 2025; exact modStd(I,1) and FGLM run successfully |
| Lean / Lake | not found | neither command resolved |
| Mathematica / Maple | not found | wolframscript absent; Maple not detected |
| Macaulay2 | not found | M2 absent |
| GAP / PARI-GP | not found | gap and pari-gp absent; PowerShell gp is only the Get-ItemProperty alias |
| R | not found | PowerShell r is only the Invoke-History alias |
| Docker Desktop | installed | 4.76.0; Linux engine used for the exact Sage/Singular certificates |
| WSL CLI | no user distribution | wsl -l -q returned no named distribution; Docker's managed Linux engine is available |
| Poppler | bundled runtime available | pdftoppm.exe under the Codex bundled dependency runtime rendered both Nguyen papers |
Get-CimInstance Win32_OperatingSystem failed with access denied, so the OS version was obtained from [System.Environment]::OSVersion instead. The Python launcher py reported no registered Python even though the explicit Miniconda interpreter works; all commands therefore use python at the path above.
The Gate-5 run downloaded the official SageMath container and executed both
the primary and independent exact number-field certificates. Lean remains an
unexecuted optional formalization route, not evidence. During the flagged-infinity run the original
Nguyen 1999 and 2004 PDFs were downloaded into references/papers/, text was
extracted, and the cited pages were rendered and visually inspected. Older
placeholder formalization entrypoints remain plans and are not cited as evidence.