demo: LMLExtra library

.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,20 @@ jobs:
           lint: true
           mk_all-check: true
 
+      # `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
+
       - name: Download referee binary
         if: github.event_name == 'push'
         env:
@@ -170,9 +187,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 +336,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

CONTRIBUTING.md

@@ -31,6 +31,24 @@ 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`, `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` 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
 
 The strength of the library lies in carefully designed and reviewed definitions.

LMLExtra.lean

@@ -0,0 +1,3 @@
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import LMLExtra.SumRewardsBounds

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

LMLTest.lean

@@ -0,0 +1 @@
+import LMLTest.ExtraDataLinter

LMLTest/ExtraDataLinter.lean

@@ -0,0 +1,179 @@
+/-
+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. 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
+
+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
+
+/-! 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 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

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

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