From 85d0eda7d269c6e796a76f9e58b987d19dd1e8c2 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 27 Aug 2026 15:16:17 +0200
Subject: [PATCH 1/2] demo: LMLExtra library

---
 .github/workflows/blueprint.yml               | 27 ++++--
 CONTRIBUTING.md                               | 17 ++++
 LMLExtra.lean                                 |  3 +
 LMLExtra/SumRewardsBounds.lean                | 67 ++++++++++++++
 LMLTest.lean                                  |  1 +
 LMLTest/ExtraDataLinter.lean                  | 66 ++++++++++++++
 LeanMachineLearning.lean                      |  2 +
 .../SequentialLearning/SumRewardsBounds.lean  | 40 +++++++++
 .../Tactic/Linter/ExtraData.lean              | 90 +++++++++++++++++++
 lakefile.toml                                 | 12 ++-
 scripts/check_extra_imports.sh                | 15 ++++
 11 files changed, 333 insertions(+), 7 deletions(-)
 create mode 100644 LMLExtra.lean
 create mode 100644 LMLExtra/SumRewardsBounds.lean
 create mode 100644 LMLTest.lean
 create mode 100644 LMLTest/ExtraDataLinter.lean
 create mode 100644 LeanMachineLearning/SequentialLearning/SumRewardsBounds.lean
 create mode 100644 LeanMachineLearning/Tactic/Linter/ExtraData.lean
 create mode 100755 scripts/check_extra_imports.sh

diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 7b5fd73d..75d5da79 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -41,11 +41,14 @@ env:
   # published URL, and existing links to it would break.
   REFEREE_SITE_URL: https://leanmachinelearning.org/LML/exposition
 
-  # The library that is exposed on the site, and the one excluded from every phase that imports the
-  # project. Named once here because `collect`, `extract`, `highlight` and the hash export all have
-  # to agree — a mismatch between the hashed set and the collected set makes `provenance` hard-fail.
+  # The library that is exposed on the site, and the ones excluded from every phase that imports
+  # the project. Named once here because `collect`, `extract`, `highlight` and the hash export all
+  # have to agree — a mismatch between the hashed set and the collected set makes `provenance`
+  # hard-fail.
   REFEREE_ROOT: LeanMachineLearning
-  REFEREE_EXCLUDE_LIB: LMLTutorial
+  # Space-separated. `LMLExtra` is the companion library with lighter review (see `lakefile.toml`)
+  # and `LMLTest` holds tests; neither is part of the exposed library.
+  REFEREE_EXCLUDE_LIBS: LMLTutorial LMLExtra LMLTest
 
   # Generated data, deliberately *outside* the working tree. `provenance` records whether the tree
   # was clean when it folded, via `git status --porcelain`, which counts untracked files — so
@@ -108,6 +111,16 @@ jobs:
           lint: true
           mk_all-check: true
 
+      # `LeanMachineLearning` may use theorems of `LMLExtra` but not its data. The linter that
+      # enforces it runs as part of `lake lint` above (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`);
+      # this checks the import discipline that the linter relies on.
+      - name: Check that LeanMachineLearning imports LMLExtra only privately
+        run: scripts/check_extra_imports.sh
+
+      # Not a default target, so not built by `lake build` above (and not linted).
+      - name: Build tests
+        run: lake build LMLTest --wfail
+
       - name: Download referee binary
         if: github.event_name == 'push'
         env:
@@ -170,9 +183,10 @@ jobs:
         if: github.event_name == 'push'
         run: |
           set -euo pipefail
+          exclude=(); for lib in $REFEREE_EXCLUDE_LIBS; do exclude+=(--exclude-lib "$lib"); done
           lake env "$REFEREE_BIN" collect \
             --root "$REFEREE_ROOT" \
-            --exclude-lib "$REFEREE_EXCLUDE_LIB" \
+            "${exclude[@]}" \
             --hashes "$REFEREE_HASHES" \
             --data "$REFEREE_DATA"
 
@@ -318,8 +332,9 @@ jobs:
           # deliberately skipped — it re-elaborates every extracted file and costs more than the
           # rest of this job combined; without it the standalone files are still written and linked,
           # just not rendered inline.
+          exclude=(); for lib in $REFEREE_EXCLUDE_LIBS; do exclude+=(--exclude-lib "$lib"); done
           lake env "$REFEREE_BIN" extract \
-            --data "$REFEREE_DATA" --exclude-lib "$REFEREE_EXCLUDE_LIB" --output ./referee-site
+            --data "$REFEREE_DATA" "${exclude[@]}" --output ./referee-site
           lake env "$REFEREE_BIN" highlight \
             --data "$REFEREE_DATA" --output ./referee-site
           # `--trust` is an editorial claim, not a derived fact: it says whoever publishes this site
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index a1b3036b..20ddc46b 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -31,6 +31,23 @@ For results about definitions from Mathlib, we place them in the same namespace
 
 The `Tutorial` folder is reserved for material used in the tutorial, and should not be used for general contributions.
 
+## The `LMLExtra` library
+
+`LMLExtra` is a companion library with a lighter review process, meant to host results about the definitions of `LeanMachineLearning` (including results contributed by AI agents with limited human review).
+The two libraries live in the same Lake package and the rules are asymmetric:
+
+- `LMLExtra` may use everything in `LeanMachineLearning`.
+- `LeanMachineLearning` may use the *theorems* of `LMLExtra`, inside proofs only.
+  It must not depend on any *data* defined in `LMLExtra`: no definition, instance, structure or `Prop`-valued predicate of `LMLExtra` may appear in a statement or in a definition of `LeanMachineLearning`.
+  If a definition of `LMLExtra` becomes needed in `LeanMachineLearning`, it must be moved there and reviewed.
+
+This is enforced by two automated checks:
+
+- `LeanMachineLearning` files import `LMLExtra` files privately, with a plain `import LMLExtra.Foo` (never `public import` or `import all`).
+  The module system then rejects `LMLExtra` constants in public signatures and exposed bodies.
+  `scripts/check_extra_imports.sh` checks this discipline.
+- The `extraData` environment linter (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`, run by `lake lint`) flags any declaration outside `LMLExtra` whose type, or whose value outside of proof subterms, mentions a non-proof constant of `LMLExtra`.
+
 ## Code quality and LLM policy
 
 The strength of the library lies in carefully designed and reviewed definitions.
diff --git a/LMLExtra.lean b/LMLExtra.lean
new file mode 100644
index 00000000..f534af93
--- /dev/null
+++ b/LMLExtra.lean
@@ -0,0 +1,3 @@
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import LMLExtra.SumRewardsBounds
diff --git a/LMLExtra/SumRewardsBounds.lean b/LMLExtra/SumRewardsBounds.lean
new file mode 100644
index 00000000..90001acc
--- /dev/null
+++ b/LMLExtra/SumRewardsBounds.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.SumRewards
+
+/-!
+# Bounds on sums of rewards
+
+Demo file for the `LMLExtra` library.
+
+`LMLExtra` may use everything in `LeanMachineLearning`. In the other direction,
+`LeanMachineLearning` may use the *theorems* proved here (only inside proofs), but none of the
+*data* defined here: the definition `pullTimes` and the `Prop`-valued predicate `WasPulled` below
+must not appear in any statement or definition of `LeanMachineLearning`.
+This is enforced by the `extraData` environment linter.
+
+## Main results
+
+* `sumRewards_le_pullCount_mul`, `pullCount_mul_le_sumRewards`: bounds on the sum of rewards of
+  an action in terms of its number of pulls. Their statements only involve `LeanMachineLearning`
+  definitions, so `LeanMachineLearning` can use them.
+-/
+
+@[expose] public section
+
+open Finset
+
+namespace Learning
+
+variable {𝓐 𝓨 Ω : Type*} [DecidableEq 𝓐] [AddCommGroup 𝓨]
+  {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → 𝓨} {a : 𝓐} {s t : ℕ} {ω : Ω}
+
+/-- Times before `t` at which action `a` was chosen. -/
+def pullTimes (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ :=
+  (range t).filter (fun s ↦ A s ω = a)
+
+@[simp]
+lemma mem_pullTimes : s ∈ pullTimes A a t ω ↔ s < t ∧ A s ω = a := by simp [pullTimes]
+
+lemma card_pullTimes : #(pullTimes A a t ω) = pullCount A a t ω := rfl
+
+lemma sumRewards_eq_sum_pullTimes : sumRewards A R a t ω = ∑ s ∈ pullTimes A a t ω, R s ω := by
+  simp [sumRewards, pullTimes, sum_filter]
+
+/-- Action `a` was chosen at least once before time `t`. -/
+def WasPulled (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Prop := (pullTimes A a t ω).Nonempty
+
+lemma wasPulled_iff : WasPulled A a t ω ↔ ∃ s < t, A s ω = a := by
+  simp [WasPulled, Finset.Nonempty]
+
+lemma sumRewards_le_pullCount_mul {R : ℕ → Ω → ℝ} {c : ℝ}
+    (hR : ∀ s < t, A s ω = a → R s ω ≤ c) :
+    sumRewards A R a t ω ≤ pullCount A a t ω * c := by
+  rw [sumRewards_eq_sum_pullTimes, ← card_pullTimes, ← nsmul_eq_mul]
+  exact sum_le_card_nsmul _ _ _ fun s hs ↦ hR s (mem_pullTimes.1 hs).1 (mem_pullTimes.1 hs).2
+
+lemma pullCount_mul_le_sumRewards {R : ℕ → Ω → ℝ} {c : ℝ}
+    (hR : ∀ s < t, A s ω = a → c ≤ R s ω) :
+    pullCount A a t ω * c ≤ sumRewards A R a t ω := by
+  rw [sumRewards_eq_sum_pullTimes, ← card_pullTimes, ← nsmul_eq_mul]
+  exact card_nsmul_le_sum _ _ _ fun s hs ↦ hR s (mem_pullTimes.1 hs).1 (mem_pullTimes.1 hs).2
+
+end Learning
diff --git a/LMLTest.lean b/LMLTest.lean
new file mode 100644
index 00000000..c8341163
--- /dev/null
+++ b/LMLTest.lean
@@ -0,0 +1 @@
+import LMLTest.ExtraDataLinter
diff --git a/LMLTest/ExtraDataLinter.lean b/LMLTest/ExtraDataLinter.lean
new file mode 100644
index 00000000..7f173424
--- /dev/null
+++ b/LMLTest/ExtraDataLinter.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import Batteries.Tactic.Lint
+import LeanMachineLearning.Tactic.Linter.ExtraData
+import LMLExtra.SumRewardsBounds
+
+/-! # Tests for the `extraData` linter
+
+The declarations below live outside `LMLExtra`, so the linter applies to them.
+-/
+
+open Finset Learning
+
+variable {𝓐 Ω : Type*} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ} {ω : Ω}
+
+section allowed
+
+/-- A proof may use an `LMLExtra` theorem. -/
+theorem ok_thm_uses_extra_theorem {R : ℕ → Ω → ℝ} {c : ℝ}
+    (hR : ∀ s < t, A s ω = a → R s ω ≤ c) :
+    sumRewards A R a t ω ≤ pullCount A a t ω * c :=
+  sumRewards_le_pullCount_mul hR
+
+/-- A proof may use an `LMLExtra` theorem whose statement mentions `LMLExtra` data. -/
+theorem ok_thm_uses_extra_theorem_about_extra_data (h : ∃ s < t, A s ω = a) :
+    0 < pullCount A a t ω := by
+  rw [← card_pullTimes]
+  exact card_pos.2 (wasPulled_iff.2 h)
+
+/-- The proof subterm of a definition may use an `LMLExtra` theorem about `LMLExtra` data. -/
+noncomputable def ok_def_with_proof_subterm (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) :
+    {n : ℕ // n = pullCount A a t ω} :=
+  ⟨pullCount A a t ω, by rw [← card_pullTimes]⟩
+
+end allowed
+
+section forbidden
+
+/-- The statement mentions an `LMLExtra` definition. -/
+theorem bad_thm_statement : #(pullTimes A a t ω) = pullCount A a t ω := card_pullTimes
+
+/-- The statement mentions an `LMLExtra` `Prop`-valued definition. -/
+theorem bad_thm_statement_prop_def (h : WasPulled A a t ω) : 0 < pullCount A a t ω := by
+  rw [← card_pullTimes]
+  exact card_pos.2 h
+
+/-- The value uses an `LMLExtra` definition. -/
+def bad_def_value (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := pullTimes A a t ω
+
+end forbidden
+
+/--
+error: -- Found 3 errors in 6 declarations (plus 1 automatically generated ones) in the current file with 1 linters
+
+/- The `extraData` linter reports:
+DECLARATIONS DEPEND ON `LMLExtra` DATA. Only theorems of `LMLExtra` may be used, and only inside proofs:
+This linter can be disabled with `@[nolint extraData]`. -/
+#check @bad_thm_statement /- depends on `LMLExtra` data: [pullTimes] -/
+#check @bad_thm_statement_prop_def /- depends on `LMLExtra` data: [WasPulled] -/
+#check @bad_def_value /- depends on `LMLExtra` data: [pullTimes] -/
+-/
+#guard_msgs in
+#lint only extraData
diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 97d0683c..fa1c811a 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -47,6 +47,7 @@ public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
 public import LeanMachineLearning.SequentialLearning.Means
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
 public import LeanMachineLearning.SequentialLearning.SumRewards
+public import LeanMachineLearning.SequentialLearning.SumRewardsBounds
 public import LeanMachineLearning.Tactic.EqLift
 public import LeanMachineLearning.Tactic.EqLift.ForMathlib.Kernel
 public import LeanMachineLearning.Tactic.EqLift.ForMathlib.MeasurableEquiv
@@ -71,3 +72,4 @@ public import LeanMachineLearning.Tactic.KernelHom.Tactic.KernelDiagram
 public import LeanMachineLearning.Tactic.KernelHom.Tactic.KernelHom
 public import LeanMachineLearning.Tactic.KernelHom.Tactic.Reassoc
 public import LeanMachineLearning.Tactic.KernelHom.Tactic.Utils
+public import LeanMachineLearning.Tactic.Linter.ExtraData
diff --git a/LeanMachineLearning/SequentialLearning/SumRewardsBounds.lean b/LeanMachineLearning/SequentialLearning/SumRewardsBounds.lean
new file mode 100644
index 00000000..2f69b0a2
--- /dev/null
+++ b/LeanMachineLearning/SequentialLearning/SumRewardsBounds.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LeanMachineLearning.SequentialLearning.SumRewards
+import LMLExtra.SumRewardsBounds
+
+/-!
+# Bounds on the empirical mean
+
+This file demonstrates how `LeanMachineLearning` uses `LMLExtra`: the import of
+`LMLExtra.SumRewardsBounds` is private (plain `import`, not `public import`), so nothing from
+`LMLExtra` is re-exported, and its theorems are only used inside proofs. The statements below
+mention only `LeanMachineLearning` definitions.
+-/
+
+@[expose] public section
+
+namespace Learning
+
+variable {𝓐 Ω : Type*} [DecidableEq 𝓐] {A : ℕ → Ω → 𝓐} {a : 𝓐} {t : ℕ} {ω : Ω}
+
+lemma empMean_le_of_le {R : ℕ → Ω → ℝ} {c : ℝ} (h_pull : pullCount A a t ω ≠ 0)
+    (hR : ∀ s < t, A s ω = a → R s ω ≤ c) :
+    empMean A R a t ω ≤ c := by
+  have h_pos : (0 : ℝ) < pullCount A a t ω := by exact_mod_cast Nat.pos_of_ne_zero h_pull
+  rw [empMean, div_le_iff₀ h_pos, mul_comm]
+  exact sumRewards_le_pullCount_mul hR
+
+lemma le_empMean_of_le {R : ℕ → Ω → ℝ} {c : ℝ} (h_pull : pullCount A a t ω ≠ 0)
+    (hR : ∀ s < t, A s ω = a → c ≤ R s ω) :
+    c ≤ empMean A R a t ω := by
+  have h_pos : (0 : ℝ) < pullCount A a t ω := by exact_mod_cast Nat.pos_of_ne_zero h_pull
+  rw [empMean, le_div_iff₀ h_pos, mul_comm]
+  exact pullCount_mul_le_sumRewards hR
+
+end Learning
diff --git a/LeanMachineLearning/Tactic/Linter/ExtraData.lean b/LeanMachineLearning/Tactic/Linter/ExtraData.lean
new file mode 100644
index 00000000..8f7fec65
--- /dev/null
+++ b/LeanMachineLearning/Tactic/Linter/ExtraData.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Batteries.Tactic.Lint.Basic
+public meta import Lean.Meta.ForEachExpr
+
+/-!
+# The `extraData` linter
+
+`LMLExtra` is a companion library of `LeanMachineLearning` with a lighter review process.
+It may use everything in `LeanMachineLearning`. In the other direction, `LeanMachineLearning`
+may use the *theorems* of `LMLExtra`, but must not depend on any *data* defined there:
+definitions, instances, structures, inductive types, `Prop`-valued predicates...
+
+The `extraData` environment linter enforces this. A declaration `d` outside `LMLExtra` is
+flagged if a non-proof constant declared in an `LMLExtra` module occurs
+* in the type of `d`, or
+* if `d` is not itself a proof, in the value of `d` outside of proof subterms.
+
+Proofs are never constrained: a proof may use any `LMLExtra` theorem, including theorems whose
+statements mention `LMLExtra` definitions.
+
+Together with the module system this gives the intended discipline: `LeanMachineLearning` files
+import `LMLExtra` files *privately* (`import`, never `public import` nor `import all`; see
+`scripts/check_extra_imports.sh`), so that Lean already rejects `LMLExtra` constants in public
+signatures and exposed bodies, and this linter covers what the module system allows through
+(non-exposed definition bodies, instances found by typeclass resolution).
+-/
+
+open Lean Meta Batteries.Tactic.Lint
+
+namespace LeanMachineLearning.Linter
+
+/-- The root module name of the `LMLExtra` library. -/
+meta def extraRoot : Name := `LMLExtra
+
+/-- The module in which `c` was declared (the main module for a declaration of the current
+file). -/
+meta def moduleOf (c : Name) : CoreM Name := do
+  let env ← getEnv
+  return match env.getModuleIdxFor? c with
+    | some idx => env.header.moduleNames[idx]!
+    | none => env.mainModule
+
+/-- Is `c` declared in `LMLExtra` and not a proof, i.e. is its type not a proposition?
+Definitions, instances, structures and their projections, inductive types and their constructors,
+and `Prop`-valued predicates all qualify. Theorems do not. -/
+meta def isExtraData (c : Name) : MetaM Bool := do
+  unless (← moduleOf c).getRoot == extraRoot do return false
+  let some ci := (← getEnv).find? c | return false
+  return !(← isProp ci.type)
+
+/-- Add to `acc` the constants occurring in `e` outside of proof subterms. -/
+meta def collectDataConsts (acc : IO.Ref NameSet) (e : Expr) : MetaM Unit :=
+  forEachExpr' e fun t => do
+    match t with
+    | .const n _ => acc.modify (·.insert n); return false
+    | .app .. | .lam .. | .letE .. | .proj .. | .mdata .. =>
+      -- Do not descend into proofs: what a proof mentions is irrelevant.
+      return !(← try isProof t catch _ => pure false)
+    | _ => return true
+
+/-- The constants that the declaration `d` depends on as data: those occurring in its type, and,
+if `d` is not itself a proof, those occurring in its value outside of proof subterms. -/
+meta def dataConsts (d : Name) : MetaM NameSet := do
+  let ci ← getConstInfo d
+  let acc ← IO.mkRef ({} : NameSet)
+  collectDataConsts acc ci.type
+  unless ← isProp ci.type do
+    if let some v := ci.value? then collectDataConsts acc v
+  acc.get
+
+/-- Declarations outside `LMLExtra` must not depend on data defined in `LMLExtra`.
+See the module docstring of `LeanMachineLearning.Tactic.Linter.ExtraData`. -/
+@[env_linter] public meta def extraData : Linter where
+  noErrorsFound := "No declaration depends on `LMLExtra` data."
+  errorsFound := "DECLARATIONS DEPEND ON `LMLExtra` DATA. \
+    Only theorems of `LMLExtra` may be used, and only inside proofs:"
+  test d := do
+    -- `LMLExtra` may of course use its own definitions.
+    if (← moduleOf d).getRoot == extraRoot then return none
+    let bad ← (← dataConsts d).toList.filterM isExtraData
+    if bad.isEmpty then return none
+    return m!"depends on `LMLExtra` data: {bad.map MessageData.ofConstName}"
+
+end LeanMachineLearning.Linter
diff --git a/lakefile.toml b/lakefile.toml
index be4eda1d..937d1618 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,5 @@
 name = "LeanMachineLearning"
-defaultTargets = ["LeanMachineLearning"]
+defaultTargets = ["LeanMachineLearning", "LMLExtra"]
 lintDriver = "batteries/runLinter"
 
 [leanOptions]
@@ -22,6 +22,16 @@ rev = "cf65d43b4f5e1a79482e8c488d121853b9d7ca05"
 [[lean_lib]]
 name = "LeanMachineLearning"
 
+# Companion library with lighter review: may use everything in `LeanMachineLearning`.
+# `LeanMachineLearning` may use its theorems (in proofs) but never its data; this is enforced by
+# the `extraData` environment linter and by `scripts/check_extra_imports.sh`.
+[[lean_lib]]
+name = "LMLExtra"
+
+# Tests. Not a default target: built explicitly in CI and not linted.
+[[lean_lib]]
+name = "LMLTest"
+
 [[lean_lib]]
 name = "LMLTutorial"
 globs = ["LMLTutorial.*"]
diff --git a/scripts/check_extra_imports.sh b/scripts/check_extra_imports.sh
new file mode 100755
index 00000000..e55006be
--- /dev/null
+++ b/scripts/check_extra_imports.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# `LeanMachineLearning` may only import `LMLExtra` privately, i.e. with a plain
+# `import LMLExtra.Foo`. A `public import` would re-export `LMLExtra` to every importer of the
+# file, and an `import all` would give access to the non-public declarations of the `LMLExtra`
+# file. Both would circumvent the checks that the module system performs on private imports.
+# See `LeanMachineLearning/Tactic/Linter/ExtraData.lean`.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+
+pattern='^[[:space:]]*(public[[:space:]]+(meta[[:space:]]+)?import([[:space:]]+all)?|(meta[[:space:]]+)?import[[:space:]]+all)[[:space:]]+LMLExtra([.[:space:]]|$)'
+if grep -rnE --include='*.lean' "$pattern" LeanMachineLearning LeanMachineLearning.lean; then
+  echo "error: LeanMachineLearning must import LMLExtra privately (plain 'import LMLExtra.Foo')." >&2
+  exit 1
+fi
+echo "OK: LeanMachineLearning imports LMLExtra only privately."

From c17f26e502c43b6b77386aab5f35aafd52e00642 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Thu, 27 Aug 2026 15:47:43 +0200
Subject: [PATCH 2/2] better checks

---
 .github/workflows/blueprint.yml               |  10 +-
 CONTRIBUTING.md                               |   7 +-
 LMLTest/ExtraDataLinter.lean                  | 117 +++++++++++++++++-
 .../Tactic/Linter/ExtraData.lean              |  34 +++--
 scripts/check_extra_data.lean                 |  52 ++++++++
 scripts/check_extra_imports.sh                |  36 ++++--
 6 files changed, 232 insertions(+), 24 deletions(-)
 create mode 100644 scripts/check_extra_data.lean

diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 75d5da79..20fedaf4 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -111,12 +111,16 @@ jobs:
           lint: true
           mk_all-check: true
 
-      # `LeanMachineLearning` may use theorems of `LMLExtra` but not its data. The linter that
-      # enforces it runs as part of `lake lint` above (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`);
-      # this checks the import discipline that the linter relies on.
+      # `LeanMachineLearning` may use theorems of `LMLExtra` but not its data
+      # (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`). The first step checks the import
+      # discipline the module system relies on; the second is the authoritative check of the rule:
+      # the same test as the `extraData` linter of `lake lint` above, but ignoring `@[nolint]`.
       - name: Check that LeanMachineLearning imports LMLExtra only privately
         run: scripts/check_extra_imports.sh
 
+      - name: Check that LeanMachineLearning does not depend on LMLExtra data
+        run: lake env lean --run scripts/check_extra_data.lean
+
       # Not a default target, so not built by `lake build` above (and not linted).
       - name: Build tests
         run: lake build LMLTest --wfail
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 20ddc46b..fd608e80 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -43,10 +43,11 @@ The two libraries live in the same Lake package and the rules are asymmetric:
 
 This is enforced by two automated checks:
 
-- `LeanMachineLearning` files import `LMLExtra` files privately, with a plain `import LMLExtra.Foo` (never `public import` or `import all`).
-  The module system then rejects `LMLExtra` constants in public signatures and exposed bodies.
+- `LeanMachineLearning` files import `LMLExtra` files privately, with a plain `import LMLExtra.Foo` (never `public import`, `meta import` or `import all`), and only from files using the module system.
+  The module system then rejects `LMLExtra` constants in public signatures and exposed bodies, and no `LMLExtra` metaprogram runs while elaborating `LeanMachineLearning`.
   `scripts/check_extra_imports.sh` checks this discipline.
-- The `extraData` environment linter (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`, run by `lake lint`) flags any declaration outside `LMLExtra` whose type, or whose value outside of proof subterms, mentions a non-proof constant of `LMLExtra`.
+- The `extraData` environment linter (`LeanMachineLearning/Tactic/Linter/ExtraData.lean`, run by `lake lint` and available as `#lint only extraData`) flags any declaration outside `LMLExtra` whose type, or whose value outside of proof subterms, mentions a non-proof constant of `LMLExtra`.
+  CI runs the same check through `lake env lean --run scripts/check_extra_data.lean`, which ignores `@[nolint extraData]`: there is no exception to this rule.
 
 ## Code quality and LLM policy
 
diff --git a/LMLTest/ExtraDataLinter.lean b/LMLTest/ExtraDataLinter.lean
index 7f173424..0fe16e0b 100644
--- a/LMLTest/ExtraDataLinter.lean
+++ b/LMLTest/ExtraDataLinter.lean
@@ -9,7 +9,18 @@ import LMLExtra.SumRewardsBounds
 
 /-! # Tests for the `extraData` linter
 
-The declarations below live outside `LMLExtra`, so the linter applies to them.
+The declarations below live outside `LMLExtra`, so the linter applies to them. The first two
+sections show the intended behavior. The following ones are attempts to make a declaration depend
+on `LMLExtra` data without being reported: the `#lint` at the end shows that every attempt is
+caught on the constant that actually mentions the data (which is not always the declaration
+written by the user).
+
+Attempts that are rejected elsewhere and therefore do not appear here:
+* `attribute [nolint extraData] Learning.pullCount` from another file: attributes cannot be added
+  to declarations of imported modules.
+* `public import`/`meta import`/`import all` of `LMLExtra`, or importing it from a non-`module`
+  file: rejected by `scripts/check_extra_imports.sh`.
+* `@[nolint extraData]` added by a metaprogram: ignored by `scripts/check_extra_data.lean`.
 -/
 
 open Finset Learning
@@ -52,15 +63,117 @@ def bad_def_value (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Fin
 
 end forbidden
 
+/-! Launder through an "internal"-looking name. Reported on `Learning._laundered`. -/
+
+def Learning._laundered (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := pullTimes A a t ω
+
+def a1_uses_laundered (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ :=
+  Learning._laundered A a t ω
+
+/-! Launder through a private definition. Reported on `laundered`. -/
+
+private def laundered (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := pullTimes A a t ω
+
+def a2_uses_private (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := laundered A a t ω
+
+/-! Structure field default value. Reported on `WithDefault.times._default`, and on the use since
+the default is inlined. -/
+
+structure WithDefault (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) where
+  times : Finset ℕ := pullTimes A a t ω
+
+def a3_uses_default (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : WithDefault A a t ω := {}
+
+/-! `partial def`: the body lives in `a4_partial._unsafe_rec`, where it is reported. -/
+
+partial def a4_partial (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) (n : ℕ) : Finset ℕ :=
+  if n = 0 then pullTimes A a t ω else a4_partial A a t ω (n - 1)
+
+/-! `if` on an `LMLExtra` proposition with classical decidability. -/
+
+open Classical in
+noncomputable def a5_ite (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
+  if WasPulled A a t ω then 1 else 0
+
+/-! `Classical.choose` with a clean predicate and an `LMLExtra` witness: allowed. The chosen
+element only depends on the predicate, not on the witness of the proof. -/
+
+noncomputable def a6_choose (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ :=
+  Classical.choose (p := fun s ↦ #s = pullCount A a t ω)
+    ⟨_, card_pullTimes (A := A) (a := a) (t := t) (ω := ω)⟩
+
+/-! Launder through an instance. Reported on `instEvil`. -/
+
+instance instEvil : Inhabited (Finset ℕ) := ⟨pullTimes (fun _ _ ↦ 0) 0 0 ()⟩
+
+noncomputable def a7_default : Finset ℕ := @default _ instEvil
+
+/-! `match`: the `LMLExtra` data ends up in the main definition. -/
+
+def a8_match (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) (n : ℕ) : Finset ℕ :=
+  match n with
+  | 0 => pullTimes A a t ω
+  | _ + 1 => ∅
+
+/-! `where` auxiliary. Reported on `a9_where.aux`. -/
+
+def a9_where (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := aux
+where aux : Finset ℕ := pullTimes A a t ω
+
+/-! `@[nolint extraData]` disables the linter on the declaration, visibly. -/
+
+@[nolint extraData]
+def a10_nolint (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := pullTimes A a t ω
+
+def a10_uses (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := a10_nolint A a t ω
+
+/-! Data smuggled through a proposition: the statement of the theorem is reported. -/
+
+theorem a11_nonempty (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) :
+    Nonempty {s : Finset ℕ // s = pullTimes A a t ω} := ⟨⟨_, rfl⟩⟩
+
+noncomputable def a11_choice (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ :=
+  (Classical.choice (a11_nonempty A a t ω)).1
+
+/-! `LMLExtra` data as an implicit argument of a `LeanMachineLearning`/Mathlib constant. -/
+
+noncomputable def a12_implicit (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : ℕ :=
+  @Finset.card ℕ (pullTimes A a t ω)
+
+/-! `opaque` with a body: the body is not unfoldable but it is what the compiled code runs. -/
+
+opaque a13_opaque (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) : Finset ℕ := pullTimes A a t ω
+
+/-! `@[implemented_by]` an `LMLExtra` definition: the logical content is clean, the compiled code
+is `LMLExtra`'s. -/
+
+@[implemented_by pullTimes]
+def a14_impl {𝓐 Ω : Type*} [DecidableEq 𝓐] (A : ℕ → Ω → 𝓐) (a : 𝓐) (t : ℕ) (ω : Ω) :
+    Finset ℕ := ∅
+
 /--
-error: -- Found 3 errors in 6 declarations (plus 1 automatically generated ones) in the current file with 1 linters
+error: -- Found 17 errors in 29 declarations (plus 18 automatically generated ones) in the current file with 1 linters
 
 /- The `extraData` linter reports:
 DECLARATIONS DEPEND ON `LMLExtra` DATA. Only theorems of `LMLExtra` may be used, and only inside proofs:
 This linter can be disabled with `@[nolint extraData]`. -/
+#check @a4_partial._unsafe_rec /- depends on `LMLExtra` data: [pullTimes] -/
+#check @WithDefault.times._default /- depends on `LMLExtra` data: [pullTimes] -/
 #check @bad_thm_statement /- depends on `LMLExtra` data: [pullTimes] -/
 #check @bad_thm_statement_prop_def /- depends on `LMLExtra` data: [WasPulled] -/
 #check @bad_def_value /- depends on `LMLExtra` data: [pullTimes] -/
+#check @_laundered /- depends on `LMLExtra` data: [pullTimes] -/
+#check @laundered /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a3_uses_default /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a5_ite /- depends on `LMLExtra` data: [WasPulled] -/
+#check instEvil /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a8_match /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a9_where.aux /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a11_nonempty /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a11_choice /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a12_implicit /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a13_opaque /- depends on `LMLExtra` data: [pullTimes] -/
+#check @a14_impl /- depends on `LMLExtra` data: [pullTimes] -/
 -/
 #guard_msgs in
 #lint only extraData
diff --git a/LeanMachineLearning/Tactic/Linter/ExtraData.lean b/LeanMachineLearning/Tactic/Linter/ExtraData.lean
index 8f7fec65..03130c13 100644
--- a/LeanMachineLearning/Tactic/Linter/ExtraData.lean
+++ b/LeanMachineLearning/Tactic/Linter/ExtraData.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Batteries.Tactic.Lint.Basic
+public meta import Lean.Compiler.ImplementedByAttr
 public meta import Lean.Meta.ForEachExpr
 
 /-!
@@ -19,11 +20,23 @@ definitions, instances, structures, inductive types, `Prop`-valued predicates...
 The `extraData` environment linter enforces this. A declaration `d` outside `LMLExtra` is
 flagged if a non-proof constant declared in an `LMLExtra` module occurs
 * in the type of `d`, or
-* if `d` is not itself a proof, in the value of `d` outside of proof subterms.
+* if `d` is not itself a proof, in the value of `d` outside of proof subterms (the body of an
+  `opaque` counts as its value, and so does the target of an `@[implemented_by]` attribute: both
+  are what the compiled code of `d` runs).
+
+The linter is applied to every constant of the environment, including private and automatically
+generated ones (structure field defaults, `match` auxiliaries, `_unsafe_rec` of `partial` defs,
+`where` auxiliaries...): a violation is reported on the constant that mentions the `LMLExtra`
+data, so it cannot be laundered through an unlinted helper.
 
 Proofs are never constrained: a proof may use any `LMLExtra` theorem, including theorems whose
 statements mention `LMLExtra` definitions.
 
+`scripts/check_extra_data.lean` runs the same check in CI, ignoring `@[nolint extraData]`: an
+attribute can be added by a metaprogram (of `LMLExtra`, since a plain `import` already runs the
+macros and elaborators of the imported module) without appearing in the source, and there is no
+legitimate exception to the rule anyway.
+
 Together with the module system this gives the intended discipline: `LeanMachineLearning` files
 import `LMLExtra` files *privately* (`import`, never `public import` nor `import all`; see
 `scripts/check_extra_imports.sh`), so that Lean already rejects `LMLExtra` constants in public
@@ -36,11 +49,11 @@ open Lean Meta Batteries.Tactic.Lint
 namespace LeanMachineLearning.Linter
 
 /-- The root module name of the `LMLExtra` library. -/
-meta def extraRoot : Name := `LMLExtra
+public meta def extraRoot : Name := `LMLExtra
 
 /-- The module in which `c` was declared (the main module for a declaration of the current
 file). -/
-meta def moduleOf (c : Name) : CoreM Name := do
+public meta def moduleOf (c : Name) : CoreM Name := do
   let env ← getEnv
   return match env.getModuleIdxFor? c with
     | some idx => env.header.moduleNames[idx]!
@@ -49,13 +62,13 @@ meta def moduleOf (c : Name) : CoreM Name := do
 /-- Is `c` declared in `LMLExtra` and not a proof, i.e. is its type not a proposition?
 Definitions, instances, structures and their projections, inductive types and their constructors,
 and `Prop`-valued predicates all qualify. Theorems do not. -/
-meta def isExtraData (c : Name) : MetaM Bool := do
+public meta def isExtraData (c : Name) : MetaM Bool := do
   unless (← moduleOf c).getRoot == extraRoot do return false
   let some ci := (← getEnv).find? c | return false
   return !(← isProp ci.type)
 
 /-- Add to `acc` the constants occurring in `e` outside of proof subterms. -/
-meta def collectDataConsts (acc : IO.Ref NameSet) (e : Expr) : MetaM Unit :=
+public meta def collectDataConsts (acc : IO.Ref NameSet) (e : Expr) : MetaM Unit :=
   forEachExpr' e fun t => do
     match t with
     | .const n _ => acc.modify (·.insert n); return false
@@ -65,13 +78,18 @@ meta def collectDataConsts (acc : IO.Ref NameSet) (e : Expr) : MetaM Unit :=
     | _ => return true
 
 /-- The constants that the declaration `d` depends on as data: those occurring in its type, and,
-if `d` is not itself a proof, those occurring in its value outside of proof subterms. -/
-meta def dataConsts (d : Name) : MetaM NameSet := do
+if `d` is not itself a proof, those occurring in its value outside of proof subterms, as well as
+the target of an `@[implemented_by]` attribute on `d`. -/
+public meta def dataConsts (d : Name) : MetaM NameSet := do
   let ci ← getConstInfo d
   let acc ← IO.mkRef ({} : NameSet)
   collectDataConsts acc ci.type
   unless ← isProp ci.type do
-    if let some v := ci.value? then collectDataConsts acc v
+    -- The body of an `opaque` is not unfoldable, but it is what its compiled code runs.
+    if let some v := ci.value? (allowOpaque := true) then collectDataConsts acc v
+    -- `@[implemented_by impl] def d` replaces the compiled code of `d` by that of `impl`.
+    if let some impl := Compiler.implementedByAttr.getParam? (← getEnv) d then
+      acc.modify (·.insert impl)
   acc.get
 
 /-- Declarations outside `LMLExtra` must not depend on data defined in `LMLExtra`.
diff --git a/scripts/check_extra_data.lean b/scripts/check_extra_data.lean
new file mode 100644
index 00000000..afb200c4
--- /dev/null
+++ b/scripts/check_extra_data.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import LeanMachineLearning.Tactic.Linter.ExtraData
+
+/-!
+# `check_extra_data`: no `LeanMachineLearning` declaration depends on `LMLExtra` data
+
+Standalone driver, for CI, of the check performed by the `extraData` environment linter
+(see `LeanMachineLearning/Tactic/Linter/ExtraData.lean`).
+
+Unlike `lake lint`, it does not honor `@[nolint extraData]`: there is no legitimate exception to
+this rule (move the definition to `LeanMachineLearning` instead), and an attribute can be added by
+a metaprogram without appearing in the source.
+
+Usage: `lake env lean --run scripts/check_extra_data.lean [Module ...]`, default
+`LeanMachineLearning`. The given modules are imported and every constant declared in a module with
+the same root as one of them is checked. Exits with code 1 if a violation is found.
+-/
+
+open Lean Meta LeanMachineLearning.Linter
+
+/-- The constants declared in a module whose root is in `roots` that depend on `LMLExtra` data,
+with the data they depend on. -/
+def findViolations (roots : List Name) : MetaM (Array (Name × List Name)) := do
+  let mut bad := #[]
+  for (c, _) in (← getEnv).constants.map₁ do
+    let root := (← moduleOf c).getRoot
+    if root == extraRoot || !roots.contains root then continue
+    let deps ← (← dataConsts c).toList.filterM isExtraData
+    unless deps.isEmpty do bad := bad.push (c, deps)
+  return bad.qsort (·.1.toString < ·.1.toString)
+
+unsafe def main (args : List String) : IO UInt32 := do
+  let modules := if args.isEmpty then [`LeanMachineLearning] else args.map String.toName
+  let roots := modules.map Name.getRoot
+  initSearchPath (← findSysroot)
+  enableInitializersExecution
+  let env ← importModules (modules.map ({ module := · })).toArray {} (trustLevel := 1024)
+    (loadExts := true)
+  let ctx : Core.Context := { fileName := "<check_extra_data>", fileMap := default }
+  let (bad, _) ← (findViolations roots).run'.toIO ctx { env }
+  if bad.isEmpty then
+    IO.println s!"OK: no declaration of {roots} depends on LMLExtra data."
+    return 0
+  IO.eprintln s!"error: {bad.size} declaration(s) depend on LMLExtra data \
+    (definitions, instances, predicates...). Only theorems of LMLExtra may be used, in proofs."
+  for (c, deps) in bad do
+    IO.eprintln s!"  {c}: {deps}"
+  return 1
diff --git a/scripts/check_extra_imports.sh b/scripts/check_extra_imports.sh
index e55006be..42b96cfd 100755
--- a/scripts/check_extra_imports.sh
+++ b/scripts/check_extra_imports.sh
@@ -1,15 +1,35 @@
 #!/usr/bin/env bash
 # `LeanMachineLearning` may only import `LMLExtra` privately, i.e. with a plain
-# `import LMLExtra.Foo`. A `public import` would re-export `LMLExtra` to every importer of the
-# file, and an `import all` would give access to the non-public declarations of the `LMLExtra`
-# file. Both would circumvent the checks that the module system performs on private imports.
+# `import LMLExtra.Foo`, and only from files using the module system.
+#
+# * `public import` would re-export `LMLExtra` to every importer of the file.
+# * `import all` would give access to the non-public declarations of the `LMLExtra` file.
+# * `meta import` would run `LMLExtra` metaprograms (macros, elaborators, initializers) while
+#   elaborating `LeanMachineLearning`.
+# * In a file that is not a `module`, every import is public and meta.
+#
+# All of these would circumvent the checks that the module system performs on private imports.
 # See `LeanMachineLearning/Tactic/Linter/ExtraData.lean`.
 set -euo pipefail
 cd "$(dirname "$0")/.."
 
-pattern='^[[:space:]]*(public[[:space:]]+(meta[[:space:]]+)?import([[:space:]]+all)?|(meta[[:space:]]+)?import[[:space:]]+all)[[:space:]]+LMLExtra([.[:space:]]|$)'
-if grep -rnE --include='*.lean' "$pattern" LeanMachineLearning LeanMachineLearning.lean; then
-  echo "error: LeanMachineLearning must import LMLExtra privately (plain 'import LMLExtra.Foo')." >&2
-  exit 1
+# Any import of `LMLExtra`, with any modifiers.
+any='^[[:space:]]*((public|meta)[[:space:]]+)*import([[:space:]]+all)?[[:space:]]+LMLExtra([.[:space:]]|$)'
+# The only allowed form: `import LMLExtra.Foo`, at the start of the line, no modifiers.
+allowed='^[0-9]+:import[[:space:]]+LMLExtra(\.[A-Za-z0-9_.]+)?[[:space:]]*(--.*)?$'
+
+status=0
+for f in $(grep -rlE --include='*.lean' "$any" LeanMachineLearning LeanMachineLearning.lean || true); do
+  if grep -nE "$any" "$f" | grep -vE "$allowed"; then
+    echo "error: $f: LMLExtra must be imported with a plain 'import LMLExtra.Foo'." >&2
+    status=1
+  fi
+  if ! grep -qE '^module([[:space:]]|$)' "$f"; then
+    echo "error: $f imports LMLExtra but is not a 'module': its imports are public and meta." >&2
+    status=1
+  fi
+done
+if [ "$status" -eq 0 ]; then
+  echo "OK: LeanMachineLearning imports LMLExtra only privately, from module files."
 fi
-echo "OK: LeanMachineLearning imports LMLExtra only privately."
+exit "$status"