PHASE 7 — SOURCE-LEVEL STRUCTURE AUDIT
Captured: 2026-08-06
Target: ConnesRigidity.lean @ 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6
SHA-256: 31f6c419f341ee6aa5b03bc15800a9d8ee2c654c344aab90bdef0639353ccc91
37,374 lines / 2,369 top-level declarations

Method: static source inspection with line-numbered extraction. The source
was NOT modified. This section is source structure only; it is not a kernel
check and makes no claim about correctness.

================================================================
IDENTIFIER MAP — DECLARATION SITES
================================================================
LINE    IDENTIFIER                                      KIND
662     V := Fin 4 → R                                  abbrev
676     T := TensorProduct F V V                        abbrev
680     B : Submodule F T := Submodule.span F            def
          (Set.range square)
682     D := V × B                                      abbrev
875     K := KSubgroup                                  abbrev
1399    actingGroup_hasKazhdanPropertyT                 theorem
10572   shiftedCarry (n) (l l' : X) : Y                 def
10597   CarryGroup (_n : ℕ)                             structure
11407   E (n : ℕ)                                       abbrev
12258   shiftedCarry_self_eq_evaluate_d                 theorem
13591   kLinear : K →* (V ≃ₗ[F] V)                       def
13610   kTensorLinear : K →* (T ≃ₗ[F] T)                 def
13639   kDividedSquareLinear : K →* (B ≃ₗ[F] B)          def
13678   kDAction : K →* MulAut (Multiplicative D)        def
13696   Lambda := SemidirectProduct                      abbrev
          (Multiplicative D) K kDAction
13700   lambdaGroup : CountableDiscreteGroup             def
13967   kYLinear_shiftedCarry                           theorem
14048   kEAction (n) : K →* MulAut (Multiplicative (E n)) def
14063   Gamma (n) := SemidirectProduct                   abbrev
          (Multiplicative (E n)) K (kEAction n)
14069   gammaGroup (n) : CountableDiscreteGroup          def
29813   suslinRelativeElementaryGeneration               theorem
31550   k_D_orbit_infinite                              theorem
31610   semidirect_isICC                                theorem
31697   kEAddAction_orbit_infinite_of_exact             theorem
31821   gamma_isICC (n) : IsICC (gammaGroup n)          theorem
34935   gamma_hasKazhdanPropertyT_unconditional (n)     theorem
36493   lambda_isICC_of_infinite_module_orbits          theorem
36520   lambda_isICC_of_module_orbits                   theorem
36526   lambda_isICC : IsICC lambdaGroup                theorem
36684   lambda_hasKazhdanPropertyT_unconditional        theorem
36712   paper_factors_isomorphic (n)                    theorem
36941   paperAnalyticInput : PaperAnalyticInput         theorem
36954   exists_nonisomorphic_propertyT_icc_groups_      theorem  <-- FINAL (A)
          with_isomorphic_factors
37347   exists_infinite_pairwise_nonisomorphic_         theorem  <-- FINAL (B)
          propertyT_icc_groups_with_isomorphic_factors

IDENTIFIER-DRIFT NOTES (audit prompt named these; actual names differ):
  - "gamma property-(T) theorem"  -> gamma_hasKazhdanPropertyT_unconditional (34935)
  - "kEAddAction_orbit_infinite_of_exact" -> present verbatim (31697)
  - "suslinRelativeElementaryGeneration"  -> present verbatim (29813), plus
    three named variants at 9562, 9583, 9605
    (..._of_maximal_away_powered_increments,
     ..._of_maximal_local_powered_increments,
     ..._of_maximal_local_elementary)
  - "lambda_isICC" / "gamma_isICC" -> present verbatim, but stated about
    lambdaGroup / gammaGroup rather than Lambda / Gamma. See Q5 below —
    this is a packaging distinction, not a different object.

================================================================
THE SEVEN EXPLICIT PHASE-7 SOURCE QUESTIONS
================================================================

Q1. Are the final groups syntactically defined using Mathlib
    `SemidirectProduct`?

    YES — directly and syntactically.

      13696:  abbrev Lambda := SemidirectProduct (Multiplicative D) K kDAction
      14063:  abbrev Gamma (n : ℕ) :=
                SemidirectProduct (Multiplicative (E n)) K (kEAction n)

    `SemidirectProduct` occurs 225 times in the file. The countability
    instances are derived through Mathlib's own
    `SemidirectProduct.equivProd.injective.countable`.

Q2. Where does `shiftedCarry` enter?

    Declared at line 10572:
        def shiftedCarry (n : ℕ) (l l' : X) : Y

    Its primary structural role is as the 2-COCYCLE DEFINING THE GROUP LAW
    of the internal abelian extension `CarryGroup n` (structure at 10597):

        10618:  x.quadratic + y.quadratic + shiftedCarry n x.linear y.linear
                  (the addition)
        10621:  neg x := <x.linear, x.quadratic + shiftedCarry n x.linear x.linear>
                  (the negation)

    Supporting algebraic facts: shiftedCarry_zero_left/right (10575/10579),
    _comm (10583), _add_left (10587), _add_right (10592),
    _self_eq_evaluate_d (12258). Topological continuity lemmas at
    11314-11400 and 12581-12662. Equivariance at 13967.

Q3. Does `shiftedCarry` appear in the definition of the K-action on B?

    NO. The body of `kDividedSquareLinear` (13639) was read in full:

        def kDividedSquareLinear : K →* (B ≃ₗ[F] B) where
          toFun k := (kTensorLinear k).ofSubmodules B B (kTensorLinear_map_B k)
          ...

    There is no occurrence of `shiftedCarry` in that definition, nor in
    `kDAction` (13678), which is built from `kDLinear` via
    `AddEquiv.toMultiplicative`.

Q4. Is the action on B instead inherited from the tensor/divided-square
    action?

    YES. `kDividedSquareLinear` is literally the restriction of
    `kTensorLinear : K →* (T ≃ₗ[F] T)` to the submodule
    `B := Submodule.span F (Set.range square) ⊆ T`, via
    `.ofSubmodules B B (kTensorLinear_map_B k)` — i.e. the action on B is
    the tensor action, restricted, with `kTensorLinear_map_B` supplying the
    proof that B is invariant. Confirmed by the simp lemma at 13653:
        (kDividedSquareLinear k b : T) = kTensorLinear k (b : T)   := rfl

    The relationship between shiftedCarry and the K-action is stated
    separately as an EQUIVARIANCE lemma, not a definition (13967):
        kYLinear k (shiftedCarry n l l') =
          shiftedCarry n (kXLinear k l) (kXLinear k l')

Q5. Does the ICC theorem apply to the exact final group definitions?

    YES. `lambda_isICC` and `gamma_isICC` are stated about `lambdaGroup`
    and `gammaGroup n`, which are the CountableDiscreteGroup packagings of
    exactly `Lambda` and `Gamma n`:

        13700:  def lambdaGroup : CountableDiscreteGroup where
                  Carrier := Lambda
                  group := inferInstance
                  countable := inferInstance

        14069:  def gammaGroup (n : ℕ) : CountableDiscreteGroup where
                  Carrier := Gamma n
                  group := inferInstance
                  countable := inferInstance

    The Carrier fields are `Lambda` and `Gamma n` themselves — the
    top-level semidirect products of Q1, not the internal `CarryGroup`
    abelian construction. The audit prompt's specific caution — do not
    infer that an internal central subgroup is central in the final
    semidirect product without proving the acting group fixes it — is
    therefore not triggered at the level of WHICH OBJECT the ICC theorems
    are about: they are about the final objects. Whether their PROOFS are
    correct is a kernel question, answered by the build and by
    #print axioms, not by this static reading.

Q6. Does the final theorem have unresolved hypotheses?

    NO. Both final theorems are closed existential statements taking no
    hypotheses:

    (A) 36954  exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors
        ∃ Γ Λ : CountableDiscreteGroup.{0},
          Group.FG Γ ∧ Group.FG Λ ∧ IsICC Γ ∧ HasKazhdanPropertyT Γ ∧
          IsICC Λ ∧ HasKazhdanPropertyT Λ ∧
          TracialGroupFactorsIsomorphic Γ Λ ∧ ¬GroupsIsomorphic Γ Λ

    (B) 37347  exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_
               with_isomorphic_factors
        ∃ (Λ) (Γ : ℕ → CountableDiscreteGroup.{0}), ... pairwise
          non-isomorphic, all with isomorphic tracial factors ...

    Both match the CHALLENGE statements in
    ComparatorChallenges/E_ConnesRigidity.lean (verbatim modulo namespace
    qualification). Neither carries a side condition, a `variable`
    hypothesis, or an unproven parameter.

    RELATIONSHIP BETWEEN THE TWO — this resolves the audit prompt's
    theorem-name divergence:

      Both are proved from a single common construction,
      `manuscriptInfinitePropertyTFiber`:

        (A) refine <F.Gamma 0, F.Lambda, F.gamma_fg 0, F.lambda_fg,
              F.gamma_icc 0, F.gamma_propertyT 0, F.lambda_icc,
              F.lambda_propertyT, F.factors_isomorphic 0, ?_>

        (B) refine <F.Lambda, F.Gamma, F.lambda_fg, F.gamma_fg,
              F.lambda_icc, F.gamma_icc, F.lambda_propertyT,
              F.gamma_propertyT, F.factors_isomorphic, ?_, ?_,
              F.lambda_not_isomorphic>

      So (A) is NOT an intermediate lemma feeding (B), and (B) is not a
      later strengthening built on (A). They are SIBLING top-level results
      instantiating the same fiber — (A) at the single index 0, (B) over
      all of ℕ. The audit prompt's checkpoint name (A) is a genuine final
      theorem of the development, and so is (B). Both are listed in
      ComparatorChallenges/E_ConnesRigidity.json for checking.

Q7. What does Lean report as the axiom dependency set of the final theorem?

    NOT ANSWERABLE BY SOURCE INSPECTION. See print_axioms.log for Lean's
    own answer via #print axioms, and comparator.log for the independent
    check against the permitted_axioms whitelist. The static searches in
    source_searches.txt do NOT answer this question and are not offered as
    doing so.

================================================================
LIMITS OF THIS SECTION
================================================================
Everything above is static source structure: what is declared, where, and
in terms of what. It establishes WHICH objects the theorems are about and
that the statements are closed. It does NOT establish that any proof is
correct — that is what the Lean kernel and Comparator are for, and their
results are recorded separately.
