PHASE 5b — AXIOM WHITELIST AND RESULT

================================================================
WHITELIST AS CONFIGURED BY THE REPOSITORY
================================================================
From ComparatorChallenges/E_ConnesRigidity.json
(SHA-256 ca2bdd2752cc9839a63d8d5217408c1ae934eb0c93dc241580a18bf16fd36f6c,
 git blob f5d2964be6b1a154bc12b38a0f99f0960960a2d9):

    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]

Three axioms. These are the standard axioms of Lean 4's logical foundation.
Notably ABSENT from the whitelist: sorryAx, and any bespoke axiom.

================================================================
RESULT
================================================================
PASS — Comparator exited 0 with this whitelist in force.

Comparator's documented contract is that, on success, every theorem in the
solution listed in `theorem_names` "use[s] no more axioms than listed in
permitted_axioms". Exit status 0 with `enable_nanoda: true` therefore
constitutes the checker's assertion that both target theorems stay inside
that three-axiom budget.

The constants Comparator exported from the solution module, observed
directly in the run output, were:

    Nat, String, String.mk, Char, Char.ofNat, List,
    Quot, Quot.mk, Quot.lift, Quot.ind,
    ConnesRigidity.exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors,
    ConnesRigidity.exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors,
    propext, Quot.sound, Classical.choice,
    Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod,
    Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor,
    Nat.shiftLeft, Nat.shiftRight, String.ofList

The only axioms in that set are exactly propext, Quot.sound, and
Classical.choice. The remainder are the target theorems themselves plus the
core arithmetic/string constants the export format requires.

================================================================
CROSS-CHECK AGAINST THE OTHER TWO SOURCES
================================================================
Three independent statements about the axiom set now agree:

  1. formalization.yaml (VENDOR SELF-REPORT)
     axioms: propext, Classical.choice, Quot.sound;  sorry_count: 0

  2. Lean's own #print axioms (MACHINE-CHECKED, this audit)
     both final theorems -> [propext, Classical.choice, Quot.sound]
     ...and 11 supporting declarations, all identical.
     See print_axioms.log.

  3. Comparator + nanoda (INDEPENDENT KERNEL, this audit)
     exit 0 against the three-axiom whitelist.
     See comparator.log.

(1) was a claim. (2) and (3) are measurements, and they were obtained by
different mechanisms: (2) reads the environment produced by the elaborating
Lean; (3) re-checks exported proof terms through the Lean kernel replay AND
through nanoda, a separate Rust implementation of the Lean kernel.

sorryAx does not appear in any of them. In Lean, a declaration whose proof
contains `sorry` anywhere in its transitive dependency graph carries sorryAx
in #print axioms. Its absence is machine-checked evidence of no unproven
placeholder — evidence of a kind that no text search could produce.
