Session 1: capability log, README status

Author: SuvirRathore

CAPABILITY_LOG.md

@@ -9,11 +9,41 @@ One line per session on where AI tools succeeded or failed, and why.
 
 ## 2026-08-10 — session 1 (Mathlib survey, v4.28.0)
 
-- [survey] `G_K` + Krull topology — EXISTS — `FieldTheory/KrullTopology.lean`, `krullTopology` instance.
-- [survey] Finite places, `E_λ` — EXISTS — `IsDedekindDomain.HeightOneSpectrum`, `.adicCompletion`.
-- [survey] `GL_n`, characteristic polynomial — EXISTS — `Matrix/GeneralLinearGroup/`, `Matrix/Charpoly/`.
-- [survey] Global function fields — PARTIAL — `NumberTheory/FunctionField.lean` has the predicate and valuations, no curve tie-in.
-- [survey] Frobenius — PARTIAL, PRINCIPAL GAP — `RingTheory/Frobenius.lean` gives `arithFrobAt` for a FINITE group acting on a ring with finite residue field. No construction of `Frob_v` in the absolute Galois group (needs the compatible system across finite levels, up to conjugacy). Must be taken as a hypothesis.
-- [survey] Unramified at a place — PARTIAL — `RingTheory/Unramified/`, `RamificationInertia/Unramified.lean`; no ready-made unramified-outside-`S` condition for a representation.
-- [survey] Char-poly coefficients descending to `E` — MISSING — no lemma; stated as a hypothesis.
-- [survey] `π₁^ét(X)` — MISSING — `CategoryTheory/Galois/` is abstract Galois categories only (Merten 2024); the finite étale site of a scheme is not instantiated as one, so no `π₁^ét`. Decided the slice formulation on this basis.
+- [survey] `G_K` + Krull topology — exists — `FieldTheory/KrullTopology.lean`, `krullTopology` instance.
+- [survey] Finite places, `E_λ` — exists — `IsDedekindDomain.HeightOneSpectrum`, `.adicCompletion`.
+- [survey] `GL_n`, characteristic polynomial — exists — `Matrix/GeneralLinearGroup/`, `Matrix/Charpoly/`.
+- [survey] Global function fields — partial — `NumberTheory/FunctionField.lean` has the predicate and valuations, no curve tie-in.
+- [survey] Frobenius — partial, principal gap — `RingTheory/Frobenius.lean` gives `arithFrobAt` for a finite group acting on a ring with finite residue field. No construction of `Frob_v` in the absolute Galois group (needs the compatible system across finite levels, up to conjugacy). Must be taken as a hypothesis.
+- [survey] Unramified at a place — partial — `RingTheory/Unramified/`, `RamificationInertia/Unramified.lean`; no ready-made unramified-outside-`S` condition for a representation.
+- [survey] Char-poly coefficients descending to `E` — missing — no lemma; stated as a hypothesis.
+- [survey] `π₁^ét(X)` — missing — `CategoryTheory/Galois/` is abstract Galois categories only (Merten 2024); the finite étale site of a scheme is not instantiated as one, so no `π₁^ét`. Decided the slice formulation on this basis.
+
+## 2026-08-10 — session 1 (Lean work)
+
+### Mathlib findings
+
+- [finding] `MulSemiringAction (AbsGal K Kbar) (integralClosure A Kbar)` — missing from Mathlib v4.28.0, constructed here in ~10 lines. This was the only real obstruction to applying Mathlib's Frobenius machinery to the absolute Galois group.
+- [finding] Initial survey verdict ("no absolute-Galois Frobenius") was wrong and was corrected by reading the source. `AlgHom.IsArithFrobAt` / `IsArithFrobAt` are stated for a *monoid* action with `SMulCommClass` — no finiteness required. Only the choice function `arithFrobAt` needs `[Finite (S ⧸ Q)]`. Consequence: `IsFrobAt` is definable, not axiomatic.
+- [finding] Sharper distinction, and the headline result: the *definition* of arithmetic Frobenius transfers to the infinite level (`IsArithFrobAt A g Q` reads `g x - x ^ Nat.card (A ⧸ v) ∈ Q`, and `A/v` is finite), but the *existence theorem* `exists_of_isInvariant` does not — it requires `Finite (S ⧸ Q)`, and at `K̄` the residue field is the algebraic closure of `A/v`, hence infinite. Existence therefore remains an axiom for genuine mathematical reasons, not for want of API.
+- [finding] `π₁^ét(X)` — absent. `Mathlib/CategoryTheory/Galois/` (Merten 2024) is a complete abstract Galois-category development, but the finite étale site of a scheme is not instantiated as one. Determined the slice's formulation.
+- [finding] `Matrix.charpoly_units_conj` exists, so conjugation-invariance of the characteristic polynomial is provable rather than assumed.
+- [finding] `Ideal.under_smul` and `Ideal.IsPrime.smul` both exist — guessed by name, correct first try.
+
+### AI tool performance
+
+- [AI] Aristotle — smoke test, single `sorry` (`1 + 1 = 2`) — succeeded — returned `by norm_num`, project compiled.
+- [AI] Aristotle — returning results — reported "The change is committed and pushed" when it had touched only its own server-side sandbox; the local working tree was unchanged. Results reach the caller only via `--destination <archive>` with `--wait`. Failure mode: sandbox-side actions narrated as if performed on the repo.
+- [AI] Claude — Mathlib survey from file listings and grep — partially wrong — produced a plausible but incorrect verdict on Frobenius by inferring from `arithFrobAt`'s signature without reading `IsArithFrobAt`'s. Corrected only by reading the source directly. Failure mode: confident generalisation from an adjacent declaration.
+- [AI] Claude — Lean syntax — wrong twice — attached docstrings (`/-- -/`) to `variable` and to `omit ... in`, neither of which is a declaration. Cost two build cycles. Compounding factor: Lean's parser reports this as `unexpected token; expected 'lemma'`, which points nowhere near the cause.
+- [AI] Claude — `Matrix.charpoly_units_conj` application — wrong first try — wrapped the argument in `Units.map`, causing a `(GL n R)ˣ` type mismatch; `GL n R` is already `(Matrix n n R)ˣ`.
+- [AI] Claude — elaboration cost — unanticipated — proving conjugation-invariance directly inside `Completion E lam` (a `UniformSpace.Completion`) hit the default heartbeat limit. Fixed by proving the lemma over an abstract `CommRing` and specialising.
+
+### Status
+
+Compiling: `AbsGal`, `CoeffPlace`, `Completion`, `LambdaAdicRep`, `IsCompatibleFamily`,
+`IsFrobeniusSystem`, the Lafforgue statement (`sorry`), plus two proved theorems —
+`charpoly_eq_of_isConj` and `isFrobAt_conj` — and `IsFrobAt` as a genuine definition.
+
+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.

README.md

@@ -1,8 +1,9 @@
 # lambda_adic_slice
 
 Statement-level formalisation of one definitional slice from arithmetic geometry.
-Statements only: every proof is `sorry`. The point is to locate which ingredients
-Mathlib v4.28.0 currently supports and which are missing.
+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
+results are proved.
 
 ## The slice
 
@@ -22,20 +23,40 @@ Fix:
 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 for curves; L. Lafforgue).** Suppose `K` is a global
+**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
 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.
+
 ## 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 plausibly 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.
+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)