Tide G2 + G2+: kappa3 affine + shifted-affine (anharmonic)

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

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

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

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