Third-round corrections; sorry-count check in CI

- Lafforgue VII.6(v): the E_lambda descent statement concerns the n-fold
  direct sum of the companion, not its n-th power; the companion's
  finite-order determinant is carried from the construction in the proof
  rather than read off clause (v). Both stated where the theorem is
  identified.
- Module header rewritten: the deleted integral-closure-instance claim was
  still asserted there, and the theorem count predated the family corollary.
- AbsGal and CompanionRep docstrings state their literal scope: the closure
  reading comes from the IsAlgClosure hypothesis the theorems carry.
- Attestation made exact and strengthened: the axiom guard pins axiom-name
  sets, not sorry counts, so a second sorry inside the tainted closure would
  have passed; CI now counts sorry tokens and requires exactly one.
- AUDIT: eq_of_isUnramifiedAt's actual hypotheses (Noetherian +
  Algebra.IsUnramifiedAt, no group); primesOver, not LiesOver, is the
  restated idiom; Representation.IsIrreducible and IsOfFinOrder recorded as
  counterparts; degree-one wording scoped to guaranteed match; note on
  definitions elaborating over a bare CommRing.

Author: SuvirRathore

.github/workflows/build.yml

@@ -23,3 +23,9 @@ jobs:
 
       - name: Check axiom profile
         run: lake env lean Axioms.lean
+
+      - name: Check sorry count
+        run: |
+          count=$( (grep -hE '^[[:space:]]+sorry[[:space:]]*$' LambdaAdicSlice.lean LambdaAdicSlice/*.lean || true) | wc -l )
+          echo "sorry tokens: $count"
+          test "$count" -eq 1

AUDIT.md

@@ -51,11 +51,15 @@ infinite, and every result taking one is then vacuously true.
 counts, not one: a finite residue field at the chosen prime, `[Finite G]`, and
 `[Algebra.IsInvariant R S G]`. Existence of Frobenius elements in the absolute
 Galois group therefore has to be assumed as data. The same file carries a fuller
-finite-level theory: a canonical `arithFrobAt`, conjugacy of the canonical
+finite-level theory: a canonical `arithFrobAt` and conjugacy of the canonical
 Frobenii at primes over one base prime (`isConj_arithFrobAt`, via
-`exists_primesOver_isConj`), and uniqueness under unramifiedness
-(`AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt`), all under the same finiteness and
-invariance hypotheses, so none of it transfers either.
+`exists_primesOver_isConj`), both under the same finiteness and invariance
+hypotheses, and uniqueness under unramifiedness
+(`AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt`), an `AlgHom`-level statement whose
+hypotheses are instead Noetherianity of the extension and `Algebra.IsUnramifiedAt`
+at the prime. None of it transfers: the first two for the group-finiteness
+reasons above, the third because the integral closure in `K̄` is neither
+Noetherian nor unramified there.
 
 `isPretransitive_of_isGaloisGroup` requires `[Finite G]` and
 `[IsGaloisGroup G A B]`, so transitivity of the action on primes above a place is
@@ -100,9 +104,10 @@ trivially satisfiable; a single place leaves the compatibility conditions
 constraining one Frobenius conjugacy class instead of infinitely many. An
 earlier version of this file claimed an explicit cheap witness in the one-place
 case, a companion-matrix representation of the constant-field quotient. That was
-overstated: the construction matches the prescribed polynomial only at a place
-of degree one, since a place of degree `d` sends the generator to the `d`-th
-power of the chosen matrix, and it needs the roots of the polynomial to be units
+overstated: the construction is guaranteed to match the prescribed
+polynomial only at a place of degree one — a place of degree `d` sends the
+generator to the `d`-th power of the chosen matrix, and equality of the
+characteristic polynomials then generally fails — and it needs the roots of the polynomial to be units
 at the target `λ`, which continuity supplies only at `λ₀`. Nor would any witness
 of that shape survive the present conclusion: a representation factoring through
 a procyclic group has image generated by a single matrix `C`, so its span lies
@@ -182,25 +187,38 @@ continuity.
 
 ## What is not machine-checked
 
-Compile status and the axiom profile are checked in CI; see `Axioms.lean` and
-`.github/workflows/build.yml`. The axiom check covers the declarations named
-there and their dependency closures; a `sorry` in a declaration outside those
-would not be caught, since `lake build` exits successfully on the warning it
-emits. No instances are declared on types Mathlib owns, so the diamond an earlier
+Compile status, the axiom profile, and the count of `sorry` tokens are checked in CI; see `Axioms.lean` and
+`.github/workflows/build.yml`. The axiom check pins the set of axiom names in each named declaration's
+dependency closure. On its own that misses two things: a `sorry` in a
+declaration outside those closures, and a second `sorry` inside a closure
+already reporting `sorryAx`, since the set of names does not change; `lake
+build` accepts both with only a warning. CI therefore also counts the `sorry`
+tokens in the source and requires exactly one. No instances are declared on types Mathlib owns, so the diamond an earlier
 version created no longer arises; the five instances declared here are the
 projections of `CompanionRep`, whose carrier is defined here.
 
-Three notions defined here have close Mathlib counterparts that are not used.
+Five notions defined here have close Mathlib counterparts that are not used.
 `LambdaAdicRep` is a `ContinuousMonoidHom`; the recurring conjunction
-`Q.IsPrime ∧ Q.under A = v.asIdeal` restates `Ideal.LiesOver`, the idiom
-`RingTheory/Frobenius.lean` itself uses; and `Field.absoluteGaloisGroup` is the
-fixed-closure form of `AbsGal`. Each is equivalent to what is written, and each would be the better choice in a version aimed at upstreaming. Two further
+`Q.IsPrime ∧ Q.under A = v.asIdeal` is membership in `Ideal.primesOver`, the
+idiom `RingTheory/Frobenius.lean` itself uses, where `Ideal.LiesOver` alone
+records only the contraction equality; `Field.absoluteGaloisGroup` is the
+fixed-closure form of `AbsGal`; `IsIrred` is a matrix presentation of
+`Representation.IsIrreducible`; and `DetFiniteOrderHom` applied to `ρ` says
+`IsOfFinOrder` of the composite of `Matrix.GeneralLinearGroup.det` with `ρ`.
+Each matches what is written over the field-valued, positive-dimension setting
+used here, and each would be the better choice in a version aimed at
+upstreaming. Two further
 items: `IsUnramifiedAt` is hard-wired to representations over `E_λ`, so the same
 inertia condition is written a second time, inline, in the conclusion of
 `exists_companion`, where a version stated for an arbitrary `G →* GL n R` would
-let hypothesis, conclusion and the family corollary share one predicate; and
-`FrobeniusChoice` supplies a lift at every place where only the places outside
-`S` are used.
+let hypothesis, conclusion and the family corollary share one predicate; and `FrobeniusChoice` supplies a lift at every place where only the places
+outside `S` are used. Alongside these, one fact of Lean's elaboration: section
+instance variables enter a definition only when it uses them, so the definitions
+here are stated over a bare commutative ring, and the Dedekind, fraction-field
+and algebraic-closure setting the README fixes binds only in the theorems, which
+include it automatically. The theorems therefore match the README's frame
+exactly; `IsCompatibleFamily`, which no theorem consumes, never regains that
+setting and is that much more general than its prose.
 
 The literature attributions, including Deligne's part-numbering in Weil II and
 the hypotheses and conclusions of Lafforgue's Theorem VII.6, have been checked

Axioms.lean

@@ -1,8 +1,9 @@
 /-
 Machine-checked attestation of the axiom profile. `lake env lean Axioms.lean`
-fails if any proved lemma acquires an axiom dependency, or if the companion
-theorems stop depending on `sorryAx` — that is, if the single deliberate `sorry`
-silently moves or multiplies. Run in CI.
+fails if any proved lemma acquires an axiom dependency or if either companion
+theorem's axiom set changes. It pins the set of axiom names, not the number or
+location of `sorry` terms; the source-level count in CI covers those. Run in
+CI.
 -/
 import LambdaAdicSlice.Companions
 

LambdaAdicSlice/Companions.lean

@@ -5,13 +5,14 @@ Authors: Suvir Rathore
 -/
 /-
 Statement-level formalisation: compatible families of λ-adic Galois
-representations, and the statement of Lafforgue's companion theorem for curves.
-
-Five supporting results are proved. The companion theorem itself is stated only;
-its proof is `sorry`. Ingredients Mathlib v4.28.0 cannot construct — existence of
-Frobenius elements in the absolute Galois group, and the `MulSemiringAction` of
-`G_K` on the integral closure — are supplied as explicit data or instances and
-documented as such.
+representations, and the companion-existence statement of Lafforgue's theorem
+for curves.
+
+Five supporting results are proved. The companion theorem is stated with its
+proof left `sorry`, and the family over all coefficient places is derived from
+it by choice, inheriting that `sorry`. The one ingredient Mathlib v4.28.0
+cannot construct — existence of Frobenius elements in the absolute Galois
+group — is taken as explicit data and documented as such.
 -/
 import Mathlib
 
@@ -36,8 +37,10 @@ variable (A K : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
 -- A fixed algebraic closure of `K`.
 variable (Kbar : Type*) [Field Kbar] [Algebra K Kbar] [IsAlgClosure K Kbar]
 
-/-- The absolute Galois group `G_K`. The Krull topology instance comes from
-`Mathlib/FieldTheory/KrullTopology.lean`. -/
+/-- The automorphism group of `Kbar` over `K`. The abbreviation itself asks only
+for an extension; wherever the theorems below live, the ambient
+`IsAlgClosure K Kbar` hypothesis makes this the absolute Galois group `G_K`. The
+Krull topology instance comes from `Mathlib/FieldTheory/KrullTopology.lean`. -/
 abbrev AbsGal := Kbar ≃ₐ[K] Kbar
 
 -- The coefficient field `E`.
@@ -323,7 +326,9 @@ universe u
 
 /-- A **companion representation** at `λ`: a continuous representation of `G_K`
 into `GL_n(M)` for some finite extension `M` of `E_λ`, carrying the `E_λ`-module
-topology.
+topology. As with `AbsGal`, the structure asks of `Kbar` only that it extend
+`K`; the `G_K` reading comes from the `IsAlgClosure` hypothesis in force where
+the theorems use it.
 
 The coefficient field is bundled because Lafforgue's theorem does not produce
 companions over `E_λ` itself. Theorem VII.6(v) states the companion over a finite
@@ -361,15 +366,17 @@ variable (A K Kbar : Type*) [CommRing A] [IsDedekindDomain A] [Field K]
 variable (E : Type*) [Field E] [NumberField E] (n : ℕ)
 
 /-- The finite-extension companion-existence consequence of Lafforgue's Theorem
-VII.6(v), after fixing the coefficient field `E` and an `E_{λ₀}`-model, stated one
-place `λ` at a time.
+VII.6, after fixing the coefficient field `E` and an `E_{λ₀}`-model, stated one
+place `λ` at a time. Clause (v) gives the companion and its coefficient field;
+the companion's finite-order determinant is carried from the construction in the
+proof rather than read off the clause.
 
 This is a slice of VII.6, not the whole of it. VII.6 begins from an irreducible
 lisse sheaf of finite-order determinant and constructs `E` and the polynomials
 `P_v`; here both are supplied as data. VII.6 also proves purity, unit-ness of the Frobenius
 roots away from `p` with slope bounds at the places over `p`, and a further
-statement descending the `n`-th power of the companion to `E_λ` itself, none of
-which is formalised.
+statement descending the `n`-fold direct sum of the
+companion to `E_λ` itself, none of which is formalised.
 
 `A` is a finite-type Dedekind `𝔽_q`-algebra with fraction field the function
 field `K`, so `Spec A` is a smooth affine curve over `𝔽_q` and its closed points

README.md

@@ -4,8 +4,9 @@
 
 A statement-level formalisation in Lean 4 of compatible families of λ-adic Galois
 representations, and of the companion-existence statement of Lafforgue's theorem
-for curves. Five supporting lemmas are proved; the companion theorem is stated and
-left `sorry` deliberately. Getting the statement exactly right is the point,
+for curves. Five supporting lemmas are proved, the companion
+theorem is stated and left `sorry` deliberately, and the family over all
+coefficient places is derived from it by choice. Getting the statement exactly right is the point,
 since a statement can compile, pass an axiom audit, and still be mathematically
 false. Several such errors were found here and corrected.
 
@@ -48,12 +49,13 @@ determinant of finite order.
 The statement is made one place `λ` at a time. A family indexed by all `λ`
 follows by choice, and `exists_companion_family` is that derivation.
 
-This is the companion-existence part of Lafforgue's Theorem VII.6(v), not the
-whole of VII.6. VII.6 starts from an irreducible lisse sheaf with finite-order
+This is the companion-existence part of Lafforgue's Theorem VII.6, not the
+whole of it: clause (v) gives the companion and its coefficient field, and the
+companion's finite-order determinant is carried from the construction in the
+proof. VII.6 starts from an irreducible lisse sheaf with finite-order
 determinant and constructs `E` and the `P_v`, which are hypotheses here; it also proves
 purity, unit-ness of the Frobenius roots away from `p` with slope bounds at the
-places over `p`, and a further statement descending the `n`-th power of the
-companion to `E_λ` itself. In
+places over `p`, and a further statement descending the `n`-fold direct sum of the companion to `E_λ` itself. In
 the other direction, the curve here is the affine `Spec A` with `S` removed,
 where VII.6 treats a smooth curve as an open subscheme of a projective one.
 
@@ -212,10 +214,14 @@ made the statement assert more than Lafforgue's theorem gives. A `sorry` conceal
 the difference: a statement that is unprovable because it is false looks exactly
 like a statement that is unproved because the infrastructure is missing.
 
-CI runs the build and checks the axiom profile of the declarations named in
-`Axioms.lean`, so the deliberate `sorry` cannot silently spread into them. It
-does not cover declarations outside their dependency closures, since `lake build`
-exits successfully on the warning a `sorry` emits. Further review is welcome.
+CI runs the build, checks the axiom profile of the declarations named in
+`Axioms.lean`, and counts the `sorry` tokens in the source, requiring exactly
+one. The axiom guard pins the set of axiom names in each declaration's
+dependency closure — the five lemmas admit none beyond the classical three, the
+two theorems additionally `sorryAx` — not the number or location of `sorry`
+terms. The count is what rules out a second `sorry` arriving inside an
+already-tainted proof, or in a declaration outside the guarded closures, either
+of which `lake build` accepts with only a warning. Further review is welcome.
 
 ## Next steps