PHASE 5 — BUILD EXIT STATUS

================================================================
FIRST ATTEMPT — AUDITOR ERROR, NOT A REPOSITORY FAILURE
================================================================
Command : lake build --jobs 4 ConnesRigidity
Exit    : 1
Elapsed : 0:00.11
Output  : error: unknown long option '--jobs'

CLASSIFICATION: TOOLING / AUDITOR ERROR.

This is recorded rather than discarded, per audit rule 6 (preserve every
command and error). It is NOT a build failure of the repository and NOT a
source failure. Lake 5.0.0 exposes no `-j` or `--jobs` option at all —
verified against `lake --help` and `lake help build`, neither of which lists
a jobs flag. Nothing was compiled; the process exited in 0.11 seconds.

CONSEQUENCE FOR THE AUDIT PROMPT'S PARALLELISM GUIDANCE:
The prompt directs "at most 2 build jobs" at ~16 GB and "at most 4" at
~32 GB. That guidance is not directly expressible in Lake 5.0.0, which has
no job-count CLI option. The nearest available control is Lean's thread
count, so LEAN_NUM_THREADS=4 was used instead (32 GB tier). The substitution
is recorded rather than silently made. Note also that job parallelism is
largely irrelevant to this particular target: Mathlib was fully restored
from cache, so the build compiled essentially a single module, and one Lean
file is elaborated by one process regardless of job count.

================================================================
SECOND ATTEMPT — THE AUDITED BUILD
================================================================
Command      : LEAN_NUM_THREADS=4 lake build ConnesRigidity
Working dir  : /root/audits/pinned  (detached worktree @ 94bc0feb...)
Started      : 2026-08-06T07:50:35.96-04:00
Finished     : 2026-08-06T07:56:09.46-04:00

EXIT STATUS  : 0

Resource measurements (/usr/bin/time -v):
    Elapsed (wall clock)          : 5:31.95
    User time                     : 623.48 s
    System time                   : 16.61 s
    Percent of CPU                : 192%
    Maximum resident set size     : 10,844,244 KB  = 10.34 GiB
    Swaps                         : 0
    Major page faults             : 25,624
    Minor page faults             : 1,424,690
    Voluntary context switches    : 552,329
    File system inputs            : 16,206,800
    File system outputs           : 138,336
    Page size                     : 4096 bytes

MEMORY NOTE — recorded honestly:
Peak RSS was 10.34 GiB with ZERO swaps. WSL2's default allocation on this
host would have been ~15 GiB (50% of 31.69 GB). The build would therefore
most likely have fit within the default allocation, with roughly 4.5 GiB of
headroom. The allocation was raised to 24 GB (via .wslconfig) BEFORE the
build as a precaution against the anticipated single-large-file risk. In
hindsight that precaution was probably not strictly necessary. It is
recorded because the audit should not overstate the difficulty of what it
did, and because the measured peak is the useful number for anyone
reproducing this.

================================================================
BUILD DIAGNOSTICS
================================================================
Lake emitted NO warnings, NO errors, and no progress lines on this build
(non-TTY invocation suppresses the progress indicator). The complete
captured output of the build command consists of the /usr/bin/time -v
resource block reproduced above and nothing else. There were no `sorry`
warnings, no `unused variable` diagnostics, and no deprecation notices.

================================================================
ARTIFACTS PRODUCED (proof of LOCAL compilation)
================================================================
/root/audits/pinned/.lake/build/lib/lean/
    ConnesRigidity.olean        61,174,904 bytes   Aug  6 07:55
    ConnesRigidity.ilean         4,255,264 bytes   Aug  6 07:56
    ConnesRigidity.olean.hash           16 bytes
    ConnesRigidity.ilean.hash           16 bytes
    ConnesRigidity.trace             2,381 bytes

WAS THE TARGET ACTUALLY COMPILED HERE, OR RESTORED FROM CACHE?
COMPILED HERE. This was established BEFORE the build, not inferred after:

  - Immediately after `lake exe cache get` and before `lake build`, a search
    of .lake/build for any file named ConnesRigidity* returned nothing. The
    Mathlib cache contains Mathlib artifacts only (8,275 .olean files under
    .lake/packages/mathlib/); ConnesRigidity is not a Mathlib module and has
    no cache entry.
  - The build then consumed 623 seconds of user CPU and 10.34 GiB peak RSS —
    consistent with genuine elaboration, not with artifact restoration.
  - The resulting .olean carries a build timestamp of 07:55, inside the
    build window 07:50:35 - 07:56:09.

Because the target's absence was verified beforehand, the plan's
delete-and-rebuild step was unnecessary and was not performed; the evidence
it would have produced is already in hand.

================================================================
SOURCE INTEGRITY AFTER THE BUILD
================================================================
git status --porcelain=v1 (pinned worktree) : EMPTY (clean)
ConnesRigidity.lean SHA-256  : 31f6c419f341ee6aa5b03bc15800a9d8ee2c654c344aab90bdef0639353ccc91
                               (unchanged from Phase 2)
lake-manifest.json SHA-256   : d366c97598e820009831d12376d4e41004b1847ac6074ec79b15bf9e1ea09d46
                               (unchanged from Phase 2)

No tracked file was modified at any point. `lake update` was never run.
.lake/ is gitignored, so build output does not dirty the tree.

================================================================
WHAT THIS EXIT CODE DOES AND DOES NOT ESTABLISH
================================================================
DOES: the pinned file elaborated and compiled successfully under Lean 4.32.0
on this machine, and Lean's kernel accepted the declarations it produced
during that elaboration.

DOES NOT: establish the axiom dependency set (see print_axioms.log), verify
the proof terms through an independent kernel (see comparator.log), or say
anything about whether the formal statements faithfully capture the informal
theorem. A successful compilation is not a mathematical endorsement.
