Tide G3: third-moment asymptotic for the anharmonic Gibbs#17
Merged
Conversation
…partial) Foundational primitive for the upcoming `Threepoint.GibbsObservable` instances at the harmonic potential with monomial observables: the h = 0 conjunct of `GibbsObservable` reduces to a `simp [zero_mul, add_zero]`-style identity, independent of the observable. Two lemmas: - `harmonic_perturbed_numerator_zero_eq` for any `φ : ℝ → ℝ`. - `harmonic_perturbed_numerator_zero_eq_pow` specialising to `φ(x) = x^k`. The headline `harmonic_id_gibbsObservable_pow` and the analytic core (domination bound, dominated-differentiation invocation, HasDerivAt conjunct) remain. Tide log: sri/projects/patterning/tide-log/2026-05-07-tide-harmonic-gibbsobservable-monomials.md. G4 from the 7 May candidates survey. Imports Laplace.OneD.HarmonicGibbsRegularity (for Tide 10 plumbing) and Threepoint.CrossSusceptibility (for the GibbsObservable definition). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…tial)
Tide G4 from the 7 May candidates survey, first chunk: one
foundational primitive that discharges the first conjunct of every
`Threepoint.GibbsObservable` instance for the harmonic + linear setup,
independent of observable choice:
- harmonic_perturbed_numerator_zero_eq: ∫ φ·exp(-(t·((λ/2)x² + 0·x))) =
∫ φ·exp(-(t·(λ/2)x²)) for any φ : ℝ → ℝ.
Plus the monomial specialisation harmonic_perturbed_numerator_zero_eq_pow.
GPT-5.5 Pro's deliberation pivoted from the originally-planned
closed-form route (Candidate B, ~350 lines, requires a central
Gaussian-moment library Mathlib doesn't ship) to dominated
differentiation under the integral sign (Candidate D, generic in k,
~250-350 lines, reuses seabed integrability). The dominated-diff
core (Young-style domination bound, pointwise differentiability,
hasDerivAt_integral_of_dominated_loc_of_deriv_le invocation, and the
GibbsObservable instance wrapping) is sketched in
notes/gibbsobservable_monomials_handoff.md and will land in a
follow-up session.
Zero sorry / 0 axiom / 0 native_decide.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Smallest tide on the board. Packages the third moment ⟨x³⟩_t of the
anharmonic Gibbs measure as a user-facing asymptotic:
t² · ⟨x³⟩_t → -5α/(2λ³) as t → ∞
deferred from Tide 9 where it was internal to the proof of
cov_anharmonic_asymptotic.
Identity: ⟨x³⟩ = Cov[x², x] + ⟨x²⟩·⟨x⟩ (from gibbsCov definition).
Combined with cov_anharmonic_asymptotic, secondMoment_anharmonic_asymptotic,
and mean_anharmonic_asymptotic, the third moment falls out by Tendsto
algebra: t²·⟨x³⟩ = t²·Cov[x²,x] + (t·⟨x²⟩)·(t·⟨x⟩)
→ -2α/λ³ + (1/λ)·(-α/(2λ²)) = -5α/(2λ³).
~30 lines on top of Tide 9's existing infrastructure. Zero sorry.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
thirdMoment_anharmonic_asymptotictoLaplace/OneD/AnharmonicKappa3.lean— packaging the third moment ⟨x³⟩_t of the anharmonic Gibbs measure as a user-facing asymptotic:t² · ⟨x³⟩_t → -5α/(2λ³)ast → ∞.cov_anharmonic_asymptotic; this packages it as a separate theorem.⟨x³⟩ = Cov[x², x] + ⟨x²⟩·⟨x⟩(fromgibbsCovdefinition). Combined withcov_anharmonic_asymptotic,secondMoment_anharmonic_asymptotic, andmean_anharmonic_asymptotic, the third moment falls out by Tendsto algebra.sorry/axiom/native_decide.G3 from the 7 May candidates survey. Tide 9's retrospective named this as a deferred follow-up.
Test plan
lake buildcleanscripts/sorriesclean