README and capability log: post-review state and limitations

Author: SuvirRathore

CAPABILITY_LOG.md

@@ -47,3 +47,30 @@ Compiling: `AbsGal`, `CoeffPlace`, `Completion`, `LambdaAdicRep`, `IsCompatibleF
 Open: `IsCompatibleFamily` still takes an *arbitrary* `IsFrobAt` parameter rather than
 the concrete definition. Until that is wired up, the compatible-family definition is a
 faithful schema, not a statement about actual Frobenius elements.
+
+## 2026-08-11 — session 2
+
+### Lean work
+
+- [finding] `IsArithFrobAt.mul_inv_mem_inertia` and `Ideal.inertia` exist in v4.28.0. Frobenius well-definedness at a fixed prime is therefore provable, and was proved (`toHom_eq_of_isArithFrobAt`).
+- [finding] Mathlib's `exists_of_isInvariant` needs `[Finite (S ⧸ Q)]`, so it does not apply at `K̄`. Frobenius existence in the absolute Galois group is a genuine gap — a self-contained candidate for a future contribution.
+- [decision] Superseded declarations deleted rather than annotated. The development trajectory lives in git history and in this log; the source file shows one correct chain.
+
+### Independent review
+
+An earlier version was reviewed by a separate AI system with no history of this
+project. It found four substantive errors, all of which compiled cleanly:
+
+- [error] `IsFrobeniusSystem.isConj_of` asserted that any two Frobenius elements at a place are conjugate. **False.** Two Frobenius lifts at the same prime differ by an inertia element. Had this structure ever been supplied, everything downstream would have been vacuous. Axiom deleted; the correct inertia-based argument proved instead.
+- [error] `charpoly_eq_of_isConj` was presented as establishing that condition (2) is well posed. It does not: the argument needs inertia, not conjugacy.
+- [error] The Lafforgue statement was false as written. Counterexample: a rank-one unramified character of the constant-field quotient can have Frobenius eigenvalues outside `E`. Irreducibility, finite-order determinant, and `E`-rationality added.
+- [error] Frobenius existence was never assumed. Defining a structure with an `exists_frob` field is not assuming it, so the compatibility condition could hold vacuously. Replaced by `FrobeniusChoice` passed as data.
+- [error] Minor: `n : ℕ` admitted `n = 0`; unramifiedness used `∃ Q` where `∀ Q` is wanted; `HeightOneSpectrum A` silently indexes an affine model.
+
+### AI tool performance
+
+- [AI] Claude — Lean/Mathlib mechanics — STRONG. Located the missing `MulSemiringAction`, wrote it correctly, found `Matrix.charpoly_units_conj`, `Ideal.under_smul`, `IsArithFrobAt.conj`, and the inertia lemma. Almost every compile failure was mechanical (arity, docstring placement, `noncomputable`) and fixed in one cycle.
+- [AI] Claude — mathematical faithfulness — WEAK, and this is the headline finding. Asserted a false axiom without checking it against the decomposition/inertia exact sequence; stated a main theorem missing essential hypotheses; described a lemma as establishing well-definedness when it did not; and wrote README claims that the code did not support. All four compiled. None was caught by `lake build`, by iteration, or by self-review.
+- [AI] Claude — self-assessment — UNRELIABLE. Proposed sanity checks that were real but insufficient (`#print axioms` confirms proofs avoid `sorry`; it says nothing about whether definitions are vacuous or statements are true).
+- [AI] independent review — DECISIVE. A model with no investment in the prior choices found in one pass what iteration had not. The practical lesson: for formalisation, an adversarial reader is not optional quality assurance, it is the only check on the step that type-checking cannot see — whether the formal statement means the informal one.
+- [AI] Aristotle — see session 1. Sandbox-side actions were narrated as if performed on the caller's repository.

LambdaAdicSlice/Basic.lean

@@ -364,7 +364,7 @@ Lafforgue's); and `HeightOneSpectrum A` indexes the closed points of an affine
 model, omitting the places at infinity of the projective curve.
 
 Statement only: the proof is `sorry`. -/
-theorem exists_isCompatibleFamily''_of_irreducible
+theorem exists_isCompatibleFamily_of_irreducible
     (hK : FunctionField Fq K)
     (hn : 0 < n)
     (Frob : FrobeniusChoice A K Kbar)

README.md

@@ -1,72 +1,112 @@
 # lambda_adic_slice
 
-Statement-level formalisation of one definitional slice from arithmetic geometry.
-The point is to locate which ingredients Mathlib v4.28.0 currently supports and
-which are missing. The main theorem is stated, not proved; two supporting
+A statement-level formalisation of one definitional slice from arithmetic
+geometry: compatible families of λ-adic Galois representations, and the
+statement of Lafforgue's companion theorem for curves.
+
+The purpose is to find out precisely which ingredients Mathlib v4.28.0 supports
+and which it does not. The main theorem is stated, not proved. Five supporting
 results are proved.
 
 ## The slice
 
 Fix:
-- `K` a global field and `K̄` an algebraic closure, `G_K = Gal(K̄/K)` its absolute
-  Galois group equipped with the Krull topology;
-- `E` a number field (the coefficient field), `λ` ranging over finite places of `E`,
-  with completion `E_λ` and residue characteristic `ℓ(λ)`;
-- `S` a finite set of finite places of `K`;
-- `n ≥ 1` an integer.
-
-**Definition (compatible family).** A family `(ρ_λ)_λ` of continuous homomorphisms
-`ρ_λ : G_K → GL_n(E_λ)` is a *compatible family unramified outside `S`* if:
-
-1. for every `λ`, `ρ_λ` is unramified at every finite place `v` of `K` with
-   `v ∉ S` and `v ∤ ℓ(λ)`;
-2. for every such `v`, the characteristic polynomial of `ρ_λ(Frob_v)` has
-   coefficients in `E` (via a fixed embedding `E ↪ E_λ`) and is independent of `λ`.
-
-**Theorem (Deligne's conjecture, proved by L. Lafforgue).** Suppose `K` is a global
-function field, i.e. the function field of a smooth projective curve over a finite
-field, and `ℓ(λ) ≠ char K`. Then every continuous `λ`-adic representation
-`ρ_λ : G_K → GL_n(E_λ)` unramified outside `S` is a member of a compatible family
+- `K` a global field with algebraic closure `K̄`, and `G_K = Gal(K̄/K)` its
+  absolute Galois group with the Krull topology;
+- `A` a Dedekind domain with fraction field `K`, so that `HeightOneSpectrum A`
+  indexes the finite places of an affine model;
+- `E` a number field (the coefficient field), `λ` ranging over its finite
+  places, with completion `E_λ` and residue characteristic `ℓ(λ)`;
+- `S` a finite set of places;
+- `n ≥ 1`.
+
+**Definition (compatible family).** Given a choice of Frobenius element at each
+place, a family `(ρ_λ)_λ` of continuous homomorphisms `ρ_λ : G_K → GL_n(E_λ)`
+is a *compatible family unramified outside `S`* if:
+
+1. for every `λ`, `ρ_λ` is unramified at every `v ∉ S` with `v ∤ ℓ(λ)`;
+2. for every such `v`, the characteristic polynomial of `ρ_λ(Frob_v)` is the
+   image of a polynomial `P_v ∈ E[T]` that does not depend on `λ`.
+
+**Theorem (Lafforgue's companion theorem).** Let `K` be a global function field
+and `ℓ(λ₀) ≠ char K`. Let `ρ_{λ₀}` be continuous, irreducible, of finite-order
+determinant, unramified outside `S`, and with Frobenius characteristic
+polynomials rational over `E`. Then `ρ_{λ₀}` is a member of a compatible family
 unramified outside `S`.
 
-## Status
-
-Definitions and the Lafforgue statement compile against Mathlib v4.28.0. Two results
-are *proved*, not assumed:
-
-- `charpoly_eq_of_isConj` — the characteristic polynomial of `ρ_λ(g)` depends only on
-  the conjugacy class of `g`, so condition (2) is well posed;
-- `isFrobAt_conj` — conjugates of a Frobenius element at `v` are again Frobenius
-  elements at `v`.
-
-`IsFrobAt` is a definition, not an axiom: it is built on Mathlib's `IsArithFrobAt`
-via a `MulSemiringAction` of `G_K` on the integral closure of `A` in `K̄`, which
-Mathlib does not provide and which is supplied here.
-
-Existence of a Frobenius element at each place remains an axiom. This is not missing
-API: Mathlib's existence proof (`exists_of_isInvariant`) requires a finite residue
-field at the chosen prime, and at `K̄` that residue field is the algebraic closure of
-`A/v`, hence infinite. The *definition* of arithmetic Frobenius transfers to the
-infinite level; the existence *proof* does not.
+## What is proved
+
+- `charpoly_eq_of_isConj_gl`, `charpoly_eq_of_isConj` — the characteristic
+  polynomial of `ρ(g)` depends only on the conjugacy class of `g`.
+- `isFrobAt_conj` — conjugates of a Frobenius element at `v` are again
+  Frobenius elements at `v` (from `IsArithFrobAt.conj`).
+- `toHom_eq_of_isArithFrobAt` — if `ρ` is unramified at `v` and `g`, `g'` are
+  Frobenius elements at the *same* prime `Q` above `v`, then `ρ g = ρ g'`. The
+  argument runs through inertia: `IsArithFrobAt.mul_inv_mem_inertia` gives
+  `g * g'⁻¹ ∈ inertia Q`, which `ρ` kills.
+- `charpoly_eq_of_isArithFrobAt` — the corresponding statement for
+  characteristic polynomials.
+
+`IsFrobAt` is a definition, not an axiom: it is built on Mathlib's
+`IsArithFrobAt` via a `MulSemiringAction` of `G_K` on the integral closure of
+`A` in `K̄`. That instance is **not** in Mathlib and is supplied here; it turned
+out to be the only real obstruction, since `IsArithFrobAt` is already stated for
+monoid actions and needs no finiteness.
+
+## Limitations
+
+Stated explicitly, because a formalisation that compiles is not thereby correct.
+
+- **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 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.
+- **Frobenius independence is proved only at a fixed prime.** Comparing
+  Frobenius elements at different primes above `v` needs transitivity of the
+  `G_K`-action on primes above `v`, which is not available here.
+- **`IsIrred` is irreducibility over `E_λ`**, not absolute irreducibility. The
+  base change to an algebraic closure of `E_λ` is not formalised.
+- **No coefficient-field descent.** The conclusion places the companions over
+  `E_λ` itself. Lafforgue's theorem gives companions over finite extensions of
+  `E_λ`; descending to a common number field is Chin's theorem and is not
+  formalised here.
+- **`HeightOneSpectrum A` indexes an affine model.** For `K = 𝔽_q(t)` and
+  `A = 𝔽_q[t]` the place at infinity is omitted, so "unramified outside `S`"
+  permits ramification there. This is not the same as `π₁^ét(X ∖ S)` for
+  projective `X`.
+- **The main theorem is `sorry`.** Formalising the proof is not in scope.
 
 ## Note on formulation
 
 Stated via `G_K` with an unramified-outside-`S` condition rather than via
-`π₁^ét(X ∖ S)`. These agree for a smooth projective curve `X` with function field `K`,
-and the `G_K` formulation is the one Mathlib v4.28.0 can express: Galois categories
-and fibre functors exist abstractly (`Mathlib/CategoryTheory/Galois/`), but the finite
-étale site of a scheme is not instantiated as a Galois category, so there is no
-`π₁^ét(X)` available.
-
-## Future work (currently out of scope)
-
-- Deligne's conjecture for `K` the function field of a normal variety of finite type
-  over a finite field (dimension ≥ 2), where the index set is closed points of the
-  variety rather than places of `K` — proved by Drinfeld.
-- Chin + Drinfeld independence-of-`ℓ` for arithmetic monodromy groups. Requires
-  algebraic-group infrastructure well beyond this slice.
+`π₁^ét(X ∖ S)`. Mathlib v4.28.0 has a complete abstract Galois-category
+development (`Mathlib/CategoryTheory/Galois/`), but the finite étale site of a
+scheme is not instantiated as a Galois category, so no `π₁^ét(X)` is available.
+
+## Correctness
+
+`lake build` verifies that the proofs are valid. It does not verify that the
+definitions say what they are intended to say. An independent review of an
+earlier version found four substantive errors, all of which had compiled: a
+false axiom asserting that Frobenius lifts at a place are conjugate (they differ
+by inertia); a well-definedness claim that the proved lemmas did not support; a
+main theorem missing the hypotheses that make it true; and a vacuity hole where
+Frobenius existence was never actually assumed. Those are fixed. Further review
+is welcome — see `CAPABILITY_LOG.md`.
+
+## Future work
+
+- Deligne's conjecture for function fields of normal varieties of finite type
+  over a finite field of dimension ≥ 2, where the index set is closed points
+  rather than places — proved by Drinfeld.
+- Chin + Drinfeld independence-of-`ℓ` for arithmetic monodromy groups.
+- Existence of Frobenius elements in the absolute Galois group — self-contained,
+  currently missing from Mathlib, and a plausible contribution.
 
 ## Build
 
 Lean v4.28.0, Mathlib v4.28.0 (pinned for Aristotle compatibility).
-`lake exe cache get && lake build`
+lake exe cache get && lake build