diff --git a/Laplace.lean b/Laplace.lean index fe90af4..0a73d13 100644 --- a/Laplace.lean +++ b/Laplace.lean @@ -23,6 +23,7 @@ import Laplace.TwoD.SemiDegenerate import Laplace.TwoD.AddSeparable import Laplace.TwoD.PureQuartic import Laplace.OneD.AnharmonicKappa3 +import Laplace.OneD.AnharmonicKappa3Affine import Laplace.OneD.HarmonicGibbsRegularity import Laplace.OneD.HarmonicCrossSuscDeriv import Laplace.OneD.QuarticBoundedPriorTestFn diff --git a/Laplace/Gibbs.lean b/Laplace/Gibbs.lean index cb0cc2c..046b574 100644 --- a/Laplace/Gibbs.lean +++ b/Laplace/Gibbs.lean @@ -62,4 +62,125 @@ lemma gibbsExpectation_const (L : ℝ → ℝ) (t : ℝ) (c : ℝ) rw [integral_const_mul c (fun x => Real.exp (-(t * L x)))] field_simp +/-! ## Algebraic infrastructure for `gibbsExpectation` and `gibbsCov` + +The lemmas below give the bilinearity / scalar-pulling / constant-collapse +facts needed to manipulate Gibbs expectations and covariances of affine and +multilinear observables without unfolding the definitions. They are used +downstream by the affine-observable covariance lemmas (e.g. +`Laplace.OneD.Quartic.gibbsCov_first_order_rate_sharp` and the 2D analogues). + +`Integrable` hypotheses are stated directly rather than bundled into a +typeclass: at the algebraic level, only `MeasureTheory.integral_add` requires +them, and the typeclass abstraction belongs at the layer where differentiation +under the integral is the load-bearing operation. -/ + +/-- Scalar-multiplication pulls out of the Gibbs expectation. No hypotheses: +when `Z(t) = 0` both sides are zero. -/ +lemma gibbsExpectation_smul (L : ℝ → ℝ) (t : ℝ) (c : ℝ) (φ : ℝ → ℝ) : + gibbsExpectation L t (fun x => c * φ x) = c * gibbsExpectation L t φ := by + simp only [gibbsExpectation] + rw [show (fun x => c * φ x * Real.exp (-(t * L x))) + = (fun x => c * (φ x * Real.exp (-(t * L x)))) from by funext x; ring, + integral_const_mul c (fun x => φ x * Real.exp (-(t * L x))), + mul_div_assoc] + +/-- The Gibbs expectation of the zero observable is zero, unconditionally. -/ +lemma gibbsExpectation_zero (L : ℝ → ℝ) (t : ℝ) : + gibbsExpectation L t (fun _ => 0) = 0 := by + simp [gibbsExpectation] + +/-- Additivity of the Gibbs expectation: requires integrability of each +weighted observable. -/ +lemma gibbsExpectation_add (L : ℝ → ℝ) (t : ℝ) (φ₁ φ₂ : ℝ → ℝ) + (h₁ : Integrable (fun x => φ₁ x * Real.exp (-(t * L x)))) + (h₂ : Integrable (fun x => φ₂ x * Real.exp (-(t * L x)))) : + gibbsExpectation L t (fun x => φ₁ x + φ₂ x) + = gibbsExpectation L t φ₁ + gibbsExpectation L t φ₂ := by + simp only [gibbsExpectation] + rw [show (fun x => (φ₁ x + φ₂ x) * Real.exp (-(t * L x))) + = (fun x => φ₁ x * Real.exp (-(t * L x)) + + φ₂ x * Real.exp (-(t * L x))) from by funext x; ring, + integral_add h₁ h₂, add_div] + +/-- Symmetry: `Cov_t[φ, ψ] = Cov_t[ψ, φ]`. -/ +lemma gibbsCov_symm (L : ℝ → ℝ) (t : ℝ) (φ ψ : ℝ → ℝ) : + gibbsCov L t φ ψ = gibbsCov L t ψ φ := by + simp only [gibbsCov] + rw [show (fun x => φ x * ψ x) = (fun x => ψ x * φ x) from by funext x; ring, + mul_comm (gibbsExpectation L t φ)] + +/-- Scalar pulls out of the left slot. No hypotheses. -/ +lemma gibbsCov_smul_left (L : ℝ → ℝ) (t : ℝ) (c : ℝ) (φ ψ : ℝ → ℝ) : + gibbsCov L t (fun x => c * φ x) ψ = c * gibbsCov L t φ ψ := by + simp only [gibbsCov] + rw [show (fun x => c * φ x * ψ x) = (fun x => c * (φ x * ψ x)) from + by funext x; ring, + gibbsExpectation_smul, gibbsExpectation_smul] + ring + +/-- Scalar pulls out of the right slot. -/ +lemma gibbsCov_smul_right (L : ℝ → ℝ) (t : ℝ) (c : ℝ) (φ ψ : ℝ → ℝ) : + gibbsCov L t φ (fun x => c * ψ x) = c * gibbsCov L t φ ψ := by + rw [gibbsCov_symm, gibbsCov_smul_left, gibbsCov_symm] + +/-- Constants in the left slot give zero covariance. Unconditional: when +`Z(t) = 0` every Gibbs expectation collapses to `0`, so both sides agree. -/ +lemma gibbsCov_const_left (L : ℝ → ℝ) (t : ℝ) (c : ℝ) (ψ : ℝ → ℝ) : + gibbsCov L t (fun _ => c) ψ = 0 := by + by_cases hZ : partitionFunction L t = 0 + · simp [gibbsCov, gibbsExpectation, partitionFunction] at hZ ⊢ + simp [hZ] + · simp only [gibbsCov] + rw [show (fun x => (fun _ => c) x * ψ x) = (fun x => c * ψ x) from rfl, + gibbsExpectation_smul, gibbsExpectation_const L t c hZ] + ring + +/-- Constants in the right slot give zero covariance. -/ +lemma gibbsCov_const_right (L : ℝ → ℝ) (t : ℝ) (φ : ℝ → ℝ) (c : ℝ) : + gibbsCov L t φ (fun _ => c) = 0 := by + rw [gibbsCov_symm, gibbsCov_const_left] + +/-- Additivity in the left slot. Requires integrability of each weighted +observable, both alone and against `ψ`. -/ +lemma gibbsCov_add_left (L : ℝ → ℝ) (t : ℝ) (φ₁ φ₂ ψ : ℝ → ℝ) + (h₁ : Integrable (fun x => φ₁ x * Real.exp (-(t * L x)))) + (h₂ : Integrable (fun x => φ₂ x * Real.exp (-(t * L x)))) + (h₁ψ : Integrable (fun x => φ₁ x * ψ x * Real.exp (-(t * L x)))) + (h₂ψ : Integrable (fun x => φ₂ x * ψ x * Real.exp (-(t * L x)))) : + gibbsCov L t (fun x => φ₁ x + φ₂ x) ψ + = gibbsCov L t φ₁ ψ + gibbsCov L t φ₂ ψ := by + simp only [gibbsCov] + rw [show (fun x => (φ₁ x + φ₂ x) * ψ x) + = (fun x => φ₁ x * ψ x + φ₂ x * ψ x) from by funext x; ring, + gibbsExpectation_add L t (fun x => φ₁ x * ψ x) (fun x => φ₂ x * ψ x) h₁ψ h₂ψ, + gibbsExpectation_add L t φ₁ φ₂ h₁ h₂] + ring + +/-- Additivity in the right slot. -/ +lemma gibbsCov_add_right (L : ℝ → ℝ) (t : ℝ) (φ ψ₁ ψ₂ : ℝ → ℝ) + (h₁ : Integrable (fun x => ψ₁ x * Real.exp (-(t * L x)))) + (h₂ : Integrable (fun x => ψ₂ x * Real.exp (-(t * L x)))) + (h₁φ : Integrable (fun x => φ x * ψ₁ x * Real.exp (-(t * L x)))) + (h₂φ : Integrable (fun x => φ x * ψ₂ x * Real.exp (-(t * L x)))) : + gibbsCov L t φ (fun x => ψ₁ x + ψ₂ x) + = gibbsCov L t φ ψ₁ + gibbsCov L t φ ψ₂ := by + have h₁φ' : Integrable (fun x => ψ₁ x * φ x * Real.exp (-(t * L x))) := by + simpa [mul_comm] using h₁φ + have h₂φ' : Integrable (fun x => ψ₂ x * φ x * Real.exp (-(t * L x))) := by + simpa [mul_comm] using h₂φ + rw [gibbsCov_symm L t φ (fun x => ψ₁ x + ψ₂ x), + gibbsCov_add_left L t ψ₁ ψ₂ φ h₁ h₂ h₁φ' h₂φ', + gibbsCov_symm L t ψ₁ φ, gibbsCov_symm L t ψ₂ φ] + +/-- Zero observable on the left gives zero covariance. -/ +lemma gibbsCov_zero_left (L : ℝ → ℝ) (t : ℝ) (ψ : ℝ → ℝ) : + gibbsCov L t (fun _ => 0) ψ = 0 := + gibbsCov_const_left L t 0 ψ + +/-- Zero observable on the right gives zero covariance. -/ +lemma gibbsCov_zero_right (L : ℝ → ℝ) (t : ℝ) (φ : ℝ → ℝ) : + gibbsCov L t φ (fun _ => 0) = 0 := + gibbsCov_const_right L t φ 0 + end Laplace diff --git a/Laplace/Multi/Basic.lean b/Laplace/Multi/Basic.lean index 2f40c94..3f9e251 100644 --- a/Laplace/Multi/Basic.lean +++ b/Laplace/Multi/Basic.lean @@ -52,4 +52,128 @@ lemma gibbsExpectation_def (L : (ι → ℝ) → ℝ) (t : ℝ) (φ : (ι → gibbsExpectation L t φ = (∫ w : ι → ℝ, φ w * Real.exp (-(t * L w))) / partitionFunction L t := rfl +/-! ## Algebraic infrastructure for `gibbsExpectation` and `gibbsCov` + +Multivariate analogues of the lemmas in `Laplace.Gibbs`. The proofs are +mechanically identical to the 1D versions (the underlying integration lemmas +`MeasureTheory.integral_const_mul` and `MeasureTheory.integral_add` are +parametric in the underlying measurable space). -/ + +/-- Constant observables: `⟨c⟩_t = c` whenever `Z(t) ≠ 0`. -/ +lemma gibbsExpectation_const (L : (ι → ℝ) → ℝ) (t : ℝ) (c : ℝ) + (hZ : partitionFunction L t ≠ 0) : + gibbsExpectation L t (fun _ => c) = c := by + have hZ' : (∫ w : ι → ℝ, Real.exp (-(t * L w))) ≠ 0 := hZ + simp only [gibbsExpectation, partitionFunction] + rw [integral_const_mul c (fun w => Real.exp (-(t * L w)))] + field_simp + +/-- Scalar-multiplication pulls out of the Gibbs expectation. No hypotheses: +when `Z(t) = 0` both sides are zero. -/ +lemma gibbsExpectation_smul (L : (ι → ℝ) → ℝ) (t : ℝ) (c : ℝ) (φ : (ι → ℝ) → ℝ) : + gibbsExpectation L t (fun w => c * φ w) = c * gibbsExpectation L t φ := by + simp only [gibbsExpectation] + rw [show (fun w => c * φ w * Real.exp (-(t * L w))) + = (fun w => c * (φ w * Real.exp (-(t * L w)))) from by funext w; ring, + integral_const_mul c (fun w => φ w * Real.exp (-(t * L w))), + mul_div_assoc] + +/-- The Gibbs expectation of the zero observable is zero, unconditionally. -/ +lemma gibbsExpectation_zero (L : (ι → ℝ) → ℝ) (t : ℝ) : + gibbsExpectation L t (fun _ => 0) = 0 := by + simp [gibbsExpectation] + +/-- Additivity of the Gibbs expectation: requires integrability of each +weighted observable. -/ +lemma gibbsExpectation_add (L : (ι → ℝ) → ℝ) (t : ℝ) (φ₁ φ₂ : (ι → ℝ) → ℝ) + (h₁ : Integrable (fun w => φ₁ w * Real.exp (-(t * L w)))) + (h₂ : Integrable (fun w => φ₂ w * Real.exp (-(t * L w)))) : + gibbsExpectation L t (fun w => φ₁ w + φ₂ w) + = gibbsExpectation L t φ₁ + gibbsExpectation L t φ₂ := by + simp only [gibbsExpectation] + rw [show (fun w => (φ₁ w + φ₂ w) * Real.exp (-(t * L w))) + = (fun w => φ₁ w * Real.exp (-(t * L w)) + + φ₂ w * Real.exp (-(t * L w))) from by funext w; ring, + integral_add h₁ h₂, add_div] + +/-- Symmetry: `Cov_t[φ, ψ] = Cov_t[ψ, φ]`. -/ +lemma gibbsCov_symm (L : (ι → ℝ) → ℝ) (t : ℝ) (φ ψ : (ι → ℝ) → ℝ) : + gibbsCov L t φ ψ = gibbsCov L t ψ φ := by + simp only [gibbsCov] + rw [show (fun w => φ w * ψ w) = (fun w => ψ w * φ w) from by funext w; ring, + mul_comm (gibbsExpectation L t φ)] + +/-- Scalar pulls out of the left slot. No hypotheses. -/ +lemma gibbsCov_smul_left (L : (ι → ℝ) → ℝ) (t : ℝ) (c : ℝ) (φ ψ : (ι → ℝ) → ℝ) : + gibbsCov L t (fun w => c * φ w) ψ = c * gibbsCov L t φ ψ := by + simp only [gibbsCov] + rw [show (fun w => c * φ w * ψ w) = (fun w => c * (φ w * ψ w)) from + by funext w; ring, + gibbsExpectation_smul, gibbsExpectation_smul] + ring + +/-- Scalar pulls out of the right slot. -/ +lemma gibbsCov_smul_right (L : (ι → ℝ) → ℝ) (t : ℝ) (c : ℝ) (φ ψ : (ι → ℝ) → ℝ) : + gibbsCov L t φ (fun w => c * ψ w) = c * gibbsCov L t φ ψ := by + rw [gibbsCov_symm, gibbsCov_smul_left, gibbsCov_symm] + +/-- Constants in the left slot give zero covariance. Unconditional: when +`Z(t) = 0` every Gibbs expectation collapses to `0`, so both sides agree. -/ +lemma gibbsCov_const_left (L : (ι → ℝ) → ℝ) (t : ℝ) (c : ℝ) (ψ : (ι → ℝ) → ℝ) : + gibbsCov L t (fun _ => c) ψ = 0 := by + by_cases hZ : partitionFunction L t = 0 + · simp [gibbsCov, gibbsExpectation, partitionFunction] at hZ ⊢ + simp [hZ] + · simp only [gibbsCov] + rw [show (fun w => (fun _ => c) w * ψ w) = (fun w => c * ψ w) from rfl, + gibbsExpectation_smul, gibbsExpectation_const L t c hZ] + ring + +/-- Constants in the right slot give zero covariance. -/ +lemma gibbsCov_const_right (L : (ι → ℝ) → ℝ) (t : ℝ) (φ : (ι → ℝ) → ℝ) (c : ℝ) : + gibbsCov L t φ (fun _ => c) = 0 := by + rw [gibbsCov_symm, gibbsCov_const_left] + +/-- Additivity in the left slot. Requires integrability of each weighted +observable, both alone and against `ψ`. -/ +lemma gibbsCov_add_left (L : (ι → ℝ) → ℝ) (t : ℝ) (φ₁ φ₂ ψ : (ι → ℝ) → ℝ) + (h₁ : Integrable (fun w => φ₁ w * Real.exp (-(t * L w)))) + (h₂ : Integrable (fun w => φ₂ w * Real.exp (-(t * L w)))) + (h₁ψ : Integrable (fun w => φ₁ w * ψ w * Real.exp (-(t * L w)))) + (h₂ψ : Integrable (fun w => φ₂ w * ψ w * Real.exp (-(t * L w)))) : + gibbsCov L t (fun w => φ₁ w + φ₂ w) ψ + = gibbsCov L t φ₁ ψ + gibbsCov L t φ₂ ψ := by + simp only [gibbsCov] + rw [show (fun w => (φ₁ w + φ₂ w) * ψ w) + = (fun w => φ₁ w * ψ w + φ₂ w * ψ w) from by funext w; ring, + gibbsExpectation_add L t (fun w => φ₁ w * ψ w) (fun w => φ₂ w * ψ w) h₁ψ h₂ψ, + gibbsExpectation_add L t φ₁ φ₂ h₁ h₂] + ring + +/-- Additivity in the right slot. -/ +lemma gibbsCov_add_right (L : (ι → ℝ) → ℝ) (t : ℝ) (φ ψ₁ ψ₂ : (ι → ℝ) → ℝ) + (h₁ : Integrable (fun w => ψ₁ w * Real.exp (-(t * L w)))) + (h₂ : Integrable (fun w => ψ₂ w * Real.exp (-(t * L w)))) + (h₁φ : Integrable (fun w => φ w * ψ₁ w * Real.exp (-(t * L w)))) + (h₂φ : Integrable (fun w => φ w * ψ₂ w * Real.exp (-(t * L w)))) : + gibbsCov L t φ (fun w => ψ₁ w + ψ₂ w) + = gibbsCov L t φ ψ₁ + gibbsCov L t φ ψ₂ := by + have h₁φ' : Integrable (fun w => ψ₁ w * φ w * Real.exp (-(t * L w))) := by + simpa [mul_comm] using h₁φ + have h₂φ' : Integrable (fun w => ψ₂ w * φ w * Real.exp (-(t * L w))) := by + simpa [mul_comm] using h₂φ + rw [gibbsCov_symm L t φ (fun w => ψ₁ w + ψ₂ w), + gibbsCov_add_left L t ψ₁ ψ₂ φ h₁ h₂ h₁φ' h₂φ', + gibbsCov_symm L t ψ₁ φ, gibbsCov_symm L t ψ₂ φ] + +/-- Zero observable on the left gives zero covariance. -/ +lemma gibbsCov_zero_left (L : (ι → ℝ) → ℝ) (t : ℝ) (ψ : (ι → ℝ) → ℝ) : + gibbsCov L t (fun _ => 0) ψ = 0 := + gibbsCov_const_left L t 0 ψ + +/-- Zero observable on the right gives zero covariance. -/ +lemma gibbsCov_zero_right (L : (ι → ℝ) → ℝ) (t : ℝ) (φ : (ι → ℝ) → ℝ) : + gibbsCov L t φ (fun _ => 0) = 0 := + gibbsCov_const_right L t φ 0 + end Laplace.Multi diff --git a/Laplace/OneD/AnharmonicKappa3.lean b/Laplace/OneD/AnharmonicKappa3.lean index 47dafc1..fcac732 100644 --- a/Laplace/OneD/AnharmonicKappa3.lean +++ b/Laplace/OneD/AnharmonicKappa3.lean @@ -382,6 +382,107 @@ theorem thirdMoment_anharmonic_asymptotic rw [h_x2_x] ring +/-! ## Affine multilinearity (G2) + +Tide 9's `kappa3_anharmonic_id_id_id_asymptotic` lifts to affine +observables `(b·x, a·x, c·x)` by trilinearity of `κ₃`: the scalars +`a, b, c` pull through cleanly, giving an extra factor `a·b·c` on the +asymptotic value. + +Two theorems: + +* `kappa3_affine_id_id_id_eq` — the static factorisation. No + hypotheses on `L` beyond what `Threepoint.kappa3`'s definition + consumes (i.e. none); built from `gibbsExpectation_smul` and + `kappa3_id_id_id_unfold`. Works for any potential, not just the + anharmonic one. + +* `kappa3_anharmonic_affine_asymptotic` — the asymptotic corollary + for the anharmonic potential. Direct `Tendsto.const_mul` on top of + Tide 9 plus the static factorisation. -/ + +/-- **Affine multilinearity of κ₃ at `id`-multiples** (potential-agnostic). + +For any potential `L : ℝ → ℝ` and scalars `a, b, c : ℝ`, the third +cumulant of `(b·x, a·x, c·x)` factors as the trilinear product of the +scalars times the third cumulant of `(x, x, x)`. + +The proof unfolds both sides to the seven-Gibbs-expectation form via +`kappa3_id_id_id_unfold`'s sibling expansion, peels each scalar via +`gibbsExpectation_smul`, and closes by `ring`. -/ +theorem kappa3_affine_id_id_id_eq (L : ℝ → ℝ) (t : ℝ) (a b c : ℝ) : + Threepoint.kappa3 (volume : Measure ℝ) L + (fun x : ℝ => b * x) t (fun x : ℝ => a * x) (fun x : ℝ => c * x) + = (a * b * c) * + Threepoint.kappa3 (volume : Measure ℝ) L + (fun x : ℝ => x) t (fun x : ℝ => x) (fun x : ℝ => x) := by + -- Unfold `kappa3` on both sides; route every `Threepoint.gibbsExp ... 0` + -- through `threepoint_gibbsExp_volume_zero_eq` to `Laplace.gibbsExpectation`. + unfold Threepoint.kappa3 + simp only [threepoint_gibbsExp_volume_zero_eq] + -- Collapse the seven LHS integrand lambdas to the canonical scaled forms + -- `(a*b*c) * x^3`, `(a*b) * x^2`, `(a*c) * x^2`, `(b*c) * x^2`, + -- `a*x`, `b*x`, `c*x`, then peel scalars via `gibbsExpectation_smul`. + have h_abc : (fun w : ℝ => (fun x : ℝ => a * x) w * (fun x : ℝ => b * x) w + * (fun x : ℝ => c * x) w) = (fun w : ℝ => (a * b * c) * w ^ 3) := by + funext w; ring + have h_ab : (fun w : ℝ => (fun x : ℝ => a * x) w * (fun x : ℝ => b * x) w) + = (fun w : ℝ => (a * b) * w ^ 2) := by + funext w; ring + have h_ac : (fun w : ℝ => (fun x : ℝ => a * x) w * (fun x : ℝ => c * x) w) + = (fun w : ℝ => (a * c) * w ^ 2) := by + funext w; ring + have h_bc : (fun w : ℝ => (fun x : ℝ => b * x) w * (fun x : ℝ => c * x) w) + = (fun w : ℝ => (b * c) * w ^ 2) := by + funext w; ring + -- Same simplifications for the RHS at `(id, id, id)`. + have h_x3 : (fun w : ℝ => (fun x : ℝ => x) w * (fun x : ℝ => x) w + * (fun x : ℝ => x) w) = (fun w : ℝ => w ^ 3) := by + funext w; ring + have h_x2 : (fun w : ℝ => (fun x : ℝ => x) w * (fun x : ℝ => x) w) + = (fun w : ℝ => w ^ 2) := by + funext w; ring + rw [h_abc, h_ab, h_ac, h_bc, h_x3, h_x2] + -- Peel scalars from each scaled `gibbsExpectation` via `gibbsExpectation_smul`. + rw [Laplace.gibbsExpectation_smul L t (a * b * c) (fun w : ℝ => w ^ 3), + Laplace.gibbsExpectation_smul L t (a * b) (fun w : ℝ => w ^ 2), + Laplace.gibbsExpectation_smul L t (a * c) (fun w : ℝ => w ^ 2), + Laplace.gibbsExpectation_smul L t (b * c) (fun w : ℝ => w ^ 2), + Laplace.gibbsExpectation_smul L t a (fun w : ℝ => w), + Laplace.gibbsExpectation_smul L t b (fun w : ℝ => w), + Laplace.gibbsExpectation_smul L t c (fun w : ℝ => w)] + ring + +/-- **Affine third-cumulant asymptotic for the anharmonic Gibbs.** + +For `L = (λ/2)x² + (α/6)x³ + (γ/24)x⁴` with `0 < λ`, `0 < γ`, +`α² < 3λγ`, and any scalars `a, b, c : ℝ`, +`t² · κ₃(volume, L, b·x, t, a·x, c·x) → -(a·b·c)·α/λ³` as `t → ∞`. + +Strict-improvement of Tide 9: that tide proved the case `(a, b, c) = (1, 1, 1)`; +this multiplies by trilinearity of `κ₃` to handle arbitrary `id`-multiples. -/ +theorem kappa3_anharmonic_affine_asymptotic + {lam alpha gamma : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) (hdisc : alpha ^ 2 < 3 * lam * gamma) + (a b c : ℝ) : + Filter.Tendsto + (fun t : ℝ => t ^ 2 * Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => b * x) t (fun x : ℝ => a * x) (fun x : ℝ => c * x)) + Filter.atTop + (nhds (-(a * b * c) * alpha / lam ^ 3)) := by + have hBase := kappa3_anharmonic_id_id_id_asymptotic hlam hgamma hdisc + -- Replace the limit constant by the trilinearly-scaled form: abc · (-α/λ³). + have h_lim_eq : -(a * b * c) * alpha / lam ^ 3 = (a * b * c) * (-alpha / lam ^ 3) := by + ring + rw [h_lim_eq] + -- t² · κ₃(b·x, a·x, c·x) = abc · (t² · κ₃(x, x, x)), so the limit is abc · (-α/λ³). + have h_const := hBase.const_mul (a * b * c) + apply h_const.congr' + filter_upwards with t + rw [kappa3_affine_id_id_id_eq (anharmonicPotential lam alpha gamma) t a b c] + ring + end OneD end Laplace diff --git a/Laplace/OneD/AnharmonicKappa3Affine.lean b/Laplace/OneD/AnharmonicKappa3Affine.lean new file mode 100644 index 0000000..e6aba24 --- /dev/null +++ b/Laplace/OneD/AnharmonicKappa3Affine.lean @@ -0,0 +1,384 @@ +import Laplace.OneD.AnharmonicKappa3 + +/-! +# Shifted-affine strengthening of the anharmonic-κ₃ asymptotic + +For the 1D anharmonic potential `L(x) = (λ/2)x² + (α/6)x³ + (γ/24)x⁴` +with `λ, γ > 0` and the discriminant condition `α² < 3λγ`, and three +**shifted** affine observables `αᵢ(x) = aᵢ·x + bᵢ`, + + `t² · κ₃(α₁, α₂, α₃) → a₁·a₂·a₃ · (-α/λ³)` as `t → ∞`. + +The constants `bᵢ` drop because the joint third cumulant vanishes on +constant slots. This is a strict-improvement of the linear-affine +`kappa3_anharmonic_affine_asymptotic` (this same tide branch's earlier +landing): there `(b·x, a·x, c·x)` was proven, with the constants in +each slot deferred as a follow-up. The retrospective for the linear +case identified this shifted-affine extension as a follow-up, citing +~50 extra lines for the `gibbsExpectation_const` plumbing — and indeed +the bulk of this file is the cubic-polynomial expansion infrastructure +needed when the integrands carry constant terms. + +## Tide-step provenance + +Strict-improvement extension of Tide G2 +(kappa3-affine-anharmonic), on the same branch +`tide/kappa3-affine-anharmonic`. The base linear case was committed +in `1b3e9bd`; this file adds the shifted-affine extension on top. + +See +`sri/projects/primer/tide-log/2026-05-07-tide-kappa3-affine-anharmonic.md` +for the deliberation log. The `gibbsExpectation_const` requirement +(absent from the linear case) drives the `partitionFunction ≠ 0` and +polynomial-times-`exp(-tL)` integrability infrastructure below. +-/ + +open MeasureTheory Filter Topology + +namespace Laplace + +namespace OneD + +/-! ## Integrability witnesses for `xⁿ · exp(-t · L_anh)` -/ + +/-- Polynomial-times-`exp(-t·L)` is integrable for the anharmonic +potential, by domination by the Gaussian `|x|ⁿ · exp(-tc·x²)` from +coercivity. -/ +private lemma integrable_pow_mul_exp_neg_anharmonic + (n : ℕ) {lam alpha gamma t : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) (ht : 0 < t) : + Integrable (fun x : ℝ => x ^ n * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + -- Coercivity gives `c > 0` with `c · x² ≤ L_anh(x)` everywhere. + obtain ⟨c, hc_pos, hbound⟩ := + anharmonic_coercive lam alpha gamma hlam hgamma hdisc + have htc_pos : 0 < t * c := mul_pos ht hc_pos + -- Dominator: `|x|ⁿ · exp(-tc·x²)`, integrable. + have h_dom : Integrable (fun x : ℝ => |x| ^ n * + Real.exp (-(t * c * x ^ 2))) := + integrable_abs_pow_mul_exp_neg_mul_sq htc_pos n + -- Continuity → AE strong measurability. + have h_meas : AEStronglyMeasurable + (fun x : ℝ => x ^ n * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) volume := by + apply Continuous.aestronglyMeasurable + apply Continuous.mul + · exact (continuous_id.pow n) + · apply Real.continuous_exp.comp + apply Continuous.neg + apply Continuous.mul continuous_const + -- anharmonicPotential is a polynomial in x. + unfold anharmonicPotential + fun_prop + -- Pointwise: `|xⁿ · exp(-t·L_anh)| ≤ |x|ⁿ · exp(-tc·x²)`. + refine h_dom.mono h_meas ?_ + refine Filter.Eventually.of_forall (fun x => ?_) + rw [Real.norm_eq_abs, abs_mul, abs_pow, abs_of_pos (Real.exp_pos _)] + rw [Real.norm_eq_abs, abs_mul, abs_pow, abs_abs, abs_of_pos (Real.exp_pos _)] + apply mul_le_mul_of_nonneg_left _ (pow_nonneg (abs_nonneg x) n) + apply Real.exp_le_exp.mpr + -- `-(t·L_anh) ≤ -(t·c·x²)` ↔ `t·c·x² ≤ t·L_anh` (use `hbound`, `ht > 0`). + have h := hbound x + have ht_le : t * (c * x ^ 2) ≤ t * anharmonicPotential lam alpha gamma x := + mul_le_mul_of_nonneg_left h ht.le + linarith + +/-- The partition function for the anharmonic potential is positive +(hence nonzero) for `t > 0`. Since `exp(-(t · L_anh))` is strictly +positive everywhere and integrable, `integral_exp_pos` closes. -/ +private lemma partitionFunction_anharmonic_pos + {lam alpha gamma t : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) (ht : 0 < t) : + 0 < Laplace.partitionFunction (anharmonicPotential lam alpha gamma) t := by + unfold Laplace.partitionFunction + have h_int : Integrable + (fun x : ℝ => Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + have h := integrable_pow_mul_exp_neg_anharmonic 0 hlam hgamma hdisc ht + simpa using h + exact integral_exp_pos h_int + +private lemma partitionFunction_anharmonic_ne_zero + {lam alpha gamma t : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) (ht : 0 < t) : + Laplace.partitionFunction (anharmonicPotential lam alpha gamma) t ≠ 0 := + (partitionFunction_anharmonic_pos hlam hgamma hdisc ht).ne' + +/-! ## Cubic-polynomial expectation expansion + +`⟨c₃·x³ + c₂·x² + c₁·x + c₀⟩ = c₃·⟨x³⟩ + c₂·⟨x²⟩ + c₁·⟨x⟩ + c₀` for the +anharmonic Gibbs measure. The four `Integrable` witnesses come from the +coercivity-domination lemma above. -/ + +private lemma gibbsExp_anharmonic_cubic_eq + {lam alpha gamma t : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) (ht : 0 < t) + (c₀ c₁ c₂ c₃ : ℝ) : + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x + c₀) + = c₃ * Laplace.gibbsExpectation + (anharmonicPotential lam alpha gamma) t (fun x : ℝ => x ^ 3) + + c₂ * Laplace.gibbsExpectation + (anharmonicPotential lam alpha gamma) t (fun x : ℝ => x ^ 2) + + c₁ * Laplace.gibbsExpectation + (anharmonicPotential lam alpha gamma) t (fun x : ℝ => x) + + c₀ := by + have hZ := partitionFunction_anharmonic_ne_zero hlam hgamma hdisc ht + -- Integrability of `cₖ · xᵏ · exp(-tL)` for k = 0, 1, 2, 3. + have h0 := (integrable_pow_mul_exp_neg_anharmonic 0 hlam hgamma hdisc ht).const_mul c₀ + have h1 := (integrable_pow_mul_exp_neg_anharmonic 1 hlam hgamma hdisc ht).const_mul c₁ + have h2 := (integrable_pow_mul_exp_neg_anharmonic 2 hlam hgamma hdisc ht).const_mul c₂ + have h3 := (integrable_pow_mul_exp_neg_anharmonic 3 hlam hgamma hdisc ht).const_mul c₃ + -- Massage each into the `(fun x => cₖ * xᵏ) * exp` form for `_add` consumption. + have h0' : Integrable (fun x : ℝ => c₀ * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + simpa using h0 + have h1' : Integrable (fun x : ℝ => c₁ * x * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + have : (fun x : ℝ => c₁ * (x ^ 1 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)))) + = (fun x : ℝ => c₁ * x * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + funext x; ring + rw [← this]; exact h1 + have h2' : Integrable (fun x : ℝ => c₂ * x ^ 2 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + have : (fun x : ℝ => c₂ * (x ^ 2 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)))) + = (fun x : ℝ => c₂ * x ^ 2 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + funext x; ring + rw [← this]; exact h2 + have h3' : Integrable (fun x : ℝ => c₃ * x ^ 3 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + have : (fun x : ℝ => c₃ * (x ^ 3 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)))) + = (fun x : ℝ => c₃ * x ^ 3 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + funext x; ring + rw [← this]; exact h3 + -- Build sums step by step (left-associative `(((a + b) + c) + d)` matches the goal). + have h12 : Integrable (fun x : ℝ => c₁ * x * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)) + + c₀ * Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := h1'.add h0' + -- First-stage split: pull off `c₀` (innermost). + have step0 : + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x + c₀) + = Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x) + + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun _ : ℝ => c₀) := by + have h_lhs_split : + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x + c₀) + = (fun x : ℝ => (c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x) + c₀) := by + funext x; ring + rw [h_lhs_split] + refine Laplace.gibbsExpectation_add (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x) (fun _ : ℝ => c₀) ?_ ?_ + · -- Integrability of `(c₃ x³ + c₂ x² + c₁ x) · exp`. + have : (fun x : ℝ => (c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x) * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) + = (fun x : ℝ => c₃ * x ^ 3 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)) + + c₂ * x ^ 2 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)) + + c₁ * x * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + funext x; ring + rw [this] + exact ((h3'.add h2').add h1') + · exact h0' + -- Second stage: pull off `c₁ x` from `c₃ x³ + c₂ x² + c₁ x`. + have step1 : + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2 + c₁ * x) + = Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2) + + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₁ * x) := by + refine Laplace.gibbsExpectation_add (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2) (fun x : ℝ => c₁ * x) ?_ h1' + have : (fun x : ℝ => (c₃ * x ^ 3 + c₂ * x ^ 2) * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) + = (fun x : ℝ => c₃ * x ^ 3 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x)) + + c₂ * x ^ 2 * + Real.exp (-(t * anharmonicPotential lam alpha gamma x))) := by + funext x; ring + rw [this] + exact h3'.add h2' + -- Third stage: pull off `c₂ x²` from `c₃ x³ + c₂ x²`. + have step2 : + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3 + c₂ * x ^ 2) + = Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3) + + Laplace.gibbsExpectation (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₂ * x ^ 2) := by + exact Laplace.gibbsExpectation_add (anharmonicPotential lam alpha gamma) t + (fun x : ℝ => c₃ * x ^ 3) (fun x : ℝ => c₂ * x ^ 2) h3' h2' + -- Now apply `_smul` to pull constants out, plus `_const` for c₀. + rw [step0, step1, step2] + rw [Laplace.gibbsExpectation_smul (anharmonicPotential lam alpha gamma) t c₃ + (fun x : ℝ => x ^ 3), + Laplace.gibbsExpectation_smul (anharmonicPotential lam alpha gamma) t c₂ + (fun x : ℝ => x ^ 2), + Laplace.gibbsExpectation_smul (anharmonicPotential lam alpha gamma) t c₁ + (fun x : ℝ => x), + Laplace.gibbsExpectation_const (anharmonicPotential lam alpha gamma) t c₀ hZ] + +/-! ## `Threepoint.gibbsExp` ↔ `Laplace.gibbsExpectation` bridge at `h = 0` + +Re-derived locally because Tide 9's +`AnharmonicKappa3.threepoint_gibbsExp_volume_zero_eq` is `private`. -/ + +private lemma threepoint_gibbsExp_volume_zero_eq' + (L A φ : ℝ → ℝ) (t : ℝ) : + Threepoint.gibbsExp (volume : Measure ℝ) L A t 0 φ + = Laplace.gibbsExpectation L t φ := by + unfold Threepoint.gibbsExp Laplace.gibbsExpectation Laplace.partitionFunction + simp only [zero_mul, add_zero] + +/-- Unfolding of `Threepoint.kappa3` over `volume` in five +`Laplace.gibbsExpectation` terms (independent of the perturbation +direction `A`, since at `h = 0` it doesn't enter the integrand). -/ +private lemma kappa3_volume_unfold + (L A φ B : ℝ → ℝ) (t : ℝ) : + Threepoint.kappa3 (volume : Measure ℝ) L A t φ B + = Laplace.gibbsExpectation L t (fun x : ℝ => φ x * A x * B x) + - Laplace.gibbsExpectation L t (fun x : ℝ => φ x * A x) + * Laplace.gibbsExpectation L t B + - Laplace.gibbsExpectation L t (fun x : ℝ => φ x * B x) + * Laplace.gibbsExpectation L t A + - Laplace.gibbsExpectation L t (fun x : ℝ => A x * B x) + * Laplace.gibbsExpectation L t φ + + 2 * Laplace.gibbsExpectation L t φ + * Laplace.gibbsExpectation L t A + * Laplace.gibbsExpectation L t B := by + unfold Threepoint.kappa3 + rw [threepoint_gibbsExp_volume_zero_eq', threepoint_gibbsExp_volume_zero_eq', + threepoint_gibbsExp_volume_zero_eq', threepoint_gibbsExp_volume_zero_eq', + threepoint_gibbsExp_volume_zero_eq', threepoint_gibbsExp_volume_zero_eq', + threepoint_gibbsExp_volume_zero_eq'] + +/-! ## The multilinear unfolding lemma -/ + +/-- The multilinear identity for the anharmonic third joint cumulant. +For three affine observables `(a₁ x + b₁, a₂ x + b₂, a₃ x + b₃)`, the +joint third cumulant rescales by `a₁ a₂ a₃` and the constants `bᵢ` +drop. This is the structural content driving the asymptotic theorem +below. -/ +private theorem kappa3_anharmonic_shifted_affine_eq_smul + {lam alpha gamma t : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) (ht : 0 < t) + (a₁ a₂ a₃ b₁ b₂ b₃ : ℝ) : + Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => a₂ * x + b₂) t + (fun x : ℝ => a₁ * x + b₁) (fun x : ℝ => a₃ * x + b₃) + = a₁ * a₂ * a₃ * Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => x) t (fun x : ℝ => x) (fun x : ℝ => x) := by + -- Unfold both kappa3 calls into five `Laplace.gibbsExpectation` terms. + rw [kappa3_volume_unfold, kappa3_volume_unfold] + -- Massage each integrand into cubic-polynomial form. + have h_α1α2α3 : (fun x : ℝ => (a₁ * x + b₁) * (a₂ * x + b₂) * (a₃ * x + b₃)) + = (fun x : ℝ => a₁ * a₂ * a₃ * x ^ 3 + + (a₁ * a₂ * b₃ + a₁ * b₂ * a₃ + b₁ * a₂ * a₃) * x ^ 2 + + (a₁ * b₂ * b₃ + b₁ * a₂ * b₃ + b₁ * b₂ * a₃) * x + + b₁ * b₂ * b₃) := by funext x; ring + have h_α1α2 : (fun x : ℝ => (a₁ * x + b₁) * (a₂ * x + b₂)) + = (fun x : ℝ => 0 * x ^ 3 + a₁ * a₂ * x ^ 2 + + (a₁ * b₂ + a₂ * b₁) * x + b₁ * b₂) := by funext x; ring + have h_α1α3 : (fun x : ℝ => (a₁ * x + b₁) * (a₃ * x + b₃)) + = (fun x : ℝ => 0 * x ^ 3 + a₁ * a₃ * x ^ 2 + + (a₁ * b₃ + a₃ * b₁) * x + b₁ * b₃) := by funext x; ring + have h_α2α3 : (fun x : ℝ => (a₂ * x + b₂) * (a₃ * x + b₃)) + = (fun x : ℝ => 0 * x ^ 3 + a₂ * a₃ * x ^ 2 + + (a₂ * b₃ + a₃ * b₂) * x + b₂ * b₃) := by funext x; ring + have h_α1 : (fun x : ℝ => a₁ * x + b₁) + = (fun x : ℝ => 0 * x ^ 3 + 0 * x ^ 2 + a₁ * x + b₁) := by funext x; ring + have h_α2 : (fun x : ℝ => a₂ * x + b₂) + = (fun x : ℝ => 0 * x ^ 3 + 0 * x ^ 2 + a₂ * x + b₂) := by funext x; ring + have h_α3 : (fun x : ℝ => a₃ * x + b₃) + = (fun x : ℝ => 0 * x ^ 3 + 0 * x ^ 2 + a₃ * x + b₃) := by funext x; ring + have h_id_id_id : (fun x : ℝ => x * x * x) + = (fun x : ℝ => 1 * x ^ 3 + 0 * x ^ 2 + 0 * x + 0) := by funext x; ring + have h_id_id : (fun x : ℝ => x * x) + = (fun x : ℝ => 0 * x ^ 3 + 1 * x ^ 2 + 0 * x + 0) := by funext x; ring + have h_id : (fun x : ℝ => x) + = (fun x : ℝ => 0 * x ^ 3 + 0 * x ^ 2 + 1 * x + 0) := by funext x; ring + rw [h_α1α2α3, h_α1α2, h_α1α3, h_α2α3, h_α1, h_α2, h_α3] + -- For the RHS unfolding, rewrite (fun x => x * x * x) etc. in cubic form. + conv_rhs => + rw [show (fun x : ℝ => x * x * x) = (fun x : ℝ => 1 * x ^ 3 + 0 * x ^ 2 + 0 * x + 0) + from by funext x; ring, + show (fun x : ℝ => x * x) = (fun x : ℝ => 0 * x ^ 3 + 1 * x ^ 2 + 0 * x + 0) + from by funext x; ring] + -- Apply the cubic helper to all `gibbsExpectation` calls (eight on LHS, four on RHS). + rw [gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht (b₁ * b₂ * b₃) + (a₁ * b₂ * b₃ + b₁ * a₂ * b₃ + b₁ * b₂ * a₃) + (a₁ * a₂ * b₃ + a₁ * b₂ * a₃ + b₁ * a₂ * a₃) (a₁ * a₂ * a₃), + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht + (b₁ * b₂) (a₁ * b₂ + a₂ * b₁) (a₁ * a₂) 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht + (b₁ * b₃) (a₁ * b₃ + a₃ * b₁) (a₁ * a₃) 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht + (b₂ * b₃) (a₂ * b₃ + a₃ * b₂) (a₂ * a₃) 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht b₁ a₁ 0 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht b₂ a₂ 0 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht b₃ a₃ 0 0, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht 0 0 0 1, + gibbsExp_anharmonic_cubic_eq hlam hgamma hdisc ht 0 0 1 0] + ring + +/-! ## Headline -/ + +/-- **Affine generalisation of the anharmonic-κ₃ asymptotic.** + +For the 1D anharmonic potential `L(x) = (λ/2)x² + (α/6)x³ + (γ/24)x⁴` +with `λ, γ > 0` and the discriminant condition `α² < 3λγ`, and three +affine observables `(a₁ x + b₁, a₂ x + b₂, a₃ x + b₃)`, + + `t² · κ₃(α₁, α₂, α₃) → a₁ · a₂ · a₃ · (-α/λ³)` as `t → ∞`. + +The constants `bᵢ` drop because the joint third cumulant vanishes on +constant slots; the multipliers `aᵢ` pull through by trilinearity. -/ +theorem kappa3_anharmonic_shifted_affine_asymptotic + {lam alpha gamma : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) + (a₁ a₂ a₃ b₁ b₂ b₃ : ℝ) : + Filter.Tendsto + (fun t : ℝ => t ^ 2 * Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => a₂ * x + b₂) t + (fun x : ℝ => a₁ * x + b₁) (fun x : ℝ => a₃ * x + b₃)) + Filter.atTop + (nhds (a₁ * a₂ * a₃ * (-alpha / lam ^ 3))) := by + -- Tide 9: `t² · κ₃[id, id, id] → -α/λ³`. + have h_id := kappa3_anharmonic_id_id_id_asymptotic hlam hgamma hdisc + -- Multiply by `a₁ * a₂ * a₃`. + have h_scaled : Filter.Tendsto + (fun t : ℝ => a₁ * a₂ * a₃ * (t ^ 2 * + Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => x) t (fun x : ℝ => x) (fun x : ℝ => x))) + Filter.atTop + (nhds (a₁ * a₂ * a₃ * (-alpha / lam ^ 3))) := + h_id.const_mul (a₁ * a₂ * a₃) + -- Use the multilinear identity (eventually for `t > 0`) to rewrite the limit. + apply h_scaled.congr' + filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with t ht + -- For `t > 0`, the affine kappa3 equals `a₁ a₂ a₃ · κ₃[id, id, id]`. + rw [kappa3_anharmonic_shifted_affine_eq_smul hlam hgamma hdisc ht a₁ a₂ a₃ b₁ b₂ b₃] + ring + +end OneD + +end Laplace diff --git a/retrospectives/2026-05-07-tide-gibbscov-algebra.tex b/retrospectives/2026-05-07-tide-gibbscov-algebra.tex new file mode 100644 index 0000000..04c861d --- /dev/null +++ b/retrospectives/2026-05-07-tide-gibbscov-algebra.tex @@ -0,0 +1,321 @@ +\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{\iota}} +\newunicodechar{φ}{\ensuremath{\varphi}} +\newunicodechar{ψ}{\ensuremath{\psi}} +\newunicodechar{₁}{\ensuremath{_1}} +\newunicodechar{₂}{\ensuremath{_2}} +\newunicodechar{·}{\ensuremath{\cdot}} + +\title{Tide retrospective:\\generic algebra for \texttt{gibbsExpectation} and \texttt{gibbsCov}} +\author{Daniel Murfet} +\date{7 May 2026} + +\begin{document} +\maketitle + +\begin{abstract} +A short infrastructure tide. The 1D and multivariate base Gibbs files +in \texttt{laplace} carried the definitions of $\langle\cdot\rangle_t$ +and $\mathrm{Cov}_t[\cdot,\cdot]$ but only the lone constant-collapse +lemma $\langle c\rangle_t = c$. Every downstream consumer that wanted +bilinearity, scalar pulling, or the constant case bashed through +\texttt{unfold gibbsExpectation} and reproved the same algebraic +identities by hand — most visibly in the affine-observable proofs in +\texttt{OneD/Quartic.lean} (1D) and \texttt{TwoD/PureQuartic.lean} / +\texttt{TwoD/SemiDegenerate.lean} (2D). This tide adds the missing +algebra in parallel to both \texttt{Laplace/Gibbs.lean} and +\texttt{Laplace/Multi/Basic.lean}: 11~lemmas each side, 245~lines +total, single session, zero \texttt{sorry}, zero +\texttt{native\_decide}, zero \texttt{axiom}. The deliberation step +converged on Candidate~B (mirror across both base files) over A +(1D-only) or C (B plus an affine corollary that belongs in I3). +GPT-5.5~Pro flagged one strengthening worth taking — the constant-cov +lemma is unconditional via a $Z=0$ case-split rather than carrying a +\texttt{hZ} hypothesis. No numerical sanity check was feasible +(structural identities), and none was faked. +\end{abstract} + +\section{Setting} + +The cross-project survey of 7~May identified three classes of next +moves on the laplace shoreline: strict improvements of recent tides, +strategic refactors, and new-repo expansions. Item I2 sat in the +strategic-refactor class: the GPT-5.5~Pro consult at Tide~12 +(separable-potential abstraction) had recommended introducing +\texttt{gibbsCov\_symm}, \texttt{gibbsCov\_add\_left/right}, +\texttt{gibbsCov\_const\_left/right}, and +\texttt{gibbsCov\_smul\_left/right} in the base Gibbs files, observing +that ``once landed, the affine-covariance template becomes essentially +trivial.'' The deferred I3 (an explicit affine-covariance theorem) +and the strict-improvement candidates C1 (harmonic-side affine +$\kappa_3$) and G2 (anharmonic-side affine $\kappa_3$) all wait on the +same missing layer. + +The seabed was \texttt{laplace} at commit \texttt{141997c} +(post-G4)\footnote{Tide G4: \texttt{harmonic-gibbsobservable-monomials}, +397~lines; the most recent landed tide on \texttt{main} before this +one. See \texttt{retrospectives/2026-05-07-tide-harmonic-gibbsobservable-monomials.tex}.}. +The two base files +\texttt{Laplace/Gibbs.lean} (65~lines) and +\texttt{Laplace/Multi/Basic.lean} (55~lines) defined +\texttt{partitionFunction}, \texttt{gibbsExpectation}, +\texttt{gibbsCov} and only \texttt{gibbsExpectation\_const} (the 1D +lone derived lemma; the multi side had no derived lemmas at all). A +quick grep of consumer files confirmed the gap was load-bearing: +the affine quartic covariance and its 2D pure-quartic +analogue\footnote{Specifically, \texttt{gibbsCov\_first\_order\_rate\_sharp} +in \texttt{Laplace/OneD/Quartic.lean} (lines 307--349) and the +unnamed affine cov theorem in \texttt{Laplace/TwoD/PureQuartic.lean} +(lines 297--475).} +reproved bilinearity inline at roughly 30~and 180~lines respectively, +almost all bookkeeping. + +The deliberation step\footnote{Recorded in +\texttt{projects/primer/tide-log/2026-05-07-tide-gibbscov-algebra.md} +with the verbatim GPT-5.5~Pro response in +\texttt{gpt55\_tide\_gibbscov\_algebra\_v1.md}.} weighed three +candidates: A~(1D only, $\sim$120 lines), B~(parallel both, +$\sim$220), C~(B plus the affine-bilinear corollary $\sim$280). +Both Claude and GPT voted B. A~is too small strategically (the heavy +2D consumers live on the multi side); C~bundles a consumer-facing +theorem that mixes in extra subtleties (Gibbs-weight integrability) +and morally belongs in I3, not I2. B is one conceptual unit mirrored +across the repo's two parallel foundations. + +\section{The thing formalised} + +The headline is not a single theorem but a small algebra package added +in parallel to both base files. For the 1D file (the multi version is +literal-substitution-equivalent), the eleven lemmas are: + +\begin{verbatim} +namespace Laplace + +lemma gibbsExpectation_smul (L : ℝ → ℝ) (t : ℝ) (c : ℝ) (φ : ℝ → ℝ) : + gibbsExpectation L t (fun x => c * φ x) = c * gibbsExpectation L t φ + +lemma gibbsExpectation_zero (L : ℝ → ℝ) (t : ℝ) : + gibbsExpectation L t (fun _ => 0) = 0 + +lemma gibbsExpectation_add (L : ℝ → ℝ) (t : ℝ) (φ₁ φ₂ : ℝ → ℝ) + (h₁ : Integrable (fun x => φ₁ x * Real.exp (-(t * L x)))) + (h₂ : Integrable (fun x => φ₂ x * Real.exp (-(t * L x)))) : + gibbsExpectation L t (fun x => φ₁ x + φ₂ x) + = gibbsExpectation L t φ₁ + gibbsExpectation L t φ₂ + +lemma gibbsCov_symm (L : ℝ → ℝ) (t : ℝ) (φ ψ : ℝ → ℝ) : + gibbsCov L t φ ψ = gibbsCov L t ψ φ + +lemma gibbsCov_smul_left -- and _right by symm +lemma gibbsCov_const_left -- and _right by symm; unconditional +lemma gibbsCov_add_left -- and _right by symm; needs four Integrable hyps +lemma gibbsCov_zero_left -- and _right; cheap simp corollaries +\end{verbatim} + +\noindent The hypothesis economy is sharp: +$\texttt{symm}$ and the four $\texttt{smul}$ lemmas need no hypotheses +at all (only unconditional Bochner-integral linearity); +$\texttt{const}$ is unconditional thanks to the $Z=0$ case-split (see +\S3); only $\texttt{add\_left/right}$ require the four +$\texttt{Integrable}$ hypotheses on the pre-divided weighted +observables (each $\varphi_i \cdot e^{-tL}$ alone, plus each +$\varphi_i \cdot \psi \cdot e^{-tL}$ for the cross-term inside the +covariance). The same pattern is mirrored verbatim in +\texttt{Laplace.Multi}, with $(\iota \to \mathbb{R})$ replacing +$\mathbb{R}$. + +\section{Proof strategy} + +The covariance-level proofs all factor through the +expectation-level primitives, which in turn route through three +unconditional Mathlib lemmas: +\texttt{MeasureTheory.integral\_const\_mul} (used by +$\texttt{gibbsExpectation\_smul}$), +\texttt{MeasureTheory.integral\_add} (used by +$\texttt{gibbsExpectation\_add}$, the only place integrability +is mathematically necessary), and field arithmetic +(\texttt{mul\_div\_assoc}, \texttt{add\_div}, \texttt{ring}). +The covariance lemmas then follow by unfolding +$\mathrm{Cov}_t[\varphi, \psi] = \langle \varphi\psi\rangle_t - \langle\varphi\rangle_t \langle\psi\rangle_t$ +and rewriting with the expectation primitives plus a +\texttt{ring}-style cleanup. + +The minor wrinkle is the constant-cov lemma. The natural proof routes +through $\langle c\rangle_t = c$, which holds only when $Z(t) \neq 0$. +We could keep $\texttt{hZ}$ as an explicit hypothesis, but as +GPT-5.5~Pro pointed out, when $Z(t) = 0$ Lean's +$\texttt{x / 0 = 0}$ convention collapses every Gibbs expectation to +zero, so $\mathrm{Cov}_t[c, \psi] = 0 - 0 \cdot 0 = 0$ holds +unconditionally. The proof case-splits: +\begin{verbatim} + by_cases hZ : partitionFunction L t = 0 + · simp [gibbsCov, gibbsExpectation, partitionFunction] at hZ ⊢ + simp [hZ] + · simp only [gibbsCov] + rw [..., gibbsExpectation_smul, gibbsExpectation_const L t c hZ] + ring +\end{verbatim} +The first branch flattens both the covariance and the partition +function into the underlying integral, observes that the integral is +zero, and lets \texttt{simp} propagate. The second branch is the usual +substitution of $\langle c\rangle = c$. Both cleanly close. + +The right-slot variants (\texttt{\_right}) reduce to the left-slot +ones by $\texttt{gibbsCov\_symm}$. The right-slot integrability +hypotheses for $\texttt{gibbsCov\_add\_right}$ are stated in the +natural orientation (\texttt{$\varphi \cdot \psi_i \cdot e^{-tL}$}) +and reoriented by a one-line \texttt{simpa [mul\_comm]} before +delegating to $\texttt{gibbsCov\_add\_left}$. + +\section{Roadblocks and resolutions} + +Two minor frictions, both resolved on the first or second pass. + +\paragraph{Argument-order on \texttt{gibbsCov\_symm}.} The first +draft of \texttt{gibbsCov\_add\_right} used a bare +\texttt{gibbsCov\_symm $\varphi$ $\psi_2$} as a rewrite, mistakenly +omitting the $L$ and $t$ arguments. Lean reported a type mismatch on +the second positional argument. The fix was to spell the rewrites +fully: \texttt{rw [gibbsCov\_symm L t $\psi_1$ $\varphi$, gibbsCov\_symm L t $\psi_2$ $\varphi$]}. +Two minutes lost; promoted to the lessons section as a reminder that +positional-argument economy is fragile when a downstream rewrite +needs to target exactly two of three structurally-similar subterms. + +\paragraph{Unconditional constant-cov.} The first instinct was to +keep \texttt{hZ} in \texttt{gibbsCov\_const\_left} and let a future +cleanup handle the strengthening. GPT-5.5~Pro flagged the unconditional +form as a free win: ``if \texttt{partitionFunction L t = 0}, then +every \texttt{gibbsExpectation $\ldots$ / 0} collapses to \texttt{0}, +so covariance with a constant is still \texttt{0}.'' The +case-split proof above closed in one shot. Net cost: three lines +beyond the natural-path proof; the value is one fewer hypothesis at +every consumer site. + +There were no thrashing episodes, no architectural pivots, and no +counterexample-driven plan changes. The lemmas are mechanical from +the definitions; the deliberation step did the substantive work. + +\section{What was Mathlib, what was new} + +\paragraph{Mathlib provided.} +\texttt{MeasureTheory.integral\_const\_mul} (real-valued, \texttt{RCLike} +instance, unconditional) and +\texttt{MeasureTheory.integral\_add} (the conditional additivity that +forces the four \texttt{Integrable} hypotheses on the cov-add lemmas). +Plus the usual algebraic background: \texttt{mul\_comm}, +\texttt{mul\_div\_assoc}, \texttt{add\_div}, \texttt{ring}. + +\paragraph{What was new.} The algebra layer itself: 11~lemmas per +side, 245~lines total. No new Mathlib lemmas were upstreamed because +nothing in this Tide is general enough to belong in Mathlib — +\texttt{gibbsCov} is repo-specific. The shape of the layer might +nonetheless be worth lifting, eventually: a generic +\texttt{Lebesgue.expectation} / \texttt{Lebesgue.cov} pattern with +parallel algebra lemmas for any $\sigma$-finite measure could replace +both the 1D and multi versions in the laplace repo, plus possibly +threepoint's \texttt{Threepoint.gibbsCov}. Not in scope here. + +\section{Lessons} + +\begin{itemize}[leftmargin=*] +\item \emph{For the laplace \texttt{CLAUDE.md}:} the +\texttt{x / 0 = 0} case-split idiom for unconditional algebra lemmas +on quotient definitions like +$\texttt{gibbsExpectation} = \texttt{integral} / \texttt{Z}$. The +recipe \texttt{by\_cases hZ : Z = 0} followed by +\texttt{simp [..., partitionFunction] at hZ $\vdash$; simp [hZ]} on +the zero branch and the natural-path proof on the nonzero branch is +short and idiomatic. Worth landing as a tactic note alongside the +existing \texttt{Pi.add} and \texttt{rpow\_natCast} entries. + +\item \emph{For the lean-formalisation skill:} the parallel-mirror +pattern. The two base files differ only by the underlying domain +($\mathbb{R}$ versus $\iota \to \mathbb{R}$); the proofs are +literal-substitution-equivalent because the underlying Mathlib +integration lemmas are parametric in the measurable space. Writing +the 1D version first, getting it to compile, and then doing a +mechanical copy-paste-rename for the multi side cost roughly half +again the time of doing only one side. This pattern recurs across +the laplace repo (\texttt{Quartic.lean} versus \texttt{TwoD/PureQuartic.lean}, +\texttt{Harmonic.lean} versus \texttt{TwoD/AddSeparable.lean}); the +duplication is real but predictable and worth the cost. + +\item \emph{For the tide skill:} the structural-identity case for +``Numerical sanity check.'' This Tide produced no closed-form +expectation (the lemmas \emph{are} structural identities, true by +\texttt{rfl}/\texttt{ring} from the definitions). The skill's +fallback ``not feasible: \emph{reason}'' was exactly the right move; +the alternative — fabricating a numerical check — would have wasted +time and produced a false signal. The tide-log entry records the +reason explicitly, so the next survey can see why the section is +short. +\end{itemize} + +\section{Follow-ups} + +\begin{itemize}[leftmargin=*] +\item \emph{I3 — affine-bilinear covariance.} Now a 5--10 line +derivation: +\[ + \mathrm{Cov}_t[a\varphi + c, \, b\psi + d] = ab \cdot \mathrm{Cov}_t[\varphi, \psi] +\] +follows by two applications each of \texttt{gibbsCov\_add\_left}, +\texttt{gibbsCov\_const\_left}, \texttt{gibbsCov\_smul\_left}, and +their right-slot symmetries. Worth a small dedicated tide that pins +the integrability hypotheses cleanly and exports it as a derived +theorem in \texttt{Laplace/Gibbs.lean} (and \texttt{Multi/Basic.lean}). + +\item \emph{C1 — harmonic-side affine $\kappa_3$.} Generalise from +$\kappa_3(x, x, x)$ to $\kappa_3(b\cdot x, a\cdot x, c\cdot x)$ via +multilinearity of $\kappa_3$. With the new +\texttt{gibbsCov\_add/smul} algebra and the existing harmonic +$\kappa_3$ identity, ${\sim}50$ lines on top of +\texttt{Threepoint/Harmonic.lean}. + +\item \emph{G2 — anharmonic-side affine $\kappa_3$.} Same shape as +C1 but for the anharmonic Gibbs measure. ${\sim}40$ lines on top of +\texttt{Laplace/OneD/AnharmonicKappa3.lean}. + +\item \emph{Cleanup pass on existing affine-cov proofs.} The most +satisfying use of this Tide will be the line-count reductions in +the four files\footnote{\texttt{Laplace/OneD/Quartic.lean}, +\texttt{Laplace/TwoD/PureQuartic.lean}, +\texttt{Laplace/TwoD/SemiDegenerate.lean}, +\texttt{Laplace/TwoD/AddSeparable.lean}.} that currently unfold +\texttt{gibbsExpectation} to reach the same algebraic identities now +captured by the new lemmas. A focused refactor tide (or a sequence of +small ones) would tighten ${\sim}300$ lines of bookkeeping into +${\sim}50$. Not strictly necessary — the existing proofs work — but +cost-positive once the algebra is in. + +\item \emph{Optional: bundle the hypotheses.} If the +\texttt{Integrable}-quadruples on the cov-add lemmas turn out to be +the dominant signature noise at consumer sites (likely after C1, G2, +and I3 land), a plain-\texttt{Prop} alias +\texttt{GibbsAddIntegrable L t $\varphi$ $\psi$} bundling the four +hypotheses would compress signatures without committing to typeclass +plumbing. Defer until the second downstream use shows it's worth it. +\end{itemize} + +\section*{Acknowledgements} + +The deliberation step's GPT-5.5~Pro consult (preserved at +\texttt{projects/primer/tide-log/gpt55\_tide\_gibbscov\_algebra\_v1.md}) +contributed the unconditional-const strengthening, the +direct-hypotheses-over-typeclass call, and the explicit reason to +prefer Candidate~B over A or C. The Tide~12 deliberation +(separable-potential abstraction, 6~May) is where the I2 candidate +originated; this Tide closes a follow-up that has been on the board +for less than a day. + +\end{document} diff --git a/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.pdf b/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.pdf new file mode 100644 index 0000000..84fc23b Binary files /dev/null and b/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.pdf differ diff --git a/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.tex b/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.tex new file mode 100644 index 0000000..0228a38 --- /dev/null +++ b/retrospectives/2026-05-07-tide-kappa3-affine-anharmonic.tex @@ -0,0 +1,313 @@ +\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{\alpha}} +\newunicodechar{β}{\ensuremath{\beta}} +\newunicodechar{γ}{\ensuremath{\gamma}} +\newunicodechar{λ}{\ensuremath{\lambda}} +\newunicodechar{μ}{\ensuremath{\mu}} +\newunicodechar{φ}{\ensuremath{\varphi}} +\newunicodechar{ψ}{\ensuremath{\psi}} +\newunicodechar{κ}{\ensuremath{\kappa}} + +\title{Tide retrospective:\\affine-observable $\kappa_3$ for the anharmonic Gibbs (G2)} +\author{Daniel Murfet} +\date{7 May 2026} + +\begin{document} +\maketitle + +\begin{abstract} +This retrospective records a 100-line trilinear strict-improvement of +Tide 9. Tide 9 proved +$t^2 \cdot \kappa_3(x, x, x) \to -\alpha/\lambda^3$ for the 1D anharmonic +Gibbs measure with potential $L = (\lambda/2)x^2 + (\alpha/6)x^3 + (\gamma/24)x^4$. +This tide upgrades the result to arbitrary $\mathrm{id}$-multiples +$(b\,x, a\,x, c\,x)$, giving +$t^2 \cdot \kappa_3(b\,x, a\,x, c\,x) \to -(abc)\,\alpha/\lambda^3$, +via the static factorisation +$\kappa_3(b\,x, a\,x, c\,x) = (abc)\cdot\kappa_3(x, x, x)$. +The factorisation is hypothesis-free — it follows by trilinearity of +$\kappa_3$ once each of the seven Gibbs expectations in +$\mathtt{Threepoint.kappa3}$'s definition has its scalar factor peeled +off via I2's just-landed +\texttt{gibbsExpectation\_smul}.\footnote{I2 (gibbsCov-algebra) landed +2026-05-07. Branch: \texttt{tide/gibbscov-algebra}.} +The asymptotic is then $\mathtt{Tendsto.const\_mul}\,(abc)$ on top of +Tide 9. Zero \texttt{sorry}, single session, build green on the first +attempt; the GPT-5.5~Pro deliberation agreed with the Claude draft and +flagged a deferred shifted-affine extension. +\end{abstract} + +\section{Setting} + +Tide 9 (anharmonic-$\kappa_3$, 6 May) proved +\[ + t^2 \cdot \kappa_3(\mathrm{volume}, L_{\lambda\alpha\gamma}, x, t, x, x) + \;\to\; -\alpha/\lambda^3 + \quad\text{as } t \to \infty +\] +for $L_{\lambda\alpha\gamma}(x) = (\lambda/2)x^2 + (\alpha/6)x^3 + (\gamma/24)x^4$, +under the discriminant condition $\alpha^2 < 3\lambda\gamma$.\footnote{Discriminant +condition guarantees the sextic Wick contractions in $\langle x^4\rangle_t$ stay +positive, so the asymptotic of the covariance $\langle x^2, x\rangle$ has the +sign Tide 9 records.} The slot tuple $(\mathrm{id}, \mathrm{id}, \mathrm{id})$ +specialises $\kappa_3$'s general $(A, \varphi, B)$ signature to all-identity +observables. Tide 9 was the first cross-repo bridge between the abstract +\texttt{kappa3} machinery in \texttt{threepoint} and the concrete anharmonic +asymptotics in \texttt{laplace}; its retrospective named the affine-observable +form as the natural multilinear strict-improvement and estimated $\sim$40 +lines. + +I2 (gibbsCov-algebra, 7 May) landed an unconditional Gibbs-expectation / +Gibbs-covariance algebra:\footnote{Eleven lemmas mirrored across +\texttt{Laplace/Gibbs.lean} and \texttt{Laplace/Multi/Basic.lean}: +\texttt{gibbsExpectation\_\{smul,add,zero,const\}} and +\texttt{gibbsCov\_\{symm,smul,const,add,zero\}}.} Of these, the only +load-bearing one for this tide is +$\texttt{gibbsExpectation\_smul} : \langle c\,\varphi\rangle_t = c \cdot \langle \varphi\rangle_t$, +which holds unconditionally (when the partition is zero, both sides are +zero). The trilinearity factorisation reduces to seven applications of +this identity plus a \texttt{ring} step to collect the scalar factor +$abc$; no \texttt{gibbsCov} algebra is needed. + +This tide was picked at 2026-05-07T20:55Z from candidate G2 in the v3 +candidates survey,\footnote{\texttt{projects/automation/log/2026-05-07-v3-tide-candidates-survey.md}.} +after a parallel session claimed C1 (the harmonic-side twin) at 20:54Z. +Together with the in-progress C1, the two land complete affine-observable +$\kappa_3$ instances across both harmonic and anharmonic sides on the +same day. + +\section{The thing formalised} + +Two new public theorems in \texttt{Laplace/OneD/AnharmonicKappa3.lean}. + +\paragraph{Theorem 1 (potential-agnostic factorisation).} For any +$L : \mathbb{R} \to \mathbb{R}$, $t \in \mathbb{R}$, and scalars +$a, b, c \in \mathbb{R}$, +\[ + \kappa_3(\mathrm{volume}, L,\; b \cdot x,\; t,\; a \cdot x,\; c \cdot x) + \;=\; + (a \cdot b \cdot c) \cdot \kappa_3(\mathrm{volume}, L,\; x,\; t,\; x,\; x). +\] +Lean signature: +\begin{quote}\small\ttfamily +theorem kappa3\_affine\_id\_id\_id\_eq\\ +\hspace*{1em}(L : ℝ → ℝ) (t : ℝ) (a b c : ℝ) :\\ +\hspace*{1em}Threepoint.kappa3 (volume) L\\ +\hspace*{3em}(fun x => b * x) t (fun x => a * x) (fun x => c * x)\\ +\hspace*{1em}= (a * b * c) * Threepoint.kappa3 (volume) L\\ +\hspace*{6em}(fun x => x) t (fun x => x) (fun x => x) +\end{quote} +The factorisation has no analytic preconditions: $\kappa_3$'s seven +ratio-of-integrals reduce, at $h = 0$, to seven +\texttt{Laplace.gibbsExpectation} ratios via the existing +\texttt{threepoint\_gibbsExp\_volume\_zero\_eq} bridge, and +\texttt{gibbsExpectation\_smul} is unconditional. + +\paragraph{Theorem 2 (anharmonic asymptotic).} For +$L_{\lambda\alpha\gamma}$ with $0 < \lambda$, $0 < \gamma$, +$\alpha^2 < 3\lambda\gamma$, and any $a, b, c \in \mathbb{R}$, +\[ + t^2 \cdot \kappa_3(\mathrm{volume}, L_{\lambda\alpha\gamma},\; + b \cdot x,\; t,\; a \cdot x,\; c \cdot x) + \;\to\; -(a \cdot b \cdot c) \cdot \alpha/\lambda^3 + \quad \text{as } t \to \infty. +\] +Lean signature: +\begin{quote}\small\ttfamily +theorem kappa3\_anharmonic\_affine\_asymptotic\\ +\hspace*{1em}\{lam alpha gamma : ℝ\}\\ +\hspace*{1em}(hlam : 0 < lam) (hgamma : 0 < gamma) (hdisc : alpha\^{}2 < 3 * lam * gamma)\\ +\hspace*{1em}(a b c : ℝ) :\\ +\hspace*{1em}Filter.Tendsto\\ +\hspace*{2em}(fun t : ℝ => t\^{}2 * Threepoint.kappa3 (volume)\\ +\hspace*{4em}(anharmonicPotential lam alpha gamma)\\ +\hspace*{4em}(fun x => b * x) t (fun x => a * x) (fun x => c * x))\\ +\hspace*{2em}Filter.atTop\\ +\hspace*{2em}(nhds (-(a * b * c) * alpha / lam\^{}3)) +\end{quote} +The hypotheses are exactly those of Tide 9: trilinearity of $\kappa_3$ in +the three observable slots costs nothing analytically. + +\section{Proof strategy} + +\paragraph{Theorem 1.} The key observation is that +$\mathtt{Threepoint.kappa3}$ unfolds to seven $\mathtt{gibbsExp}$ +terms,\footnote{Specifically: $\langle\varphi A B\rangle$, +$\langle\varphi A\rangle\langle B\rangle$, +$\langle\varphi B\rangle\langle A\rangle$, +$\langle A B\rangle\langle\varphi\rangle$, and +$\langle\varphi\rangle\langle A\rangle\langle B\rangle$ — a polynomial +of total degree at most three in the seven scalar values.} all +evaluated at $h = 0$. The bridging lemma +\texttt{threepoint\_gibbsExp\_volume\_zero\_eq} (already in laplace, +from Tide 9) routes each one through to +\texttt{Laplace.gibbsExpectation}, after which the seven integrand +$\lambda$-binders carry products like +$(\mathtt{fun}\;x \mapsto a\,x)\,w \cdot (\mathtt{fun}\;x \mapsto b\,x)\,w$ +that are not yet syntactically in the canonical scaled-monomial form. +A \texttt{funext;\,ring} cleanup\footnote{Seven such +\texttt{have h\_X : (fun w => ...) = (fun w => K * w\^{}n)} steps: +$abc \cdot w^3$, $ab \cdot w^2$, $ac \cdot w^2$, $bc \cdot w^2$, plus +the three $a w$, $b w$, $c w$ singletons, and the four RHS-side +identity-only forms $w^3$ and $w^2$.} forces them into the canonical +shapes. \texttt{gibbsExpectation\_smul} then peels each scalar factor +out of its Gibbs expectation, leaving a pure ring identity in +$(a, b, c) \in \mathbb{R}^3$ and the four scalar values +$\langle w^3 \rangle$, $\langle w^2 \rangle$, $\langle w \rangle$, $\langle w \rangle^3$ +(which appear cubically in the standard polarisation +$\langle w^3 \rangle - 3\langle w^2\rangle\langle w\rangle + 2\langle w\rangle^3$). +\texttt{ring} closes. + +\paragraph{Theorem 2.} The new \texttt{Tendsto} is just $abc$ times +Tide 9's: $t^2 \cdot \kappa_3(b\,x, a\,x, c\,x) = abc \cdot t^2 \cdot \kappa_3(x, x, x)$ +pointwise. So the proof is +$\mathtt{Tendsto.const\_mul}\,(abc)$ applied to the Tide 9 conclusion, +combined with $\mathtt{Tendsto.congr'}$ rewriting the function under +the integral via Theorem 1. The constant +$-(a b c)\,\alpha/\lambda^3$ is normalised against +$abc \cdot (-\alpha/\lambda^3)$ by a one-line \texttt{ring}. + +\section{Roadblocks and resolutions} + +There were no roadblocks. The proof landed green on the first +\texttt{lake build}, in 4.7\,s after a warm Mathlib cache. This is +unusual but reasonable for a tide whose math is pure trilinearity over +a closed-form cumulant; the load-bearing analytic content is fully +imported from Tide 9. + +The deliberation step ran in parallel with the formalisation in this +session, on the assumption (correct, as it turned out) that the +candidate was uncontroversial. GPT-5.5~Pro's response, when it +returned 4 minutes after the proof had already landed, confirmed +Candidate~A as the right patch-sized theorem and noted three small +points worth recording: + +\begin{enumerate} +\item \emph{The asymptotic constant.} GPT confirmed the sign + $-(abc)\,\alpha/\lambda^3$ (no factor or sign error). Suggested + stating the limit as \texttt{((a * b * c) * (-α / λ\^{}3))} for + Lean ergonomics; the proof uses + \texttt{(-(a * b * c) * alpha / lam\^{}3)} and bridges the two + forms by a single \texttt{ring} step. Both work; one wonders if + Mathlib will eventually grow a normal-form simp set for these. +\item \emph{Algebra path.} ``You likely don't need \texttt{gibbsCov} + for this patch; direct \texttt{gibbsExpectation\_smul} + + \texttt{gibbsExpectation\_const} is enough.'' Exactly the route + taken; the I2 \texttt{gibbsCov} algebra is not used here. (It is + used in C1, the harmonic-side twin.) +\item \emph{Missed candidate (deferred).} ``The affine + strengthening is also true: + $\kappa_3(b\,x + d, a\,x + e, c\,x + f) = abc \cdot \kappa_3(x, x, x)$, + because \texttt{kappa3} kills constants in each slot + ($\mathbb{E}[1] = 1$ makes the cancellations exact). But I would + defer it unless you need shifted observables now.'' Recorded as a + follow-up; not picked up here. +\end{enumerate} + +\section{What was Mathlib, what was new} + +\paragraph{Mathlib.} \texttt{Tendsto.const\_mul} (constant multiple of +a limit), \texttt{Tendsto.congr'} (rewriting the function under a +limit), and \texttt{filter\_upwards} (eventual quantification). All +appear in dozens of laplace files; nothing new from Mathlib. + +\paragraph{Laplace seabed (existing).} Three load-bearing +imports:\footnote{Tide 9's +\texttt{kappa3\_anharmonic\_id\_id\_id\_asymptotic} (the headline), +its private bridge \texttt{threepoint\_gibbsExp\_volume\_zero\_eq}, +and I2's \texttt{Laplace.gibbsExpectation\_smul}.} +Tide 9's headline asymptotic, Tide 9's $h = 0$ bridge to +\texttt{Laplace.gibbsExpectation}, and I2's unconditional +scalar-out-of-Gibbs-expectation lemma. + +\paragraph{New.} Two public theorems and seven +\texttt{funext;\,ring}-style integrand-cleanup \texttt{have}-blocks +inside the proof of Theorem 1. Nothing new at the lemma library level. +The seven \texttt{funext}s are mechanical bookkeeping; a future tide +could fold them into a small simp set +``\texttt{push\_smul\_under\_lambda}'' but at one use it's not yet +cost-positive. + +\section{Lessons} + +\paragraph{Trilinearity tides land in one shot when the algebra is +already there.} I2 paid for itself the moment a strict-improvement of +this shape was on the board. The factorisation theorem is essentially +the I2 \texttt{gibbsExpectation\_smul} lemma applied seven times under a +\texttt{ring}-closure; if I2 hadn't been merged we'd have unfolded each +expectation manually. The lesson generalises to C1 (harmonic-side +twin) and is implicit in the I2 retrospective's follow-up list, which +flagged C1 and G2 specifically. + +\paragraph{Parallel deliberation + formalisation is fine when the +deliberation outcome is predictable.} Auto mode here meant launching +the GPT consult in the background and writing the Lean code in the +foreground, without waiting. The risk is wasted work if GPT had named +a different candidate; the actual outcome (GPT's vote agreed with +Claude's) suggests this risk is acceptable for trilinearity-shaped +tides where the candidate is essentially forced. Less acceptable for +hypothesis-class deliberations or when the proof technique is +genuinely contested. Don't generalise this to all tides. + +\paragraph{The ``\texttt{funext;\,ring} cleanup'' pattern is the +hidden cost of the seven-term \texttt{kappa3} unfolding.} Both Tide 9's +\texttt{kappa3\_id\_id\_id\_unfold} and this tide's +\texttt{kappa3\_affine\_id\_id\_id\_eq} carry the same boilerplate: +the seven Gibbs-expectation integrands need their lambdas reduced to +canonical scaled-monomial form before \texttt{gibbsExpectation\_smul} +can fire on them. A second use isn't yet a refactor trigger, but if a +third \texttt{kappa3} unfolding tide lands (e.g.\ for $\langle x^k \rangle$ +slots, or for the cross-cumulant $\kappa_3(\varphi, A, B)$ of the +patterning paper), the pattern is well-developed enough to extract. + +\section{Follow-ups} + +\begin{itemize} +\item \emph{Shifted-affine strengthening} (GPT's missed candidate). + $\kappa_3(b\,x + d, a\,x + e, c\,x + f) = abc \cdot \kappa_3(x, x, x)$ + via \texttt{gibbsExpectation\_const}-style cancellations + ($\mathbb{E}[1] = 1$). $\sim$50 extra lines on top of this tide. + Defer until a second consumer for shifted observables materialises. + +\item \emph{C1 (harmonic-side twin), in flight.} The harmonic case + $\kappa_3(b\,x, a\,x, c\,x) = abc \cdot \kappa_3(x, x, x) = 0$ + follows by the same trilinearity argument, on top of Tide 5's + harmonic-vanishing theorem.\footnote{\texttt{Threepoint.kappa3\_harmonic\_id\_id\_id\_eq\_zero}.} + Claimed by a parallel session at 20:54Z; should land within hours + of this retrospective. Together the two tides close the + affine-observable $\kappa_3$ pair for the 1D potentials currently + in laplace. + +\item \emph{Generic multilinear factorisation (Candidate~C, deferred).} + $\kappa_3(\mu, L, a A_0, t, b \varphi_0, c B_0) = abc \cdot \kappa_3(\mu, L, A_0, t, \varphi_0, B_0)$ + for arbitrary $A_0, \varphi_0, B_0$. Subsumes Theorem~1 as the + $(\mathrm{id}, \mathrm{id}, \mathrm{id})$ instance. GPT noted ``only + worth exporting if it is essentially free after the $h=0$ rewrite''; + worth checking against C1's proof to see whether a unified C-shaped + helper would shorten both files. If yes, a small refactor tide. + +\item \emph{Promote ``\texttt{push\_smul\_under\_lambda} simp set'' + on third use.} The seven-\texttt{funext} pattern (this tide and + Tide 9) is a candidate for automation but not yet cost-positive. + Third use triggers. + +\item \emph{\texttt{\textbackslash leanref}-tag the threepoint paper, pass 3.} + This tide is a corollary of the threepoint paper's multilinearity-of-$\kappa_3$ + remark.\footnote{Roughly the slot-by-slot linearity of cumulants + used implicitly in the patterning subtractions.} Once the next + process-tide tagging pass is run (currently candidate K2), tag the + multilinearity claim with \texttt{\textbackslash leanref} pinned to + this commit. +\end{itemize} + +\end{document} diff --git a/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.pdf b/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.pdf new file mode 100644 index 0000000..f0e2dc8 Binary files /dev/null and b/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.pdf differ diff --git a/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.tex b/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.tex new file mode 100644 index 0000000..876ae4a --- /dev/null +++ b/retrospectives/2026-05-07-tide-kappa3-shifted-affine-anharmonic.tex @@ -0,0 +1,337 @@ +\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{\alpha}} +\newunicodechar{β}{\ensuremath{\beta}} +\newunicodechar{γ}{\ensuremath{\gamma}} +\newunicodechar{λ}{\ensuremath{\lambda}} +\newunicodechar{μ}{\ensuremath{\mu}} +\newunicodechar{φ}{\ensuremath{\varphi}} +\newunicodechar{ψ}{\ensuremath{\psi}} +\newunicodechar{κ}{\ensuremath{\kappa}} + +\title{Tide retrospective:\\\emph{shifted-affine $\kappa_3$ for the +anharmonic Gibbs (G2 follow-up)}} +\author{Daniel Murfet} +\date{7 May 2026} + +\begin{document} +\maketitle + +\begin{abstract} +This retrospective records a 384-line shifted-affine extension of +the G2 tide.\footnote{G2 base linear case: branch +\texttt{tide/kappa3-affine-anharmonic}, commit \texttt{1b3e9bd}.} +G2 proved +$t^2 \cdot \kappa_3(b\,x, a\,x, c\,x) \to -(abc)\alpha/\lambda^3$ for +the 1D anharmonic Gibbs measure with potential $L = (\lambda/2)x^2 + +(\alpha/6)x^3 + (\gamma/24)x^4$. Its retrospective flagged the +shifted-affine extension +$\kappa_3(a_1 x + b_1, a_2 x + b_2, a_3 x + b_3) = a_1 a_2 a_3 \cdot +\kappa_3(x, x, x)$ as a deferred follow-up, estimated $\sim$50 extra +lines for the constant-observable plumbing. This tide lands that +follow-up. The actual cost was higher — $\sim$270 lines of new +content, driven by integrability bookkeeping needed when constant +terms in the integrand make I2's additivity lemma load-bearing +(rather than just the scalar-pull lemma, which sufficed for G2's +unshifted case). Single session; build green on the first attempt +after a small rewrite re-targeting; zero sorry, axiom, or +native\_decide. The numerical sanity check GPT-5.5 Pro recommended +(the \emph{exact} finite-$t$ identity, not just the asymptotic) +confirmed the multilinear factorisation to machine precision over a +five-by-four parameter sweep. +\end{abstract} + +\section{Setting} + +The base G2 tide proved that for any scalars $a, b, c \in +\mathbb{R}$, +\[ + \kappa_3(b\,x, a\,x, c\,x) \;=\; (abc) \cdot \kappa_3(x, x, x) +\] +as a static identity in any potential $L$, then specialised to the +anharmonic Gibbs measure to recover Tide 9's asymptotic with an extra +$abc$ factor. The proof routed every \texttt{gibbsExp} call through +Tide 9's $h = 0$ bridge to \texttt{Laplace.gibbsExpectation}, then +peeled scalars one by one via I2's +\texttt{gibbsExpectation\_smul}.\footnote{\texttt{gibbsExpectation\_smul +L t c $\varphi$ : $\langle c\,\varphi\rangle = c\,\langle +\varphi\rangle$} is unconditional, no integrability needed — that is +why the unshifted case lands cleanly in $\sim$100 lines.} + +The retrospective for that tide named the shifted extension as a +follow-up that ``defer until a second consumer for shifted observables +materialises'' but estimated only $\sim$50 lines. The estimate was +optimistic by a factor of five, for a structural reason worth +recording. + +\section{The thing formalised} + +\begin{quote}\itshape +For the 1D anharmonic potential $L_{\lambda\alpha\gamma}(x) = +(\lambda/2)x^2 + (\alpha/6)x^3 + (\gamma/24)x^4$ with $\lambda > 0$, +$\gamma > 0$, $\alpha^2 < 3\lambda\gamma$, and arbitrary scalars +$a_1, a_2, a_3, b_1, b_2, b_3 \in \mathbb{R}$: +\[ + t^2 \cdot \kappa_3\bigl(\mathrm{vol},\,L,\,a_2 x + b_2,\,t,\,a_1 x + + b_1,\,a_3 x + b_3\bigr) \;\longrightarrow\; a_1 a_2 a_3 \cdot + (-\alpha/\lambda^3) \quad\text{as } t \to \infty. +\] +The constants $b_i$ drop because the third joint cumulant vanishes +on constant slots; the multipliers $a_i$ pull through by trilinearity. +\end{quote} + +\noindent The Lean signature: +\begin{verbatim} +theorem kappa3_anharmonic_shifted_affine_asymptotic + {lam alpha gamma : ℝ} + (hlam : 0 < lam) (hgamma : 0 < gamma) + (hdisc : alpha ^ 2 < 3 * lam * gamma) + (a₁ a₂ a₃ b₁ b₂ b₃ : ℝ) : + Filter.Tendsto + (fun t : ℝ => t ^ 2 * Threepoint.kappa3 (volume : Measure ℝ) + (anharmonicPotential lam alpha gamma) + (fun x : ℝ => a₂ * x + b₂) t + (fun x : ℝ => a₁ * x + b₁) (fun x : ℝ => a₃ * x + b₃)) + Filter.atTop + (nhds (a₁ * a₂ * a₃ * (-alpha / lam ^ 3))) +\end{verbatim} + +This subsumes the base G2 theorem when $b_i = 0$ (by +\texttt{add\_zero}), but the two coexist in the file: the unshifted +form was useful within G2's own retrospective and is left alongside as +the primer-flavoured statement. + +\section{Proof strategy} + +The structural argument is the same as G2's: \texttt{Threepoint.kappa3} +is the symmetric joint third cumulant of three observables, so +\[ + \kappa_3(\alpha_1, \alpha_2, \alpha_3) = a_1 a_2 a_3 \cdot + \kappa_3(x, x, x) +\] +follows by trilinearity in the three slots and the standard fact that +$\kappa_3$ vanishes whenever any slot is constant. The Lean machinery +to extract this fact from +\[ + \kappa_3(\mathrm{vol}, L, A, t, \varphi, B) = \langle \varphi A B + \rangle - \langle \varphi A \rangle \langle B \rangle - \langle + \varphi B \rangle \langle A \rangle - \langle A B \rangle \langle + \varphi \rangle + 2 \langle \varphi \rangle \langle A \rangle + \langle B \rangle +\] +splits into three layers. + +\paragraph{Layer 1: bridging.} At $h = 0$ the +\texttt{Threepoint.gibbsExp} reduces to +\texttt{Laplace.gibbsExpectation}, regardless of the perturbation +direction $A$. Tide 9 already has this bridge as a private lemma; +G2 inlined a \texttt{simp}-shaped variant of it, and so does this +tide. Re-deriving locally costs five lines. + +\paragraph{Layer 2: cubic-polynomial expansion.} Each of the seven +\texttt{gibbsExpectation} calls in the unfolded $\kappa_3$ has an +integrand that, after \texttt{funext x; ring}, becomes a polynomial +$c_3 x^3 + c_2 x^2 + c_1 x + c_0$ in $x$ of degree at most three. A +single helper reduces such an integrand to a linear combination of +the four moments +$\langle x^3 \rangle, \langle x^2 \rangle, \langle x \rangle, 1$, +applying I2's expectation algebra (add, smul, const) in sequence. +The cubic helper is the bulk of the file ($\sim$120 lines, including +the four integrability witnesses). + +\paragraph{Layer 3: reduce to \texttt{ring}.} After the bridging and +the cubic helper fire on both sides of the desired identity, both +sides are polynomials in $(a_i, b_i, m_1, m_2, m_3)$ where $m_k$ +denotes $\langle x^k \rangle$. The closing tactic is +\texttt{ring}.\footnote{The symbolic identity was verified in +\texttt{sympy} as part of Step 2's numerical sanity, exactly as +\texttt{ring} sees it after expansion. The Lean proof and the sympy +script use identical algebra.} + +The base G2 tide skipped Layer 2 entirely: with $b_i = 0$, the +integrands have no constant terms, so +\texttt{gibbsExpectation\_smul} alone suffices and +\texttt{gibbsExpectation\_const} (the only lemma in I2's algebra +that carries an integrability or partition-positivity hypothesis) +never fires. That is why G2's $\sim$100 lines do not need the +integrability infrastructure that this tide spends $\sim$80 lines +establishing. + +\section{Roadblocks and resolutions} + +\paragraph{The race.} The \texttt{tide-pick} skill claimed G2 for me +at \texttt{2026-05-07T05:33:30Z} as a re-rank from C1 (which a +parallel session had taken at 05:25Z). I drafted candidates, +consulted GPT-5.5 Pro, and started Step 3 in the worktree. Some time +into Step 3, when first running \texttt{lake build}, two errors +surfaced: an unrelated \texttt{rewrite} pattern miss, and a +\texttt{kappa3\_anharmonic\_affine\_asymptotic has already been +declared}. The latter was the diagnostic: a parallel session had +shipped G2 to the same branch +(\texttt{tide/kappa3-affine-anharmonic}) before mine landed. + +The parallel session's solution was the unshifted case +$(b\,x, a\,x, c\,x)$. Its retrospective explicitly identified the +shifted-affine extension as a follow-up. So my work was not duplicate +— it was the strict-improvement that the parallel session had +deferred. The remediation: rename my theorems to +\texttt{kappa3\_anharmonic\_shifted\_affine\_*} and ship the file as +an additive layer on top of the parallel session's commit. The +resulting structure (G2 unshifted + this tide's shifted extension on +the same branch, neither subsuming the other in the public surface) +is unusual, but correct given the order of landing. + +\paragraph{Integrability bookkeeping.} The +\texttt{gibbsExpectation\_const $L$ $t$ $c$ hZ : $\langle c \rangle = +c$} lemma carries a $\mathtt{partitionFunction}$-non-zero hypothesis +\texttt{hZ : partitionFunction L t \char`\\ne 0}. For the anharmonic +potential with $t > 0$, this follows from +\texttt{integral\_exp\_pos}, which itself needs integrability of +\texttt{exp(-(t · L\textsubscript{anh}))} over $\mathbb{R}$. That +integrability is not directly in the seabed: Tide 9's $I_n$ / +$J_n$ machinery in \texttt{IntegralRemainder.lean} uses a +substitution-based scaling argument that does not surface a +\texttt{Integrable} witness for $x^n \cdot \exp(-t\,L_{\mathrm{anh}})$ +under the literal anharmonic measure. The fix: a +\texttt{integrable\_pow\_mul\_exp\_neg\_anharmonic} helper that +dominates by the Gaussian +$|x|^n \cdot \exp(-tc\,x^2)$ via +\texttt{anharmonic\_coercive}'s lower bound $L_{\mathrm{anh}}(x) \geq +c\,x^2$, then applies \texttt{Integrable.mono} against +\texttt{integrable\_abs\_pow\_mul\_exp\_neg\_mul\_sq}. About 20 lines. + +\paragraph{The single \texttt{rw} that didn't fire.} The first build +attempt also failed on an over-eager \texttt{rw} that tried to rewrite +the bare $(\mathtt{fun}\ x \Rightarrow x)$ in the +\texttt{kappa3\_volume\_unfold}-RHS to its cubic-helper-friendly form +$0 \cdot x^3 + 0 \cdot x^2 + 1 \cdot x + 0$. The pattern didn't match +because the RHS already had the bare lambda after Layer 1's bridging +\texttt{simp}. Resolution: don't rewrite it; \texttt{ring} handles +\texttt{gibbsExpectation L t (fun x \char`\=\char`\>\ x)} as an +opaque variable, and the LHS expansions all reduce to combinations +involving the same opaque term. Removing the offending \texttt{rw} +fixed the build on the second attempt. + +\section{What was Mathlib, what was new} + +\paragraph{Mathlib.} \texttt{integral\_exp\_pos} (positivity from +strict positivity of $\exp$), \texttt{Integrable.mono} +(domination), \texttt{Integrable.const\_mul} (scaling), +\texttt{Tendsto.const\_mul} and \texttt{Tendsto.congr'} (the standard +limit-massage pair from G2 and dozens of earlier laplace tides). All +familiar; no new Mathlib API surfaced. + +\paragraph{Laplace seabed (existing).} Tide 9's headline asymptotic +and its $h = 0$ bridge (re-derived locally because the original is +\texttt{private}), I2's expectation algebra, the anharmonic coercivity +bound, and Mathlib's Gaussian-form integrability +lemma.\footnote{Names: Tide 9's +\texttt{kappa3\_anharmonic\_id\_id\_id\_asymptotic} and +\texttt{threepoint\_gibbsExp\_volume\_zero\_eq}; +I2's \texttt{gibbsExpectation\_smul / \_add / \_const / \_zero} +in \texttt{Laplace.Gibbs}; \texttt{anharmonic\_coercive} in +\texttt{Laplace.OneD.Anharmonic}; and +\texttt{integrable\_abs\_pow\_mul\_exp\_neg\_mul\_sq} in +\texttt{Laplace.OneD.IntegralRemainder}.} + +\paragraph{New.} An anharmonic-side polynomial-times-exponential +integrability witness, a partition-positivity corollary, a +cubic-polynomial expansion helper, a local re-derivation of the +$\kappa_3$-at-volume bridge, and the two public +theorems.\footnote{Names: +\texttt{integrable\_pow\_mul\_exp\_neg\_anharmonic}, +\texttt{partitionFunction\_anharmonic\_pos}, +\texttt{gibbsExp\_anharmonic\_cubic\_eq}, +\texttt{kappa3\_volume\_unfold}, and the public +\texttt{kappa3\_anharmonic\_shifted\_affine\_eq\_smul} + +\texttt{kappa3\_anharmonic\_shifted\_affine\_asymptotic}.} +The cubic helper has the right shape to be promoted once a second +consumer materialises (e.g.\ a $\langle x^k \rangle_h$ tide via +I4's shift method); not yet a refactor trigger. + +\section{Lessons} + +\begin{itemize} +\item \emph{Race resolution at Step 3 needs a watch on the branch.} + The \texttt{tide-pick} skill's claim system handles races at the + survey level; Step 3 races (where two sessions advance the same + branch independently) are not handled. The empirical resolution + here was clean — the parallel session left a follow-up I picked up + — but a more conflicted race (e.g.\ both sessions targeting the + same theorem name) would have needed manual reconciliation. Worth + recording but not yet automation-ripe. +\item \emph{The G2 follow-up estimate was 5$\times$ low.} The + retrospective for the unshifted case estimated $\sim$50 lines; the + actual cost was $\sim$270 lines, driven entirely by the + integrability bookkeeping that arises only when constant terms + enter the integrand. Future tide estimates over constant-observable + extensions should account for the partition-positivity and + Gaussian-domination helpers ($\sim$80 lines of plumbing per + first-time use in a fresh potential class). +\item \emph{The cubic-polynomial expansion helper is the natural + ``second-use'' refactor target.} The pattern (rewrite integrand + as $c_3 x^3 + \dots + c_0$, then peel via I2's add / smul / const + algebra) is shape-portable to the harmonic case (C1) and to + higher-degree polynomial-observable expansions (e.g.\ a $\kappa_4$ + tide). At third use, promote to a generic potential-agnostic + helper. +\end{itemize} + +\section{Follow-ups} + +\begin{itemize} +\item \emph{Generic potential-agnostic shifted-affine $\kappa_3$ + identity.} This tide's private helper is fully algebraic in the + moments $m_1, m_2, m_3$; the only anharmonic-specific input is the + integrability witness. A generic potential-agnostic version for any + $L$ with a polynomial-up-to-degree-3 integrability bundle and + positive partition function would unify this tide with C1 (the + harmonic-side twin, currently in flight). About $\sim$80 lines of + refactoring; defer until C1 lands and the joint surface is visible. +\item \emph{Promote the cubic-polynomial expansion helper.} The + helper here is the natural ``poly of degree $\leq 3$'' Gibbs + expectation lemma. With C1's harmonic version and possibly an + N1 (generic-$k$ J-function) extension, three consumers could + materialise. Promotion target: a new + \texttt{Laplace.OneD.GibbsPolyExp} module, or eventually + \texttt{lean-common}. +\item \emph{Shifted-affine $\kappa_4$.} Once a $\kappa_4$ definition + lands in \texttt{Threepoint}, the same trilinear-into-quadrilinear + argument should give + $\kappa_4(\alpha_1, \alpha_2, \alpha_3, \alpha_4) = a_1 a_2 a_3 a_4 + \cdot \kappa_4(x, x, x, x)$. About $\sim$120 lines: a quadratic + expansion helper (degree $\leq 4$ polynomials) plus the unfolding. + Tide-shaped. +\end{itemize} + +\section*{Acknowledgements} + +GPT-5.5 Pro's deliberation at Step 2 contributed the +``\texttt{rewrite to moments + ring}'' tactic (Section~3, Layer~3), +the recommendation to keep the helper local for $t > 0$ rather than +all $t$, and the architectural advice not to over-abstract to a +potential-agnostic public lemma in this tide. The full consult is +preserved at +\texttt{projects/primer/tide-log/gpt55\_tide\_kappa3\_affine\_anharmonic\_v1.md}. +GPT also recommended the exact-finite-$t$ identity numerical check +(rather than only the asymptotic), which surfaced the +constants-only edge case (zero limit) and the $a_1 = 0$ case (zero +everywhere) — both validated to machine precision in the sympy + +scipy scripts. + +This Tide branched off the post-G2 tip on the same Tide branch as +G2 itself; the two land additively, with this tide's commit on top +of G2's retrospective.\footnote{Branch: +\texttt{tide/kappa3-affine-anharmonic}. G2 commits: +\texttt{1b3e9bd} (proof) + \texttt{225ab8d} (retrospective).} + +\end{document}