Third review: fix integrality mechanism, scope the SpanFull equivalence, three doc gaps

Author: SuvirRathore

CAPABILITY_LOG.md

@@ -125,3 +125,56 @@ monodromy-group paper.
 **Unchanged.** The W30 candidate remains "Frobenius elements exist in the
 absolute Galois group": genuinely missing, self-contained, and a plausible
 Mathlib PR.
+
+## 11-08-2026 — third independent review
+
+Run against the repaired state, with the round-1 and round-2 transcripts withheld
+to avoid anchoring on the same questions.
+
+**Verdict.** No false content, no vacuity, no code/documentation drift. All five
+proved lemmas re-derived and their Mathlib dependencies checked against v4.28.0
+source. The `sorry`'d statement judged a faithful, satisfiable, honestly-scoped
+rendering of Lafforgue's companion theorem for the affine curve, neither stronger
+nor weaker than the literature package. Non-degenerate satisfiability exhibited:
+`A = 𝔽_q[t]`, `ρ₀` the 2-dimensional representation of an `S₃`-cover.
+
+**Corrected.** Two prose overclaims. The integrality remark attributed unit-ness
+of the Frobenius roots to purity; it is instead part (c) of Deligne's Conjecture
+1.2.10, proved for curves by Lafforgue VII.6, and is a conclusion separate from
+the weight condition — Drinfeld's own `Γ^mix` versus `Γ^mot` distinction makes
+this explicit, and `(3+4i)/5` is a one-line witness that purity does not imply
+integrality. The `SpanFull` docstring stated the Burnside equivalence without its
+scope: it needs `R` a field and `m ≥ 1`, both of which hold at every use site but
+neither of which was said. Three cosmetic gaps also closed.
+
+**A claim of ours that was wrong.** We had reasoned that continuity of a
+representation of `G_K` into `GL_n(E_λ)` forces unramifiedness at almost all
+places. False for `n ≥ 2`. Compactness gives a stable lattice and hence a finite
+ramification set at each finite level, but the level-wise sets need not stabilise:
+a Kummer class built from `b_m = ∏_{i≤m} π_i^{ℓ^i}` gives a continuous
+upper-triangular `ρ = (χ_ℓ, c; 0, 1) : G_K → GL₂(ℤ_ℓ)` ramified at every `v_i`.
+Ramakrishna, *Infinitely ramified Galois representations*, Ann. of Math. 151
+(2000), shows even full image is compatible with infinite ramification;
+Khare–Rajan, IMRN 2001 no. 12, show the ramified set has density zero but can be
+infinite. True for `n = 1`, where the torsion of `1 + 𝔪` is finite and class field
+theory closes the argument. This is why "finitely ramified" is an explicit
+condition in Fontaine–Mazur rather than a consequence of continuity, and it means
+`hunram` is load-bearing rather than a convenience.
+
+**Mathlib survey additions (v4.28.0).**
+- `IsArithFrobAt.exists_of_isInvariant` fails at the infinite level on three
+  counts, not one: finite residue field, `[Finite G]`, and
+  `[Algebra.IsInvariant R S G]`.
+- `isPretransitive_of_isGaloisGroup` requires `[Finite G] [IsGaloisGroup G A B]`,
+  so transitivity of the action on primes above `v` is unavailable here.
+- Chebotarev density is absent from Mathlib entirely.
+- `Ideal.inertia G Q = {g | ∀ x, g • x - x ∈ Q}`; since `C ⧸ Q` is integral over
+  the field `A ⧸ v` it is a field and equals the residue field of the
+  corresponding place of `K̄`, so this is literally the classical inertia group,
+  and membership already forces stabilisation of `Q` — no decomposition-group
+  clause is needed.
+
+**Not verifiable by review.** Compile status and the axiom audit are attested, not
+reproduced; an instance diamond on the supplied `MulSemiringAction` can only be
+excluded by a build. Lafforgue VII.6 and Deligne 1.2.10 were checked through
+Drinfeld's verbatim quotations, not the paywalled originals.

LambdaAdicSlice/Basic.lean

@@ -207,10 +207,12 @@ variable (A K Kbar : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
 /-- A choice of Frobenius element at every finite place.
 
 Existence of Frobenius elements in the *absolute* Galois group is not available
-in Mathlib v4.28.0: `IsArithFrobAt.exists_of_isInvariant` requires a finite
-residue field at the chosen prime, which fails at `K̄`. Proving it needs the
-surjectivity of the decomposition group onto the residue Galois group together
-with an inverse-limit or Zorn argument over finite subextensions.
+in Mathlib v4.28.0. `IsArithFrobAt.exists_of_isInvariant` fails at `K̄` on three
+counts, not one: it requires a finite residue field at the chosen prime (at `K̄`
+that field is the algebraic closure of `A/v`), a finite acting group, and
+`Algebra.IsInvariant`. Proving existence needs the surjectivity of the
+decomposition group onto the residue Galois group together with an
+inverse-limit or Zorn argument over finite subextensions.
 
 Taking it as data rather than deriving it makes the assumption explicit and
 removes the vacuity that an unquantified `IsFrobAt v g → ...` would introduce.
@@ -290,15 +292,23 @@ section AbsoluteConditions
 
 /-- The image of `ρ` spans the full matrix algebra.
 
-This is **absolute irreducibility**, stated with no algebraic closure anywhere.
-The image contains `1` and is closed under multiplication, so its `R`-linear span
-is already an `R`-subalgebra. If that span is all of `M_m(R)` then it stays so
+For `R` a **field** and `m ≥ 1` this is **absolute irreducibility**, stated with
+no algebraic closure anywhere. The image contains `1` and is closed under
+multiplication, so its `R`-linear span is already an `R`-subalgebra. If that
+span is all of `M_m(R)` then it stays so
 after any scalar extension, hence there is no proper nonzero invariant subspace
 over any extension. Conversely, if `ρ` is absolutely irreducible then Burnside's
 theorem over an algebraic closure `R̄` gives a span of dimension `m ^ 2`, and the
 span over `R̄` is `R̄ ⊗ (span over R)`, so the span over `R` already has dimension
 `m ^ 2`.
 
+Both scope conditions hold at every use site: the coefficient rings are `E_λ`
+and a finite extension `M` of it, and `exists_companion` assumes `0 < n`. Outside
+that scope the reading degrades — at `m = 0` the predicate holds trivially while
+irreducibility fails, and over a general `CommRing` the equivalence is not
+well-posed. The definition is stated at `CommRing` generality because nothing
+below needs more.
+
 The equivalence is not formalised; it is what justifies the choice of predicate. -/
 def SpanFull {G R : Type*} [Monoid G] [CommRing R] {m : ℕ}
     (rho : G →* GL (Fin m) R) : Prop :=

README.md

@@ -42,6 +42,11 @@ with determinant of finite order.
 Stated one place `λ` at a time. A family indexed by all `λ` follows by choice and
 carries the same existence content.
 
+`M` carries the `E_λ`-module topology (`IsModuleTopology`), not an arbitrary one;
+that is what makes "continuous" well-posed. For a finite extension of the
+complete field `E_λ` it is the canonical valuation topology, so the degenerate
+reading — indiscrete topology, every map continuous — is excluded.
+
 ## What is proved
 
 - `charpoly_eq_of_isConj_gl`, `charpoly_eq_of_isConj` — the characteristic
@@ -92,13 +97,21 @@ no topology, and applies unchanged to the companion over `M`.
   Drinfeld's Lemma 2.7 (arXiv:1007.4004) is an elementary Brauer-group argument:
   a semisimple representation of dimension `r` over an algebraic closure of `E_λ`
   whose character is defined over `E_λ` descends to any extension whose degree is
-  divisible by each of `r, r-1, …, 2`. The companion's characteristic polynomials
-  lie in `E ⊆ E_λ` and it is irreducible, so `[M : E_λ] = n!` suffices. Not stated
-  in the Lean: it sharpens nothing the slice needs.
+  divisible by each of `r, r-1, …, 2`. Its hypothesis is met here: the companion
+  is irreducible, hence semisimple, and its character is defined over `E_λ`
+  because the Frobenius traces lie in `E ⊆ E_λ`, the Frobenii are dense by
+  Chebotarev in the quotient through which the companion factors, the trace is
+  continuous, and `E_λ` is closed in `M`. So `[M : E_λ] = n!` suffices. Not
+  stated in the Lean: it sharpens nothing the slice needs.
 - **Integrality.** Drinfeld's Theorem 1.1 carries a hypothesis that the roots of
-  the characteristic polynomials are `λ`-adic units. Here that is a *consequence*
-  of absolute irreducibility and finite-order determinant, via purity, not an
-  extra assumption. Nothing has been dropped relative to Theorem 1.1.
+  the characteristic polynomials are `λ`-adic units. For curves that is a
+  *consequence* of absolute irreducibility and finite-order determinant, not an
+  extra assumption, so nothing has been dropped — but the mechanism is not
+  purity. Being a unit away from `p` is part (c) of Deligne's Conjecture 1.2.10,
+  a conclusion separate from the weight condition, and for curves it is part of
+  what Lafforgue's Théorème VII.6 proves. Purity is the archimedean statement and
+  does not imply integrality: `(3 + 4i)/5` has absolute value `1` at every
+  archimedean place and is not a `5`-adic unit.
 - **At `λ₀`.** One may take `M = E_{λ₀}` and `ρ = ρ₀`, so `ρ₀` is itself one of
   the companions. No separate clause asserting this is needed, and none is
   stated: once the coefficient field varies, an equality `ρ_{λ₀} = ρ₀` is
@@ -107,9 +120,10 @@ no topology, and applies unchanged to the companion over `M`.
 ## Limitations — deliberately out of scope
 
 - **Frobenius existence is assumed, not proved.** `FrobeniusChoice` takes it as
-  data. Mathlib's `exists_of_isInvariant` requires a finite residue field at the
-  chosen prime; at `K̄` that residue field is the algebraic closure of `A/v`, so
-  the proof does not transfer. Proving it needs surjectivity of the decomposition
+  data. Mathlib's `exists_of_isInvariant` fails here on three counts, not one: it
+  requires a finite residue field at the chosen prime (at `K̄` that field is the
+  algebraic closure of `A/v`), a finite acting group, and `Algebra.IsInvariant`.
+  Proving existence needs surjectivity of the decomposition
   group onto the residue Galois group plus an inverse-limit or Zorn argument over
   finite subextensions. The *definition* of arithmetic Frobenius transfers to the
   infinite level; the existence *proof* does not. Every result mentioning
@@ -177,6 +191,12 @@ construction; and that the first round's fixes had been applied to the code but
 not to the documentation, leaving a docstring that reasserted the rejected
 well-definedness claim and cited an axiom that had been deleted.
 
+A third review, run against the repaired state with the two earlier reviews
+withheld, found no false or vacuous content and no drift between code and
+documentation. It found two prose overclaims — a misattributed mechanism in the
+integrality remark, and an equivalence stated without the scope conditions it
+needs — both corrected above.
+
 Further review is welcome — see `CAPABILITY_LOG.md`.
 
 ## Future work