PHASE 3 — REPOSITORY BUILD CONTRACT
Captured: 2026-08-06
Derived from the pinned worktree at commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6

================================================================
SOURCES OF THE CONTRACT
================================================================
The audit prompt directs deriving the build command from the repository,
preferring "the environment best supported by the repository's actual
configuration and CI files."

FINDING: The repository contains NO .github/ directory.

Recorded precisely: there is no GitHub Actions workflow or other
GitHub-specific CI configuration in this repository. This is NOT a statement
that the repository lacks a build contract, and it has no bearing on the
availability of the `git` executable (git 2.53.0 is present in the WSL2
distribution — see environment.txt).

The contract is therefore derived from, in order of authority:

  1. README.md                                  (explicit build instructions)
  2. lean-toolchain                             (pinned compiler)
  3. lakefile.toml                              (targets and dependencies)
  4. lake-manifest.json                         (pinned dependency revisions)
  5. formalization.yaml                         (declared results and axioms)
  6. ComparatorChallenges/README.md             (independent-checking path)
  7. ComparatorChallenges/E_ConnesRigidity.json (checker configuration)

================================================================
PINNED TOOLCHAIN
================================================================
lean-toolchain contents : leanprover/lean4:v4.32.0

Installed via elan (elan 4.2.3), which read lean-toolchain and installed
exactly that toolchain. No Lean version was chosen by the auditor.

Verified in the pinned worktree:
    lake  --version -> Lake version 5.0.0-src+8c9756b (Lean version 4.32.0)
    lean  --version -> Lean (version 4.32.0, x86_64-unknown-linux-gnu,
                             commit 8c9756b28d64dab099da31a4c09229a9e6a2ef35,
                             Release)
    elan toolchain list -> leanprover/lean4:v4.32.0

git status --porcelain=v1 after toolchain installation: EMPTY (clean).

================================================================
README.md — VERBATIM BUILD INSTRUCTIONS
================================================================
    The project uses Lean 4.32.0, mathlib, and Lake. With elan installed,
    fetch the mathlib cache and build all ten formalizations with:

        lake exe cache get
        lake build All

    To build an individual formalization, pass its module name to Lake:

        lake build SpherePacking

================================================================
COMMAND SELECTED FOR THIS AUDIT, AND WHY
================================================================
    lake exe cache get
    lake build ConnesRigidity

RATIONALE:

  `lake build All` is NOT used. The README offers it as the convenience
  command for building all ten formalizations, but the audited target is one
  file. All.lean pulls in every formalization in the repository — roughly
  21 MB of Lean source across ten files, including GapCVP.lean (5,335,203 B)
  and MetricCodes.lean (4,531,268 B), none of which is under audit. Building
  them would consume hours of wall-clock and would not strengthen any claim
  about ConnesRigidity.lean.

  `lake build ConnesRigidity` is the narrowest repository-supported target.
  It is not an invented command: lakefile.toml declares

      [[lean_lib]]
      name = "ConnesRigidity"

  and lists "ConnesRigidity" in defaultTargets. The README explicitly
  sanctions `lake build <ModuleName>` for an individual formalization.

  `lake exe cache get` is a DOWNLOAD of prebuilt Mathlib .olean artifacts,
  not a build. It is labelled as such wherever it appears in this audit. A
  successful cache fetch is not evidence that anything was compiled or
  kernel-checked locally.

================================================================
lakefile.toml — RELEVANT CONTENTS
================================================================
name = "ten-proofs", version = "0.1.0"

[[require]] mathlib     scope=leanprover-community  rev=v4.32.0
[[require]] Comparator  git=https://github.com/leanprover/comparator.git rev=v4.32.0

[[lean_lib]] name = "ConnesRigidity"      <- the audited target
[[lean_lib]] name = "ComparatorChallenges" (12 explicit roots, including
                                            ComparatorChallenges.E_ConnesRigidity)

IMPORTANT: lakefile.toml declares NO leanOptions, NO moreLeanArgs, and NO
maxHeartbeats override. ConnesRigidity.lean is therefore elaborated under
Lean's DEFAULT resource limits. Given the file is 1,449,151 bytes / 37,374
lines and a single Lean file is elaborated by a single process (build
parallelism does not divide it), default limits are the principal technical
risk in this audit.

Also note: because lakefile.toml declares glob/root-based lean_lib targets,
the #print axioms harness is written OUTSIDE the repository tree so that it
cannot be absorbed as a build target.

================================================================
lake-manifest.json — PINNED DEPENDENCY REVISIONS
================================================================
mathlib          leanprover-community/mathlib4      81a5d257c8e410db227a6665ed08f64fea08e997  (inputRev v4.32.0)
Comparator       leanprover/comparator.git          07bc4ea40f2266dcb861820a2ec1fa3244ed307f  (inputRev v4.32.0)
lean4export      leanprover/lean4export             4e7915201d3f9f04470d9eae002fa695f7cdc589  (inputRev master)
Lean4Checker     leanprover/lean4checker            b7398199245524275543dec6113229c9bb4902e5  (pinned by sha)
plausible        leanprover-community/plausible     e12c1910fe855cbfc38803cd4e55543906d5fa62
LeanSearchClient leanprover-community/LeanSearchClient c5d5b8fe6e5158def25cd28eb94e4141ad97c843
importGraph      leanprover-community/import-graph  7e9612bf0b9ee66db3cb5b9988a35afc706f5a12
proofwidgets     leanprover-community/ProofWidgets4 6e311e2a844da9b2cc3971187df2fe0066947b93
aesop            leanprover-community/aesop         a7dbf0c63b694e47f425f3dcddbc0e178bb432d3
Qq               leanprover-community/quote4        38d591e778f100aec9762bb582f9c7f55f50e9dc
batteries        leanprover-community/batteries     023ce7d62a0531e22a5331e20b587817a80d49ff
Cli              leanprover/lean4-cli               88679d088c9720c27ebdf2ba4dafe17341747f94  (inputRev v4.32.0)

`lake update` is NEVER run. Only `lake exe cache get` and `lake build`.
Dependency fetch was observed resolving Comparator to 07bc4ea4... and mathlib
to 81a5d257..., matching the manifest exactly.

================================================================
INDEPENDENT-CHECKING PATH (ComparatorChallenges/README.md, verbatim)
================================================================
    Install `landrun`, `lean4export`, and `nanoda_bin`, and make them
    available on `PATH`. Then, from the repository root:

        lake exe cache get
        lake exe comparator ComparatorChallenges/A_SpherePacking.json

    Replace `A_SpherePacking.json` with any other challenge configuration in
    this directory.

For this audit the invocation is:

    lake exe comparator ComparatorChallenges/E_ConnesRigidity.json

PREREQUISITES not present by default and requiring installation:
    landrun     — Linux Landlock-LSM sandbox (Linux-only; this is the reason
                  native Windows cannot execute this path at all)
    lean4export — pinned as a Lake dependency (4e7915201d...)
    nanoda_bin  — independent Rust implementation of the Lean kernel

================================================================
CRITICAL READING NOTE — `sorry` IN THE CHALLENGE FILE
================================================================
ComparatorChallenges/E_ConnesRigidity.lean CONTAINS THE TOKEN `sorry` TWICE.

This is BY DESIGN and is NOT a hole in the audited proof.

E_ConnesRigidity.lean is the CHALLENGE file: a statement-only specification.
It declares the definitions (CountableDiscreteGroup, IsICC,
HasKazhdanPropertyT, GroupVonNeumannAlgebra, canonicalTrace,
TracialGroupFactorsIsomorphic, ...) and then states the two theorems with
`:= by sorry` bodies, because the challenge's role is to fix the STATEMENT,
not to prove it. Comparator's function is to verify that the Solution
(ConnesRigidity.lean) proves theorems whose statements match the Challenge's
verbatim, that the Solution uses only permitted axioms, and that the SOLUTION
contains no sorry.

A naive text search for `sorry` across the repository will hit this file.
Reporting that as evidence of an incomplete proof would be a category error.
Recorded here in advance so the Phase 6 source-search results are not
misread. The sorry-count that matters is the one in ConnesRigidity.lean, and
it is established by Lean's own #print axioms (absence of sorryAx) and by
Comparator — not by grep.

================================================================
CHALLENGE STATEMENTS BEING CHECKED (from E_ConnesRigidity.lean)
================================================================
theorem exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors :
    ∃ Γ Λ : CountableDiscreteGroup.{0},
      Group.FG Γ ∧ Group.FG Λ ∧
      IsICC Γ ∧ HasKazhdanPropertyT Γ ∧
      IsICC Λ ∧ HasKazhdanPropertyT Λ ∧
      TracialGroupFactorsIsomorphic Γ Λ ∧
      ¬ GroupsIsomorphic Γ Λ

theorem exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors :
    ∃ (Λ : CountableDiscreteGroup.{0}) (Γ : ℕ → CountableDiscreteGroup.{0}),
      Group.FG Λ ∧ (∀ n, Group.FG (Γ n)) ∧
      IsICC Λ ∧ (∀ n, IsICC (Γ n)) ∧
      HasKazhdanPropertyT Λ ∧ (∀ n, HasKazhdanPropertyT (Γ n)) ∧
      (∀ n, TracialGroupFactorsIsomorphic (Γ n) Λ) ∧
      (∀ m n, TracialGroupFactorsIsomorphic (Γ m) (Γ n)) ∧
      (∀ ⦃m n : ℕ⦄, m ≠ n → ¬ GroupsIsomorphic (Γ m) (Γ n)) ∧
      (∀ n, ¬ GroupsIsomorphic Λ (Γ n))

Both are stated at universe level 0 and both require Group.FG (finite
generation) in addition to ICC and property (T). Recorded verbatim so that
the statement actually checked is on the record, independent of any prose
description of it. No mathematical assessment is offered here.
