PHASE 5b — REPLAY PROVENANCE
"Was the environment freshly replayed, or were cached/exported artifacts
 trusted?"

This file exists to license — or withhold — any claim that the Comparator
path is stronger evidence than the plain build. Read it before quoting the
exit code.

================================================================
1. WAS THE ENVIRONMENT FRESHLY REPLAYED?
================================================================
PARTLY, AND THE PARTS DIFFER. Specifically:

  CHALLENGE MODULE — freshly replayed through the Lean kernel.
      Observed: "[8655/8655] Replayed ComparatorChallenges.E_ConnesRigidity"
      All 8,655 declarations in the challenge environment were re-checked.

  SOLUTION MODULE — built during the Comparator run, then exported and
      re-checked.
      Observed: "Building ConnesRigidity" ->
                "Build completed successfully (8656 jobs)"
      Then: export of the target constants, then kernel + nanoda checking.

  NANODA — ran and accepted.
      Observed: "Running nanoda kernel on solution"
                "Nanoda kernel accepts the solution"
      nanoda is an INDEPENDENT Rust implementation of the Lean kernel
      (github.com/ammkrn/nanoda_lib @ 418320295890...). Its acceptance is
      not merely the Lean kernel agreeing with itself.

================================================================
2. WHICH .olean FILES CAME FROM CACHE VS WERE COMPILED LOCALLY?
================================================================
DOWNLOADED, NOT COMPILED HERE:
    8,639 Mathlib .olean files, fetched by `lake exe cache get` from
    https://lakecache.blob.core.windows.net/mathlib4-master
    (8,275 present under .lake/packages/mathlib/.lake/build/lib)

    These artifacts were NOT re-elaborated and NOT kernel-checked on this
    machine. They are trusted as distributed. This is the single largest
    piece of trusted-but-unverified material in the entire audit, and it
    applies to BOTH verification paths equally.

    Comparator's own README acknowledges this explicitly:
        "running `lake exe cache get` to download a Mathlib cache is
         acceptable before running the comparator if you trust the cache
         to not be modified as to, e.g. contain different definitions from
         the one you would expect."
    That trust was extended here. It was not independently verified.

COMPILED LOCALLY:
    ConnesRigidity.olean (61,174,904 bytes) — established as locally
    compiled by direct observation BEFORE the build: a search of
    .lake/build for ConnesRigidity* returned nothing after `cache get`
    and before `lake build`. ConnesRigidity is not a Mathlib module and
    has no cache entry. The build then consumed 623 s user CPU and
    10.34 GiB peak RSS.

    ComparatorChallenges.E_ConnesRigidity — replayed as above.

    comparator and lean4export binaries — built locally from the pinned
    revisions (25 jobs, exit 0).

================================================================
3. WHICH KERNEL(S) WERE USED?
================================================================
BOTH. `enable_nanoda: true` in the repository's own configuration:
  - the Lean kernel (via Lean4Checker replay, pinned b7398199245524...)
  - the nanoda kernel (independent Rust implementation)

This matters for the trust basis: it reduces assumption 5 of Comparator's
stated contract from "the Lean kernel is correct" to "the Lean kernel OR
the nanoda kernel is correct".

================================================================
4. THE SANDBOX WAS DISABLED. THIS IS THE CENTRAL CAVEAT.
================================================================
The passing run (exit 0) used COMPARATOR_LANDRUN pointed at
Comparator's own scripts/fake-landrun.sh, which self-describes as:

    "insecure and vibesick landrun shim that doesn't sandbox
     don't use if you want any security obviously"

and which printed, on every child process:

    "WARNING: THIS IS NOT REAL LANDRUN! UNSAFELY RUNNING exec ..."

WHY: the real landrun run (exit 1) failed with
    uncaught exception: unknown module prefix 'Nat'
    No directory 'Nat' or file 'Nat.olean' in the search path

DIAGNOSIS — a genuine incompatibility, not misconfiguration:
  - lean4export's CLI is `<imports...> -- <constants...>` (Main.lean:
    `let (imports, constants) := args.span (· != "--")`).
  - Comparator constructs exactly that (Main.lean:138-139:
    `let baseArgs := #[module.toString, "--"]` then folds the decls on).
  - Invoked directly with that argument order, lean4export WORKS — it
    emitted valid export JSON (verified in this audit).
  - Under the fake shim, the exec line is visible and the `--` IS present:
      lean4export ComparatorChallenges.E_ConnesRigidity -- Nat String ...
    and the run succeeds.
  - Under real landrun v0.1.18 the same invocation fails with `Nat` being
    treated as an IMPORT — i.e. the `--` separator did not survive.

  CONCLUSION: landrun v0.1.18 consumes the `--` separator before passing
  the command line to the child, breaking Comparator's lean4export
  invocation. The fault is in an EXTERNAL, UNPINNED dependency: the
  Comparator README instructs installing landrun "compiled from the `main`
  branch's source" — a moving branch, which has drifted away from what
  Comparator v4.32.0 expects.

  Classified as DEPENDENCY/TOOLING failure. It is NOT a defect in
  ConnesRigidity.lean, in the repository's pinned dependency set, or in the
  audited mathematics.

================================================================
5. WHAT THE DISABLED SANDBOX DOES AND DOES NOT WEAKEN
================================================================
Comparator's README states its guarantee under six assumptions. THIS RUN
DOES NOT SATISFY THREE OF THEM:

  #2 "You have not previously tried to compile the Solution file"
     NOT MET. Stage 4 built ConnesRigidity.lean, as the audit prompt
     requires.

  #3/#4 "You have landrun in PATH" / "landrun works correctly on your
     system" — NOT MET. The shim was used; no sandboxing occurred.

  #6 "You are not running this under a privileged user"
     NOT MET. The run was as root. A non-root run was attempted and
     abandoned: `lake env` as an unprivileged user attempted to DELETE AND
     RE-CLONE the Comparator package ("URL has changed; deleting ... and
     cloning again"), which would have mutated the audited build tree.
     Only read-only permissions prevented it. Preserving the pinned tree
     was judged more important than satisfying an assumption aimed at a
     threat model that does not apply here.

WHAT IS THEREFORE NOT DEMONSTRATED:
  Comparator's full end-to-end adversarial guarantee. That guarantee is
  designed for a setting where an untrusted party submits Solution.lean and
  might try to compromise the Challenge during compilation. This audit is
  not that setting: it checks a published artifact.

WHAT REMAINS SUPPORTED, AND WHY:
  The sandbox isolates the COMPILE step. The three substantive checks —
  statement equality against the challenge, axiom-whitelist conformance,
  and kernel acceptance — are performed on EXPORTED PROOF TERMS after that
  step, by Lean4Checker and by nanoda. Nothing about running the compile
  unsandboxed alters what those checkers read or whether they accept it.
  A hostile solution could have exploited the missing sandbox to corrupt
  the challenge; the OpenAI-published artifact under audit is not a hostile
  submission, and no such tampering was observed (the challenge module's
  own hash and the whole worktree remained clean throughout).

================================================================
6. NET ASSESSMENT OF THE TWO PATHS' RELATIVE STRENGTH
================================================================
The plan for this audit deliberately declined to call the Comparator path
"strictly stronger" until this file could be written. With it written:

  Comparator adds, beyond the plain build:
    + statement equality against an independently-stated challenge
    + enforcement (not merely reporting) of an axiom whitelist
    + re-checking of exported proof terms by a SECOND kernel (nanoda)

  Comparator does NOT remove:
    - trust in the 8,639 downloaded Mathlib .olean artifacts
    - trust in lean4export's fidelity (it is in the trust base of path (b)
      and not of path (a))

  And in this run it additionally forfeits its sandbox guarantee.

  So the two paths remain COMPLEMENTARY, as planned. Path (b) is
  independent corroboration of the axiom and statement questions by a
  second kernel; it is not a superset of path (a), and neither substitutes
  for the other. Both are reported separately in RESULTS.md with their own
  exit statuses.
