PHASE 6 / 7 — STATIC SOURCE SEARCHES
Captured: 2026-08-06
Target: /root/audits/pinned/ConnesRigidity.lean
Revision: 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6
SHA-256: 31f6c419f341ee6aa5b03bc15800a9d8ee2c654c344aab90bdef0639353ccc91

================================================================
METHODOLOGICAL LIMIT — STATED BEFORE THE RESULTS
================================================================
Per audit rule 11: the ABSENCE of the tokens below does NOT prove the
absence of axiom or sorry dependencies. A declaration can depend on sorryAx
transitively through an import without the literal token `sorry` appearing
anywhere in this file.

These searches are STATIC SOURCE INSPECTION ONLY. They are not a kernel
check, not a compilation, and not a dependency analysis. The authoritative
answer to the dependency question comes from Lean's own `#print axioms`
(print_axioms.log) and from the Comparator run (comparator.log). Nothing in
this file is offered as a substitute for either.

================================================================
TOKEN SEARCH — ConnesRigidity.lean
================================================================
Method: grep -c -w -- <token> ConnesRigidity.lean
(-w = whole word, so `sorry` does not match `sorryAx`, `unsafely`, etc.)

    TOKEN              COUNT
    sorry                  0
    sorryAx                0
    admit                  0
    axiom                  0
    unsafe                 0
    opaque                 0
    implemented_by         0
    extern                 0
    native_decl            0
    partial                0

ALL TEN TOKENS ARE ABSENT from ConnesRigidity.lean.

Because every count is zero, the separation the audit prompt requires
(declarations vs comments vs string literals vs imported dependencies vs
harmless terminology) is vacuous FOR THIS FILE: there are no occurrences of
any kind to classify. No occurrence appears in a comment, a string literal,
or a declaration, because no occurrence appears at all.

================================================================
REPOSITORY-WIDE `sorry` SEARCH — AND WHY IT IS NOT WHAT IT LOOKS LIKE
================================================================
Method: grep -rnw --include='*.lean' -e sorry -e sorryAx -e admit
        --exclude-dir=.lake .

RESULT: every single hit is inside ComparatorChallenges/*.lean. There are no
hits in ConnesRigidity.lean or in any of the other nine formalization files.

Hits by file (challenge files only):
    ComparatorChallenges/A_SpherePacking.lean            151, 160, 173, 181
    ComparatorChallenges/B_BinaryCodes.lean              68, 73, 171, 176, 181, 191
    ComparatorChallenges/B_SphericalCodes.lean           143, 273, 284, 292
    ComparatorChallenges/C_PermanentFormulaLowerBound.lean  88, 100
    ComparatorChallenges/D_NonSoficGroup.lean            33
    ComparatorChallenges/E_ConnesRigidity.lean           206, 221
    ComparatorChallenges/F_EhrhartVolumeInequality.lean  50, 54, 59, 74
    ComparatorChallenges/G_QuantumParallelRepetition.lean   128, 135
    ComparatorChallenges/H_GapCVP.lean                   138, 154, 210, 214,
                                                          266, 270, 305, 309
    ComparatorChallenges/I_MulticolorTriangleRamsey.lean 23, 34, 43, 48
    ComparatorChallenges/J_CompactnessConjecture.lean    48
    ComparatorChallenges/J_TwoDegenerateGraphs.lean      41, 45

INTERPRETATION — THIS IS BY DESIGN, NOT A PROOF HOLE:

The ComparatorChallenges/*.lean files are CHALLENGE files: statement-only
specifications. Each declares the definitions needed to state a problem and
then states the target theorems with `:= by sorry` bodies, because the
challenge's role is to FIX THE STATEMENT, not to prove it. Comparator then
verifies that the SOLUTION module proves theorems whose statements match the
CHALLENGE's verbatim, uses only permitted axioms, and contains no sorry.

The pattern holds uniformly across all ten problems, which is itself
evidence that this is the intended architecture rather than an artifact
specific to ConnesRigidity.

The two hits in E_ConnesRigidity.lean (lines 206 and 221) correspond exactly
to the two theorem statements:
    exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors
    exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors

Reporting these as incomplete proofs in the audited development would be a
category error. The sorry-count that matters is the one in the SOLUTION file
ConnesRigidity.lean, which is zero by the token search above and is
established authoritatively by #print axioms (absence of sorryAx) and by
Comparator.

================================================================
FILE SCALE
================================================================
Total declarations in ConnesRigidity.lean
(def / theorem / lemma / abbrev / structure / instance / inductive / class
 at start of line, including noncomputable/private/protected/scoped forms):

    2,369 declarations across 37,374 lines

Recorded for context on the scale of the development and on why a single
Lean file of this size is the principal resource risk in this audit: one
file is elaborated by one process, so build parallelism does not divide it.
