diff --git a/Laplace/TwoD/AddSeparable.lean b/Laplace/TwoD/AddSeparable.lean index 178129a..ec08770 100644 --- a/Laplace/TwoD/AddSeparable.lean +++ b/Laplace/TwoD/AddSeparable.lean @@ -55,12 +55,12 @@ lemma exp_neg_t_addSeparable_eq_mul (U V : ℝ → ℝ) (t : ℝ) (z : ℝ × show (-(t * (U z.1 + V z.2)) : ℝ) = -(t * U z.1) + -(t * V z.2) from by ring, Real.exp_add] -/-- **Partition-function factorisation**: under integrability of each marginal -Boltzmann weight, `Z_2D(t) = Z_U(t) · Z_V(t)`. -/ +/-- **Partition-function factorisation**: `Z_2D(t) = Z_U(t) · Z_V(t)`. +Unconditional: `MeasureTheory.integral_prod_mul` is unconditional, so the +factorisation holds even when the 1D weights are not Lebesgue-integrable +(both sides are `0` by Bochner convention in that case). -/ theorem partitionFunction_addSeparable_factor - {U V : ℝ → ℝ} {t : ℝ} - (_hU : Integrable (fun x : ℝ => Real.exp (-(t * U x)))) - (_hV : Integrable (fun y : ℝ => Real.exp (-(t * V y)))) : + (U V : ℝ → ℝ) (t : ℝ) : partitionFunction (addSeparable U V) t = Laplace.partitionFunction U t * Laplace.partitionFunction V t := by unfold partitionFunction Laplace.partitionFunction @@ -73,11 +73,10 @@ theorem partitionFunction_addSeparable_factor (g := fun y : ℝ => Real.exp (-(t * V y))) /-- **Separable-observable factorisation**: for an integrand `f(x) · g(y) · e^{-tL}`, -the 2D integral factors as a product of 1D weighted integrals. -/ +the 2D integral factors as a product of 1D weighted integrals. +Unconditional, for the same reason as `partitionFunction_addSeparable_factor`. -/ theorem integral_separable_addSeparable - {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ) - (_hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x)))) - (_hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) : + (U V : ℝ → ℝ) (t : ℝ) (f g : ℝ → ℝ) : (∫ z : ℝ × ℝ, f z.1 * g z.2 * Real.exp (-(t * addSeparable U V z))) = (∫ x : ℝ, f x * Real.exp (-(t * U x))) * (∫ y : ℝ, g y * Real.exp (-(t * V y))) := by @@ -97,17 +96,13 @@ nonzero, the 2D Gibbs expectation of a separable observable factors. -/ theorem gibbsExpectation_separable_addSeparable {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ) (hZU_ne : Laplace.partitionFunction U t ≠ 0) - (hZV_ne : Laplace.partitionFunction V t ≠ 0) - (hU : Integrable (fun x : ℝ => Real.exp (-(t * U x)))) - (hV : Integrable (fun y : ℝ => Real.exp (-(t * V y)))) - (hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x)))) - (hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) : + (hZV_ne : Laplace.partitionFunction V t ≠ 0) : gibbsExpectation (addSeparable U V) t (fun z => f z.1 * g z.2) = Laplace.gibbsExpectation U t f * Laplace.gibbsExpectation V t g := by unfold gibbsExpectation Laplace.gibbsExpectation - rw [partitionFunction_addSeparable_factor hU hV] - rw [integral_separable_addSeparable f g hf hg] + rw [partitionFunction_addSeparable_factor] + rw [integral_separable_addSeparable] field_simp /-- **Mixed-covariance vanishing**: under a product/separable Gibbs measure, @@ -116,24 +111,17 @@ observable is zero. The structural payoff of separability. -/ theorem gibbsCov_addSeparable_fst_snd_eq_zero {U V : ℝ → ℝ} {t : ℝ} (f g : ℝ → ℝ) (hZU_ne : Laplace.partitionFunction U t ≠ 0) - (hZV_ne : Laplace.partitionFunction V t ≠ 0) - (hU : Integrable (fun x : ℝ => Real.exp (-(t * U x)))) - (hV : Integrable (fun y : ℝ => Real.exp (-(t * V y)))) - (hf : Integrable (fun x : ℝ => f x * Real.exp (-(t * U x)))) - (hg : Integrable (fun y : ℝ => g y * Real.exp (-(t * V y)))) : + (hZV_ne : Laplace.partitionFunction V t ≠ 0) : gibbsCov (addSeparable U V) t (fun z => f z.1) (fun z => g z.2) = 0 := by unfold gibbsCov -- Step 1: ⟨f(z.1) · g(z.2)⟩ = ⟨f⟩_U · ⟨g⟩_V (separable-observable factorisation). - rw [show (fun z : ℝ × ℝ => f z.1 * g z.2) = - (fun z : ℝ × ℝ => f z.1 * g z.2) from rfl] - rw [gibbsExpectation_separable_addSeparable f g hZU_ne hZV_ne hU hV hf hg] + rw [gibbsExpectation_separable_addSeparable f g hZU_ne hZV_ne] -- Step 2: ⟨f(z.1)⟩_2D = ⟨f⟩_U (collapse with g = 1). have hExp_f : gibbsExpectation (addSeparable U V) t (fun z => f z.1) = Laplace.gibbsExpectation U t f := by have h := gibbsExpectation_separable_addSeparable f (fun _ => (1 : ℝ)) - hZU_ne hZV_ne hU hV hf - (by simpa using hV) + hZU_ne hZV_ne have hg1 : Laplace.gibbsExpectation V t (fun _ => (1 : ℝ)) = 1 := Laplace.gibbsExpectation_const V t 1 hZV_ne rw [show (fun z : ℝ × ℝ => f z.1 * (1 : ℝ)) = (fun z : ℝ × ℝ => f z.1) from by @@ -143,8 +131,7 @@ theorem gibbsCov_addSeparable_fst_snd_eq_zero have hExp_g : gibbsExpectation (addSeparable U V) t (fun z => g z.2) = Laplace.gibbsExpectation V t g := by have h := gibbsExpectation_separable_addSeparable (fun _ => (1 : ℝ)) g - hZU_ne hZV_ne hU hV - (by simpa using hU) hg + hZU_ne hZV_ne have hf1 : Laplace.gibbsExpectation U t (fun _ => (1 : ℝ)) = 1 := Laplace.gibbsExpectation_const U t 1 hZU_ne rw [show (fun z : ℝ × ℝ => (1 : ℝ) * g z.2) = (fun z : ℝ × ℝ => g z.2) from by diff --git a/Laplace/TwoD/PureQuartic.lean b/Laplace/TwoD/PureQuartic.lean index 845a705..0daa119 100644 --- a/Laplace/TwoD/PureQuartic.lean +++ b/Laplace/TwoD/PureQuartic.lean @@ -65,35 +65,38 @@ noncomputable def pureQuarticPotential : ℝ × ℝ → ℝ := /-! ## Boltzmann factor decomposition -/ +/-! ## Bridge to the additively-separable abstraction -/ + +/-- The pure-quartic 2D potential is an additively-separable potential +with both marginals equal to the 1D quartic. -/ +@[simp] lemma pureQuarticPotential_eq_addSeparable : + pureQuarticPotential = + addSeparable Laplace.OneD.quarticPotential Laplace.OneD.quarticPotential := by + funext z + simp only [pureQuarticPotential_apply, addSeparable_apply, + Laplace.OneD.quarticPotential_apply] + /-- The Boltzmann factor for `L(x,y) = x⁴/24 + y⁴/24` factorises as a product -of quartic factors in `x` and `y`. -/ +of quartic factors in `x` and `y`. Corollary of `exp_neg_t_addSeparable_eq_mul` +via the bridge above. -/ lemma exp_neg_t_pureQuartic_eq_mul (t : ℝ) (z : ℝ × ℝ) : Real.exp (-(t * pureQuarticPotential z)) = Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) * Real.exp (-(t * Laplace.OneD.quarticPotential z.2)) := by - rw [pureQuarticPotential_apply, Laplace.OneD.quarticPotential_apply, - Laplace.OneD.quarticPotential_apply] - rw [show -(t * (z.1 ^ 4 / 24 + z.2 ^ 4 / 24)) = - -(t * (z.1 ^ 4 / 24)) + -(t * (z.2 ^ 4 / 24)) from by ring] - exact Real.exp_add _ _ + rw [pureQuarticPotential_eq_addSeparable] + exact exp_neg_t_addSeparable_eq_mul _ _ t z /-! ## Partition function factorisation -/ /-- The 2D partition function factorises into the square of the 1D quartic -partition function. -/ +partition function. Application of `partitionFunction_addSeparable_factor` +via the bridge. -/ theorem partitionFunction_factor (t : ℝ) : partitionFunction pureQuarticPotential t = Laplace.partitionFunction Laplace.OneD.quarticPotential t * Laplace.partitionFunction Laplace.OneD.quarticPotential t := by - unfold partitionFunction Laplace.partitionFunction - rw [show (fun z : ℝ × ℝ => Real.exp (-(t * pureQuarticPotential z))) = - (fun z : ℝ × ℝ => - Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) * - Real.exp (-(t * Laplace.OneD.quarticPotential z.2))) from by - funext z; exact exp_neg_t_pureQuartic_eq_mul t z] - exact MeasureTheory.integral_prod_mul - (f := fun x : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential x))) - (g := fun y : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential y))) + rw [pureQuarticPotential_eq_addSeparable] + exact partitionFunction_addSeparable_factor _ _ _ /-- Closed form for the partition function: `Z_2D(t) = ((1/2) · (24/t)^{1/4} · Γ(1/4))²`. -/ @@ -114,23 +117,15 @@ theorem partitionFunction_pos {t : ℝ} (ht : 0 < t) : /-- The 2D moment integral of a separable monomial `z.1^m · z.2^n` against the pure-quartic Gibbs weight factorises into the product of 1D moment -integrals. -/ +integrals. Application of `integral_separable_addSeparable` at +`f = fun x ↦ x^m`, `g = fun y ↦ y^n` via the bridge. -/ theorem integral_pow_pow_factor (t : ℝ) (m n : ℕ) : (∫ z : ℝ × ℝ, z.1 ^ m * z.2 ^ n * Real.exp (-(t * pureQuarticPotential z))) = (∫ x : ℝ, x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) * (∫ y : ℝ, y ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential y))) := by - rw [show (fun z : ℝ × ℝ => z.1 ^ m * z.2 ^ n * - Real.exp (-(t * pureQuarticPotential z))) = - (fun z : ℝ × ℝ => - (z.1 ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential z.1))) * - (z.2 ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential z.2)))) from by - funext z - rw [exp_neg_t_pureQuartic_eq_mul t z] - ring] - exact MeasureTheory.integral_prod_mul - (f := fun x : ℝ => x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) - (g := fun y : ℝ => y ^ n * Real.exp (-(t * Laplace.OneD.quarticPotential y))) + simp only [pureQuarticPotential_eq_addSeparable] + exact integral_separable_addSeparable _ _ _ (fun x => x ^ m) (fun y => y ^ n) /-! ## Specialised moments needed for affine covariance -/ diff --git a/Laplace/TwoD/SemiDegenerate.lean b/Laplace/TwoD/SemiDegenerate.lean index 637526c..774f782 100644 --- a/Laplace/TwoD/SemiDegenerate.lean +++ b/Laplace/TwoD/SemiDegenerate.lean @@ -73,39 +73,43 @@ noncomputable def semiDegeneratePotential (lam : ℝ) : ℝ × ℝ → ℝ := @[simp] lemma semiDegeneratePotential_apply (lam : ℝ) (z : ℝ × ℝ) : semiDegeneratePotential lam z = lam / 2 * z.2 ^ 2 + z.1 ^ 4 / 24 := rfl +/-! ## Bridge to the additively-separable abstraction -/ + +/-- The semi-degenerate potential is an additively-separable potential +with `U = quartic` and `V = harmonic`. -/ +@[simp] lemma semiDegeneratePotential_eq_addSeparable (lam : ℝ) : + semiDegeneratePotential lam = + addSeparable Laplace.OneD.quarticPotential + (Laplace.OneD.harmonicPotential lam) := by + funext z + simp only [semiDegeneratePotential_apply, addSeparable_apply, + Laplace.OneD.quarticPotential_apply] + unfold Laplace.OneD.harmonicPotential + ring + /-! ## Boltzmann factor decomposition -/ /-- The Boltzmann factor for `L(x,y) = (λ/2)y² + x⁴/24` factorises as a -product of a quartic factor in `x` and a harmonic factor in `y`. -/ +product of a quartic factor in `x` and a harmonic factor in `y`. Corollary +of `exp_neg_t_addSeparable_eq_mul` via the bridge above. -/ lemma exp_neg_t_semiDegenerate_eq_mul (lam t : ℝ) (z : ℝ × ℝ) : Real.exp (-(t * semiDegeneratePotential lam z)) = Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) * Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2)) := by - rw [semiDegeneratePotential_apply, Laplace.OneD.quarticPotential_apply] - unfold Laplace.OneD.harmonicPotential - rw [show -(t * (lam / 2 * z.2 ^ 2 + z.1 ^ 4 / 24)) = - -(t * (z.1 ^ 4 / 24)) + -(t * (lam / 2 * z.2 ^ 2)) from by ring] - exact Real.exp_add _ _ + rw [semiDegeneratePotential_eq_addSeparable] + exact exp_neg_t_addSeparable_eq_mul _ _ t z /-! ## Partition function factorisation -/ /-- The 2D partition function factorises into the product of the 1D -quartic and 1D harmonic partition functions. -/ +quartic and 1D harmonic partition functions. Application of +`partitionFunction_addSeparable_factor` via the bridge. -/ theorem partitionFunction_factor (lam t : ℝ) : partitionFunction (semiDegeneratePotential lam) t = Laplace.partitionFunction Laplace.OneD.quarticPotential t * Laplace.partitionFunction (Laplace.OneD.harmonicPotential lam) t := by - unfold partitionFunction Laplace.partitionFunction - -- Decompose the Boltzmann factor pointwise. - rw [show (fun z : ℝ × ℝ => Real.exp (-(t * semiDegeneratePotential lam z))) = - (fun z : ℝ × ℝ => - Real.exp (-(t * Laplace.OneD.quarticPotential z.1)) * - Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2))) from by - funext z; exact exp_neg_t_semiDegenerate_eq_mul lam t z] - -- Apply Fubini-style factorisation for product integrals of separable functions. - exact MeasureTheory.integral_prod_mul - (f := fun x : ℝ => Real.exp (-(t * Laplace.OneD.quarticPotential x))) - (g := fun y : ℝ => Real.exp (-(t * Laplace.OneD.harmonicPotential lam y))) + rw [semiDegeneratePotential_eq_addSeparable] + exact partitionFunction_addSeparable_factor _ _ _ /-- Closed form for the partition function: `Z_2D(t) = (1/2)·(24/t)^{1/4}·Γ(1/4)·√(2π/(λt))`. -/ theorem partitionFunction_closed_form {lam t : ℝ} (hlam : 0 < lam) (ht : 0 < t) : @@ -126,23 +130,15 @@ theorem partitionFunction_pos {lam t : ℝ} (hlam : 0 < lam) (ht : 0 < t) : /-- The 2D moment integral of a separable monomial `z.1^m · z.2^n` against the semi-degenerate Gibbs weight factorises into the product of 1D -moment integrals. -/ +moment integrals. Application of `integral_separable_addSeparable` at +`f = fun x ↦ x^m`, `g = fun y ↦ y^n` via the bridge. -/ theorem integral_pow_pow_factor (lam t : ℝ) (m n : ℕ) : (∫ z : ℝ × ℝ, z.1 ^ m * z.2 ^ n * Real.exp (-(t * semiDegeneratePotential lam z))) = (∫ x : ℝ, x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) * (∫ y : ℝ, y ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam y))) := by - rw [show (fun z : ℝ × ℝ => z.1 ^ m * z.2 ^ n * - Real.exp (-(t * semiDegeneratePotential lam z))) = - (fun z : ℝ × ℝ => - (z.1 ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential z.1))) * - (z.2 ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam z.2)))) from by - funext z - rw [exp_neg_t_semiDegenerate_eq_mul lam t z] - ring] - exact MeasureTheory.integral_prod_mul - (f := fun x : ℝ => x ^ m * Real.exp (-(t * Laplace.OneD.quarticPotential x))) - (g := fun y : ℝ => y ^ n * Real.exp (-(t * Laplace.OneD.harmonicPotential lam y))) + simp only [semiDegeneratePotential_eq_addSeparable] + exact integral_separable_addSeparable _ _ _ (fun x => x ^ m) (fun y => y ^ n) /-! ## Specialised moments needed for affine covariance -/ diff --git a/retrospectives/2026-05-06-tide-twod-cleanup.pdf b/retrospectives/2026-05-06-tide-twod-cleanup.pdf new file mode 100644 index 0000000..14f553b Binary files /dev/null and b/retrospectives/2026-05-06-tide-twod-cleanup.pdf differ diff --git a/retrospectives/2026-05-06-tide-twod-cleanup.tex b/retrospectives/2026-05-06-tide-twod-cleanup.tex new file mode 100644 index 0000000..5320ce4 --- /dev/null +++ b/retrospectives/2026-05-06-tide-twod-cleanup.tex @@ -0,0 +1,289 @@ +\documentclass[11pt]{article} +\usepackage[utf8]{inputenc} +\usepackage{amsmath,amssymb,amsthm} +\usepackage[margin=1in]{geometry} +\usepackage{hyperref} +\usepackage{xcolor} +\usepackage{enumitem} +\usepackage{newunicodechar} +\newunicodechar{ℝ}{\ensuremath{\mathbb{R}}} +\newunicodechar{⟨}{\ensuremath{\langle}} +\newunicodechar{⟩}{\ensuremath{\rangle}} +\newunicodechar{Γ}{\ensuremath{\Gamma}} +\newunicodechar{·}{\ensuremath{\cdot}} +\newunicodechar{²}{\ensuremath{^2}} +\newunicodechar{ψ}{\ensuremath{\psi}} +\newunicodechar{φ}{\ensuremath{\varphi}} +\newunicodechar{λ}{\ensuremath{\lambda}} +\newunicodechar{≠}{\ensuremath{\ne}} + +\setlength{\emergencystretch}{3em} + +\newcommand{\userbox}[1]{\par\medskip\begin{quote}\small\textbf{\textcolor{blue!60}{DM:}} #1\end{quote}\medskip} +\newcommand{\claudebox}[1]{\par\medskip\begin{quote}\small\textbf{\textcolor{orange!60!black}{Claude:}} #1\end{quote}\medskip} +\newcommand{\gptbox}[1]{\par\medskip\begin{quote}\small\textbf{\textcolor{green!50!black}{GPT-5.5 Pro:}} #1\end{quote}\medskip} + +\title{Tide retrospective:\\\emph{2D cleanup --- refactor through AddSeparable}} +\author{Daniel Murfet (with Claude Opus 4.7)} +\date{6 May 2026} + +\begin{document} +\maketitle + +\begin{abstract} +A cleanup Tide chained on top of Tide 12 (separable-potential +abstraction). The two existing 2D files +(\texttt{SemiDegenerate.lean}, \texttt{PureQuartic.lean}) are refactored +to apply the new \texttt{AddSeparable} lemmas via small +\texttt{[simp]}-tagged bridge lemmas, instead of re-deriving +\texttt{integral\_prod\_mul} plumbing case-by-case. Net delta is +$-22$ lines across three files (the abstraction itself shed an unused +hypothesis package). Public theorem statements unchanged on the +headline \texttt{cov\_affine\_*} and moment lemmas; only internal proof +structure changes. Build green on first compile, zero +\texttt{sorry}/\texttt{axiom}/\texttt{native\_decide}. The interesting +process moves were two: a deliberate API regression on +\texttt{AddSeparable} (drop hypotheses that Tide 12 added as +discipline; the concrete refactor demonstrated they blocked rather +than helped downstream callers), and a worktree-isolated tide run that +confirmed the structural fix to the recurring concurrent-agent branch +race. +\end{abstract} + +\section{Setting} + +This is a cleanup Tide rather than a step outward. Tide 12 landed the +\texttt{Laplace.TwoD.AddSeparable} module, which exposes for any +$L(x, y) = U(x) + V(y)$ the generic factorisations +$Z_{2D}(t) = Z_U(t) \cdot Z_V(t)$ and $\langle f \otimes g \rangle = +\langle f \rangle_U \cdot \langle g \rangle_V$. Two existing 2D files +(\texttt{SemiDegenerate.lean}, $L = (\lambda/2) y^2 + x^4/24$, 514 +lines; \texttt{PureQuartic.lean}, $L = x^4/24 + y^4/24$, 478 lines) +re-derived these as case-by-case proofs. The cleanup Tide refactors +both files to apply the abstraction's lemmas through a small +\texttt{[simp]} bridge lemma, leaving the public theorem statements +intact. + +The Tide chains on top of \texttt{tide/separable-potential} per the +linear-chain branch-hygiene rule; the new branch is +\texttt{tide/twod-cleanup}, off Tide 12's tip +\texttt{725c76b}. The Tide ran in a dedicated \texttt{git worktree} at +\texttt{lean/laplace-cleanup/} --- the first concrete application of +the worktree-isolation fix that three prior retrospectives have +recommended in response to the recurring concurrent-agent branch race. + +\section{The thing formalised} + +Three pieces, in order: + +\paragraph{1. \texttt{AddSeparable.lean} API tightening.} +The \texttt{partitionFunction\_addSeparable\_factor} and +\texttt{integral\_separable\_addSeparable} lemmas drop their +integrability hypotheses, becoming unconditional (matching Mathlib's +\texttt{integral\_prod\_mul}, which is itself unconditional). The +\texttt{gibbsExpectation\_separable\_addSeparable} and +\texttt{gibbsCov\_addSeparable\_fst\_snd\_eq\_zero} lemmas drop the +weight integrability hypotheses but keep the partition-function +nonzero hypotheses (those are load-bearing --- needed to divide). + +\paragraph{2. \texttt{SemiDegenerate.lean} refactor.} +A new \texttt{[simp]}-tagged bridge lemma: +\begin{verbatim} +lemma semiDegeneratePotential_eq_addSeparable (lam : ℝ) : + semiDegeneratePotential lam = + addSeparable Laplace.OneD.quarticPotential + (Laplace.OneD.harmonicPotential lam) +\end{verbatim} +Then \texttt{partitionFunction\_factor} and +\texttt{integral\_pow\_pow\_factor} become two-line proofs each: +\begin{verbatim} +theorem partitionFunction_factor (lam t : ℝ) : ... := by + rw [semiDegeneratePotential_eq_addSeparable] + exact partitionFunction_addSeparable_factor _ _ _ + +theorem integral_pow_pow_factor (lam t : ℝ) (m n : ℕ) : ... := by + simp only [semiDegeneratePotential_eq_addSeparable] + exact integral_separable_addSeparable _ _ _ (fun x => x ^ m) (fun y => y ^ n) +\end{verbatim} +The \texttt{exp\_neg\_t\_semiDegenerate\_eq\_mul} lemma becomes a +similar two-line corollary of +\texttt{exp\_neg\_t\_addSeparable\_eq\_mul}. + +\paragraph{3. \texttt{PureQuartic.lean} refactor.} +Mirror of step 2 with \texttt{pureQuarticPotential\_eq\_addSeparable} +as the bridge. + +\paragraph{Public statements unchanged.} The \texttt{cov\_affine\_*} +theorems and the moment lemmas +(\texttt{gibbsExpectation\_fst}/\texttt{snd}/\texttt{fst\_mul\_snd}/\texttt{fst\_sq}/\texttt{snd\_sq}) +are unchanged in statement and continue to typecheck through the +refactored proofs. Net delta: $-22$ lines across the three files (64 +insertions, 86 deletions). + +\section{Proof strategy} + +The cleanup pivots on two simple observations: + +\begin{enumerate} +\item \textbf{The bridge lemma is \texttt{[simp]}-tagged.} + The semi-degenerate potential and the corresponding + \texttt{addSeparable} are pointwise equal as functions $\mathbb{R} + \times \mathbb{R} \to \mathbb{R}$. Tagging the equation + \texttt{[simp]} lets a single \texttt{simp only} rewrite the + integrand of \texttt{integral\_pow\_pow\_factor} from the named + potential to the \texttt{addSeparable} form, after which the + AddSeparable lemma applies directly. +\item \textbf{Beta-reduction handles the lambda shapes.} + \texttt{integral\_separable\_addSeparable U V t f g} expects $f, g : + \mathbb{R} \to \mathbb{R}$. To recover the existing + \texttt{integral\_pow\_pow\_factor} statement, we apply at $f = (x + \mapsto x^m)$, $g = (y \mapsto y^n)$. Lean beta-reduces \texttt{(fun + x => x ^ m) z.1} to \texttt{z.1 ^ m} automatically. +\end{enumerate} + +The API regression on \texttt{AddSeparable.lean} (dropping the +integrability hypotheses) is a separate move: the underlying proof +bodies were already unconditional via Mathlib's +\texttt{integral\_prod\_mul}; the hypotheses had been added in Tide 12 +as documentation discipline, not load-bearing. The cleanup Tide's +concrete downstream demonstrates that the hypothesis-bearing form +\emph{blocks} the bridge-rewrite, since the existing +\texttt{partitionFunction\_factor} statements have no positivity +hypotheses to source the integrability witnesses from. The simplest +fix is to drop the discipline. + +\section{Roadblocks and resolutions} + +\paragraph{The hypothesis package on \texttt{AddSeparable} blocks the +refactor.} +Tide 12 added \texttt{Integrable} hypotheses to +\texttt{partitionFunction\_addSeparable\_factor} and friends, on +GPT-5.5 Pro's recommendation: + +\gptbox{For Bochner $\int$, unconditional factorisation statements are +brittle because the theorem you will actually use is typically the +integrable version. \ldots~Downstream files will naturally be able to +apply [the hypothesis-bearing form], since for concrete potentials +they already prove finiteness/integrability of the partition function.} + +The cleanup Tide is exactly that downstream, and the prediction did +not hold. The existing \texttt{partitionFunction\_factor} in both 2D +files is \emph{unconditional} (no positivity hypotheses, just $\lambda$ +and $t$ as plain reals), so the wrapper has no integrability witnesses +to supply. The choice was either to strengthen the wrapper statements +with positivity (a public API change in two files), or to drop the +hypotheses on the abstraction's lemmas (a public API regression in +one file). Both Claude and GPT (in the deliberation for this Tide) +agreed that dropping the abstraction's hypotheses is the smaller +change; the discipline argument applies in principle, but in practice +the unconditional form is what callers want. + +This is worth recording as a Tide-skill calibration: ``Bochner +discipline'' arguments are theoretically right but pragmatically lose +to ``match the existing caller's signature shape'', at least until +Mathlib itself decides to tighten its unconditional integral-prod +lemmas. + +\paragraph{Worktree isolation: structural fix lands and works.} +This Tide is the first to run in a dedicated \texttt{git worktree}. +\texttt{lean/laplace-cleanup/} was created from +\texttt{tide/separable-potential}'s tip and held its own +\texttt{HEAD}/index/working-tree throughout the run. The parallel +sessions in \texttt{lean/laplace/} (which had branched onto +\texttt{tide/bounded-prior-continuous-test} and back to \texttt{main} +several times during this session) did not interfere. Three previous +retrospectives recommended this fix; this is the first concrete +confirmation. Worth lifting to a Tide-skill preflight step. + +\section{What was Mathlib, what was new} + +\paragraph{Mathlib provided.} Nothing new. The cleanup adds no new +Mathlib API consumption. + +\paragraph{The seabed (Tide 12) provided.} +The five generic factorisation lemmas of the +\texttt{AddSeparable} module --- the definition, the Boltzmann +decomposition, partition factorisation, integral factorisation, +expectation factorisation, and the mixed-covariance vanishing. + +\paragraph{What was new in this Tide.} +The two \texttt{[simp]} bridge lemmas\footnote{Names: +\texttt{semiDegeneratePotential\_eq\_addSeparable} and +\texttt{pureQuarticPotential\_eq\_addSeparable}.} identifying the +existing 2D potentials as instances of \texttt{addSeparable}. +Everything else is either deletion or a syntactic re-targeting of +existing proof bodies through the bridge. + +\section{Lessons} + +\begin{itemize} +\item \emph{Worktree isolation is the right structural fix.} Three +prior retrospectives recommended this; one Tide actually used it; it +worked. Promote to a Tide-skill preflight (``run the Tide in a +\texttt{git worktree} when concurrent sessions exist on the seabed +repo''). + +\item \emph{The Bochner-discipline argument loses on first contact +with downstream.} Tide 12 added \texttt{Integrable} hypotheses to +factorisation lemmas as documentation discipline. Tide 13 (this one) +removed them, because they blocked the cleanest refactor of two +unconditional callers. The right convention for Mathlib-shaped +factorisation lemmas with unconditional underlying API +(\texttt{integral\_prod\_mul}) is: stay unconditional unless a +specific caller's needs strengthen the case. ``Discipline'' alone is +not enough; concrete usage is. + +\item \emph{Cleanup Tides have higher leverage than they look.} +$-22$ lines is small. But the cleanup makes A2 (quartic--sextic mixed) +and A4 (mixed even-power 2D moments) one-line specialisations rather +than file-sized re-derivations. The next Tide that adds a 2D +potential pays a constant cost, not a file cost. +\end{itemize} + +\section{Follow-ups} + +\begin{itemize} +\item \emph{Quartic--sextic mixed potential (A2 from the 6 May +survey).} Now a clean specialisation: define +\texttt{quarticSexticPotential = addSeparable quarticPotential +sexticPotential}, supply a one-line bridge, and the partition + moment +factorisations come for free. + +\item \emph{Mixed even-power 2D moments (A4).} One-line corollary of +the integral-factorisation lemma at $f = x \mapsto x^m,\, g = y +\mapsto y^n$, in either of the two refactored files (or generically +over \texttt{addSeparable}). + +\item \emph{Promote 2D atom integrability to \texttt{AddSeparable.lean}.} +Both files still carry private \texttt{\_integrable\_pow\_pow} +witnesses built via \texttt{Integrable.mul\_prod} from two 1D +witnesses. A generic +\texttt{integrable\_separable\_addSeparable} in +\texttt{AddSeparable.lean} would shrink each downstream file by +another $\sim$30 lines. GPT flagged this as a strong optional add-on; +deferred to a follow-up Tide. + +\item \emph{Generic \texttt{gibbsCov} API (orthogonal future Tide).} +Still the natural infrastructure Tide for the affine-covariance +Candidate B from Tide 12's deliberation\footnote{Tentative names: +\texttt{gibbsCov\_symm}, \texttt{gibbsCov\_add\_left}, +\texttt{gibbsCov\_const\_left}, \texttt{gibbsCov\_smul\_left} and +right-hand variants.}. Independent of this cleanup but unblocked by it. + +\item \emph{Promote worktree isolation to the Tide skill's preflight.} +The skill currently flags the concurrent-agent race as a recurring +roadblock but does not prescribe a fix. Three retrospectives have +named the same fix; one Tide has now shown it works. Worth landing. +\end{itemize} + +\section*{Acknowledgements} + +GPT-5.5 Pro's deliberation contributed both the recommendation to +keep public theorem statements unchanged (rejecting Candidate B's +definitional refactor) and the architectural decision to drop the +integrability hypotheses on the AddSeparable lemmas rather than +strengthen the wrapper statements with positivity. The full consult is +preserved in the primer project's tide-log directory under the SRI +repo. + +\end{document}