Quality pass: comment hygiene, helper consolidation, golf, docs+CI axiom check

.github/workflows/blueprint.yml

@@ -44,6 +44,15 @@ jobs:
         run: |
           lake build
 
+      - name: Check axioms
+        run: |
+          printf 'import Exchangeability\n#print axioms Exchangeability.DeFinetti.deFinetti\n' \
+            | lake env lean --stdin > /tmp/axioms.out
+          # Exact full-output comparison: an extra axiom or extra line fails the step.
+          diff /tmp/axioms.out - <<'EOF'
+          'Exchangeability.DeFinetti.deFinetti' depends on axioms: [propext, Classical.choice, Quot.sound]
+          EOF
+
       - name: Check declarations
         run: |
           ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

DEVELOPMENT_CHRONOLOGY.md

@@ -1,6 +1,7 @@
 # Development Chronology
 
-A narrative history of this Lean 4 formalization, based on 4,024 commits (3,166 non-merge) from Sept 29, 2025 - Jan 8, 2026.
+A narrative history of this Lean 4 formalization, based on 4,247 commits (3,373 non-merge,
+counted on `main` including merges in the total) from Sept 29, 2025 - June 8, 2026.
 
 ## Phase 0: Project Initialization (Sept 29 - Oct 1, 2025)
 
@@ -150,6 +151,25 @@ Created `DirectingMeasure.lean` infrastructure for the identification chain: a s
 2. Prepares for potential mathlib integration
 3. Professional code quality standards
 
+## Phase 11: Maintenance & Hardening (Jan 9 - June 8, 2026)
+
+**226 commits (208 non-merge, `--since="2026-01-09 00:00"` on `main`) of post-completion upkeep**
+
+- `886550af` Toolchain upgrade to Lean 4.27.0-rc1, then `8ab88df2` to v4.30.0-rc2 with
+  matching mathlib
+- Cross-tree dead-code sweeps, e.g. `b642382e` (−1,713 lines) and follow-ups — several
+  thousand lines of abandoned scaffolding removed
+- Linter hygiene: `3c40bcbf` cleared all 44 remaining linter warnings; suppressions pruned
+  in stages until `3e7b30d7` dropped the last ones (0 remaining)
+- Term-mode golf batches, e.g. `ef4e47b1` collapsing 32 `by exact` wrappers
+- `93961e6f` Canonical `Contractable.{comp, map_pair}` API; call sites migrated and the old
+  L2Helpers wrappers dropped
+- Blueprint/CI: `8f848259` PR-triggered blueprint consistency check; web + pdf artifact
+  refreshes; `289affe8` doc count/date refresh ahead of the v1.3 release
+
+**Pattern:** With all three proofs complete, work shifted from proving to curation —
+keeping the tree warning-free, current with mathlib, and honest in its documentation.
+
 ---
 
 ## Key Patterns

Exchangeability/Contractability.lean

@@ -290,10 +290,8 @@ lemma exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ)
   -- and `g` = the strictly monotone embedding via `k`.
   let f : Fin m → Fin n := Fin.castLE hmn
   let g : Fin m → Fin n := fun i => ⟨k i, hk_bound i⟩
-  have hf : Function.Injective f := Fin.castLE_injective hmn
-  have hg : Function.Injective g := fun i j hij =>
-    hk_mono.injective (Fin.mk.inj hij)
-  obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g hf hg
+  obtain ⟨σ, hσ⟩ := Equiv.Perm.exists_extending_pair f g (Fin.castLE_injective hmn)
+    (fun i j hij => hk_mono.injective (Fin.mk.inj hij))
   exact ⟨σ, fun i => congrArg Fin.val (hσ i)⟩
 
 /- Helper: relabeling coordinates by a finite permutation is measurable as a map
@@ -385,9 +383,8 @@ This follows from monotonicity and the fact that any `i` is at most `last`.
 -/
 private lemma strictMono_all_lt_succ_last {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k)
     (i : Fin m) (last : Fin m) (h_last : ∀ j, j ≤ last) :
-    k i ≤ k last := by
-  apply StrictMono.monotone hk
-  exact h_last i
+    k i ≤ k last :=
+  hk.monotone (h_last i)
 
 /--
 Helper lemma: The length of the domain is bounded by the maximum value plus one.
@@ -398,9 +395,8 @@ This uses the fact that strictly monotone functions satisfy `i ≤ k(i)` for all
 private lemma strictMono_length_le_max_succ {m : ℕ} (k : Fin m → ℕ) (hk : StrictMono k)
     (last : Fin m) (h_last_is_max : last.val + 1 = m) :
     m ≤ k last + 1 := by
-  have h_mono : last.val ≤ k last := strictMono_Fin_ge_id hk last
   calc m = last.val + 1 := h_last_is_max.symm
-       _ ≤ k last + 1 := Nat.add_le_add_right h_mono 1
+       _ ≤ k last + 1 := Nat.add_le_add_right (strictMono_Fin_ge_id hk last) 1
 
 /--
 **Main theorem:** Every exchangeable sequence is contractable.

Exchangeability/Core.lean

@@ -208,15 +208,11 @@ private lemma cylinder_subset_prefixCylinders {s : Finset ℕ} {S : Set (∀ _ :
     intro i hi
     have hle : i ≤ s.sup id := by convert Finset.le_sup (f := id) hi
     omega
-  -- Transport `S` along the inclusion into the initial segment.
-  let ι : s → Fin N := fun x => ⟨x.1, h_mem x.1 x.2⟩
-  let pull : (Fin N → α) → (∀ i : s, α) := fun x => fun y => x (ι y)
+  -- Transport `S` along the inclusion into the initial segment; the cylinder is
+  -- definitionally the prefix cylinder of the pulled-back set.
+  let pull : (Fin N → α) → (∀ i : s, α) := fun x => fun y => x ⟨y.1, h_mem y.1 y.2⟩
   have hpull_meas : Measurable pull := by fun_prop
-  have hs_eq :
-      MeasureTheory.cylinder (α:=fun _ : ℕ => α) s S =
-        prefixCylinder (α:=α) (pull ⁻¹' S) := rfl
-  refine hs_eq ▸ prefixCylinder_mem_prefixCylinders (α:=α) ?_
-  exact hpull_meas hS
+  exact prefixCylinder_mem_prefixCylinders (α:=α) (hpull_meas hS)
 
 /--
 The σ-algebra generated by prefix cylinders is the product σ-algebra.

Exchangeability/DeFinetti/CommonEnding.lean

@@ -425,8 +425,6 @@ theorem conditional_iid_from_directing_measure
       exact fidi_eq_avg_product X hX_meas ν hν_prob hν_meas m k B hB_meas
         (h_bridge (k := k) hk_strict.injective (B := B) hB_meas)
 
--- *Monotone-class remark.*  Earlier drafts included an explicit monotone-class lemma
--- (`monotone_class_product_extension`) proving the π-λ step described above.  The sole
--- remaining use of that lemma is captured abstractly by the `h_bridge` hypothesis, so the
--- sketch is retained only as commentary.
+-- *Monotone-class remark.*  The π-λ step described above is captured abstractly by the
+-- `h_bridge` hypothesis, so no explicit monotone-class lemma is needed here.
 end Exchangeability.DeFinetti.CommonEnding

Exchangeability/DeFinetti/L2Helpers.lean

@@ -24,8 +24,8 @@ All lemmas here are complete (no sorries) and compile cleanly.
 - Various arithmetic bounds for convergence rates (e.g. `sqrt_div_lt_half_eps_of_nat`)
 - Fin index reindexing lemmas for filtered sums
 
-The contractability/covariance helpers that previously lived here have moved to the
-canonical `Exchangeability.Contractable.{map_single, map_pair, comp}` API in
+For contractability/covariance helpers, see the canonical
+`Exchangeability.Contractable.{map_single, map_pair, comp}` API in
 `Exchangeability/Contractability.lean`.
 
 -/

Exchangeability/DeFinetti/ViaKoopman/CesaroHelpers.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cameron Freer
 -/
 import Exchangeability.DeFinetti.ViaKoopman.Infrastructure
-import Exchangeability.DeFinetti.ViaKoopman.LpCondExpHelpers
+import Exchangeability.Probability.LpNormHelpers
 
 /-! # Cesàro Helper Lemmas
 
@@ -36,6 +36,25 @@ variable {α : Type*} [MeasurableSpace α]
 -- Short notation for shift-invariant σ-algebra (used throughout this file)
 local notation "mSI" => shiftInvariantSigma (α := α)
 
+/-- Finite sum linearity of conditional expectation, stated with the sum applied
+pointwise (`fun ω => ∑ i ∈ s, f i ω`) as it appears in the Cesàro averages below.
+η-expands to mathlib's `condExp_finset_sum`. -/
+private lemma condExp_sum_finset
+    {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
+    {m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
+    {ι : Type*} (s : Finset ι) (f : ι → Ω → ℝ)
+    (hint : ∀ i ∈ s, Integrable (f i) μ) :
+    μ[(fun ω => s.sum (fun i => f i ω)) | m]
+      =ᵐ[μ] (fun ω => s.sum (fun i => μ[f i | m] ω)) := by
+  classical
+  have h_sum_eta : (fun ω => ∑ i ∈ s, f i ω) = ∑ i ∈ s, f i := by
+    funext ω
+    simp only [Finset.sum_apply]
+  have h_ce_sum_eta : (fun ω => ∑ i ∈ s, μ[f i | m] ω) = ∑ i ∈ s, μ[f i | m] := by
+    funext ω
+    simp only [Finset.sum_apply]
+  rw [h_sum_eta, h_ce_sum_eta]
+  exact condExp_finset_sum hint m
 
 lemma condexp_precomp_iterate_eq
     {μ : Measure (Ω[α])} [IsProbabilityMeasure μ]
@@ -321,8 +340,8 @@ lemma product_ce_constant_of_lag_const
          = (fun ω => (1 / ((n + 1) : ℝ)) * (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j))) := by
       funext ω; simp [A, Finset.mul_sum, mul_comm, mul_left_comm, mul_assoc]
     rw [this]
-    exact condExp_const_mul (shiftInvariantSigma_le (α := α))
-      (1 / ((n + 1) : ℝ)) (fun ω => (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j)))
+    simpa [Pi.mul_apply, smul_eq_mul] using condExp_smul (μ := μ)
+      (1 / ((n + 1) : ℝ)) (fun ω => (Finset.range (n + 1)).sum (fun j => f (ω 0) * g (ω j))) mSI
 
   -- Push CE through the finite sum
   have h_sum :
@@ -460,8 +479,8 @@ lemma product_ce_constant_of_lag_const_from_one
          = (fun ω => (1 / (n : ℝ)) * (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1)))) := by
       funext ω; simp [A', Finset.mul_sum, mul_left_comm]
     rw [this]
-    exact condExp_const_mul (shiftInvariantSigma_le (α := α))
-      (1 / (n : ℝ)) (fun ω => (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1))))
+    simpa [Pi.mul_apply, smul_eq_mul] using condExp_smul (μ := μ)
+      (1 / (n : ℝ)) (fun ω => (Finset.range n).sum (fun j => f (ω 0) * g (ω (j + 1)))) mSI
 
   -- Push CE through the finite sum
   have h_sum :

Exchangeability/DeFinetti/ViaKoopman/README.md

@@ -32,7 +32,6 @@ This directory contains Kallenberg's "first proof" of de Finetti's theorem, usin
 | `BlockInjection.lean` | Block injection lemmas |
 | `KernelBridge.lean` | Bridge lemma for kernel measures |
 | `CylinderFunctions.lean` | Cylinder function definitions |
-| `LpCondExpHelpers.lean` | Lᵖ conditional expectation helpers |
 | `DirectingKernel.lean` | Directing measure from CE kernel |
 | `Quantization.lean` | Quantization machinery |
 | `Infrastructure.lean` | Basic definitions |

Exchangeability/DeFinetti/ViaL2/AlphaConvergence/AlphaIicEq.lean

@@ -34,8 +34,8 @@ variable {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
 
 /-- Clipping `b` to `[0,1]` can only bring it closer to anything already in `[0,1]`.
 
-Internal helper: factors out the case analysis that previously appeared in
-`alphaIic_ae_eq_alphaIicCE`. The cleanest route is via mathlib's
+Internal helper for the case analysis in `alphaIic_ae_eq_alphaIicCE`.
+The cleanest route is via mathlib's
 `LipschitzWith.projIcc`: `Set.projIcc 0 1` is `1`-Lipschitz, equals
 `max 0 (min 1 ·)` after coercion, and fixes any input already in `[0,1]`. -/
 private lemma abs_sub_clip01_le_of_mem {a b : ℝ} (ha : a ∈ Set.Icc (0 : ℝ) 1) :

Exchangeability/DeFinetti/ViaL2/AlphaIicCE.lean

@@ -78,10 +78,9 @@ noncomputable def alphaIicCE
 
 /-- Measurability of alphaIicCE.
 
-Note: Previously had BorelSpace typeclass instance resolution issues.
-The conditional expectation `condExp μ (tailSigma X) f` is measurable by
-`stronglyMeasurable_condExp.measurable`, but Lean can't synthesize the required
-`BorelSpace` instance automatically. This should be straightforward to fix. -/
+The conditional expectation is strongly measurable with respect to the tail σ-algebra
+(`stronglyMeasurable_condExp`), and `Measurable.mono` lifts this to the ambient
+σ-algebra via `tailProcess_le_ambient`. -/
 @[measurability, fun_prop]
 lemma alphaIicCE_measurable
     {μ : Measure Ω} [IsProbabilityMeasure μ]

Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean

@@ -44,8 +44,8 @@ variable {Ω α : Type*} [MeasurableSpace Ω] [MeasurableSpace α]
 
 The proof routes through the kernel-level bridge
 `directing_measure_ae_eq_condExpKernel_map` and mathlib's
-`condExp_ae_eq_integral_condExpKernel`, replacing what was previously a hand-built
-monotone-class extension from `Iic` indicators.
+`condExp_ae_eq_integral_condExpKernel`, so no monotone-class extension from `Iic`
+indicators is needed.
 
 The `[StandardBorelSpace Ω]` assumption comes from `condExpKernel`. -/
 lemma directing_measure_integral_eq_condExp

Exchangeability/Probability/IntegrationHelpers.lean

@@ -193,4 +193,30 @@ lemma integral_pushforward_sq_diff
   rw [integral_map hf.aemeasurable]
   exact (continuous_id.sub continuous_const).pow 2 |>.aestronglyMeasurable
 
+/-! ## Fatou-Type Lemmas -/
+
+/-- Fatou's lemma on `ENNReal.ofReal ∘ ‖·‖` along an a.e. pointwise limit.
+
+If `u n x → g x` a.e., then `∫⁻ ‖g‖ ≤ liminf (∫⁻ ‖u n‖)`. -/
+lemma lintegral_fatou_ofReal_norm
+  {α β : Type*} [MeasurableSpace α] {μ : Measure α}
+  [MeasurableSpace β] [NormedAddCommGroup β] [BorelSpace β]
+  {u : ℕ → α → β} {g : α → β}
+  (hae : ∀ᵐ x ∂μ, Tendsto (fun n => u n x) atTop (nhds (g x)))
+  (hu_meas : ∀ n, AEMeasurable (fun x => ENNReal.ofReal ‖u n x‖) μ)
+  (_hg_meas : AEMeasurable (fun x => ENNReal.ofReal ‖g x‖) μ) :
+  ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
+    ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop := by
+  have hae_ofReal :
+      ∀ᵐ x ∂μ,
+        Tendsto (fun n => ENNReal.ofReal ‖u n x‖) atTop
+                (nhds (ENNReal.ofReal ‖g x‖)) :=
+    hae.mono (fun x hx =>
+      ((ENNReal.continuous_ofReal.comp continuous_norm).tendsto _).comp hx)
+  calc ∫⁻ x, ENNReal.ofReal ‖g x‖ ∂μ
+      = ∫⁻ x, liminf (fun n => ENNReal.ofReal ‖u n x‖) atTop ∂μ :=
+          lintegral_congr_ae (hae_ofReal.mono fun x hx => hx.liminf_eq.symm)
+    _ ≤ liminf (fun n => ∫⁻ x, ENNReal.ofReal ‖u n x‖ ∂μ) atTop :=
+          lintegral_liminf_le' hu_meas
+
 end Exchangeability.Probability.IntegrationHelpers