Tide G2 + G2+: kappa3 affine + shifted-affine (anharmonic)#20
Merged
Conversation
Add the algebraic infrastructure for `gibbsCov` so that affine/multilinear strict-improvements (e.g. C1 harmonic-affine, G2 anharmonic-affine, the deferred I3 affine-covariance template from Tide 12) become near-trivial. Lemmas added in parallel to `Laplace/Gibbs.lean` (1D, scalar) and `Laplace/Multi/Basic.lean` (multi, `(ι → ℝ)`): Expectation level: - `gibbsExpectation_smul` (no hypotheses) - `gibbsExpectation_zero` (no hypotheses) - `gibbsExpectation_add` (Integrable hypotheses) - `gibbsExpectation_const` for the multi side (1D version pre-existing) Covariance level: - `gibbsCov_symm` (no hypotheses) - `gibbsCov_smul_left/right` (no hypotheses) - `gibbsCov_const_left/right` (unconditional via Z=0 case-split) - `gibbsCov_add_left/right` (Integrable hypotheses) - `gibbsCov_zero_left/right` simp corollaries `gibbsCov_const_*` is unconditional because when `Z(t) = 0` every expectation collapses to `0` via the `_/0 = 0` convention; otherwise the proof routes through `gibbsExpectation_const`. Both Claude and GPT-5.5 Pro voted Candidate B (algebra mirrored across both base files) over Candidate A (1D only) and Candidate C (B + the affine-bilinear corollary, which belongs in I3). Direct `Integrable` hypotheses, no `GibbsIntegrable` typeclass, no `LinearMap` refactor. Tide log: `projects/primer/tide-log/2026-05-07-tide-gibbscov-algebra.md` GPT consult: `projects/primer/tide-log/gpt55_tide_gibbscov_algebra_v1.md` 🌊 Generated with the [Tide skill](https://github.com/timaeus-research/sri/blob/main/.claude/skills/tide/SKILL.md) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Single-session infrastructure tide. 245 lines added across Laplace/Gibbs.lean (1D) and Laplace/Multi/Basic.lean (multi); 11 lemmas per side covering gibbsExpectation_smul/zero/add (1D const pre-existing, multi const newly added) and the seven covariance lemmas (gibbsCov_symm/const/smul/add, both slots) plus zero-corollary simp lemmas. Hypothesis economy: only gibbsCov_add_left/right need Integrable hypotheses (four each, on the pre-divided weighted observables); gibbsCov_const_left/right is unconditional via a Z=0 case-split. Retrospective records the deliberation (Claude+GPT both voted Candidate B, mirror across both base files), the unconditional- const strengthening GPT recommended, and the four follow-up tides this unblocks (I3 affine-bilinear, C1/G2 affine kappa3 strict- improvements, the cleanup pass on existing affine-cov proofs). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… Tide 9
Two new theorems on top of `Laplace/OneD/AnharmonicKappa3.lean`:
* `kappa3_affine_id_id_id_eq` — for any potential `L` and scalars
`a, b, c : ℝ`,
κ₃(volume, L, b·x, t, a·x, c·x) = (abc) · κ₃(volume, L, x, t, x, x).
Hypothesis-free; built from `gibbsExpectation_smul` (I2's algebra)
and `threepoint_gibbsExp_volume_zero_eq` (Tide 9's bridge).
* `kappa3_anharmonic_affine_asymptotic` — for `L = anharmonicPotential
λ α γ`, `0 < λ`, `0 < γ`, `α² < 3λγ`, and any `a, b, c : ℝ`,
t² · κ₃(volume, L, b·x, t, a·x, c·x) → -(abc)·α/λ³ as t → ∞.
Tide 9's case `(a, b, c) = (1, 1, 1)` × trilinearity.
101 lines, 0 sorry, 0 #exit, 0 native_decide, 0 axiom.
Tide-log: `projects/patterning/tide-log/2026-05-07-tide-kappa3-affine-anharmonic.md`.
GPT-5.5 Pro consult: `projects/patterning/tide-log/gpt55_tide_kappa3_affine_anharmonic_v1.md`.
7-page retrospective covering the trilinear strict-improvement of Tide 9. Both new theorems (`kappa3_affine_id_id_id_eq` factorisation and `kappa3_anharmonic_affine_asymptotic` corollary), the load-bearing role of I2's `gibbsExpectation_smul`, the parallel deliberation+formalisation pattern (single-shot landing), and three follow-ups (shifted-affine, generic Candidate C, simp-set automation) recorded. Tex builds clean (no overfull-hbox warnings). PDF tracked.
The base linear case (kappa3 vol L (b·x) t (a·x) (c·x) ~ -(abc)·α/λ³) landed in 1b3e9bd as Tide G2. That tide's retrospective flagged the shifted-affine extension `kappa3 vol L (a₂x+b₂) t (a₁x+b₁) (a₃x+b₃) ~ a₁a₂a₃·(-α/λ³)` as a deferred follow-up, estimated ~50 extra lines. This commit lands that follow-up. The constants `b_i` drop because κ₃ vanishes on constant slots (joint third cumulant is multilinear). Two new public-named theorems: - `kappa3_anharmonic_shifted_affine_eq_smul` (private helper): `kappa3 vol L (a₂x+b₂) t (a₁x+b₁) (a₃x+b₃) = a₁·a₂·a₃ · kappa3 vol L id t id id` for `t > 0`, anharmonic L with discriminant condition. - `kappa3_anharmonic_shifted_affine_asymptotic` (public): the full Tendsto t² · κ₃[α₁,α₂,α₃] → a₁·a₂·a₃ · (-α/λ³). Strict-improvement of the linear `kappa3_anharmonic_affine_asymptotic` (subsumes it when b_i = 0 by add_zero). Infrastructure: a coercivity-driven `integrable_pow_mul_exp_neg_anharmonic` witness for `xⁿ · exp(-tL)` (k = 0, 1, 2, 3) plus `partitionFunction_anharmonic_pos` (via `integral_exp_pos`), required because gibbsExpectation_const carries hZ ≠ 0. A cubic-polynomial expansion helper `gibbsExp_anharmonic_cubic_eq` reduces any `⟨c₃x³+c₂x²+c₁x+c₀⟩` to a linear combination of moments. The proof reduces to `ring` over `(a_i, b_i, m_1, m_2, m_3)` after seven `funext;ring` integrand cleanups. Numerical sanity (sympy + scipy) confirmed the exact finite-t identity to machine precision. 384 lines total; 0 sorry / 0 axiom / 0 native_decide. Build green (modulo pre-existing warnings in Multi/* files).
…follow-up) Records the 270-line shifted-affine extension of G2 landed in 0841f48 (this same branch). Notes the Step 3 race (parallel session shipped G2 first; my work was the deferred follow-up they flagged in their retrospective), the integrability bookkeeping that drove the size from G2's estimated 50 to the actual 270 lines, and the cubic-polynomial expansion helper as a candidate for refactor at third use. Three follow-ups: generic potential-agnostic version, helper promotion, and a kappa4 analogue.
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
Two strict-improvements of Tide 9 (
kappa3_anharmonic_id_id_id_asymptotic), stacked on PR #19 (I2 gibbscov-algebra):kappa3_affine_id_id_id_eq(potential-agnostic trilinear factorisation) andkappa3_anharmonic_affine_asymptotic(t² · κ₃(b·x, a·x, c·x) → -(abc)·α/λ³). 101 lines inLaplace/OneD/AnharmonicKappa3.lean.(a_i x + b_i). 270 lines inLaplace/OneD/AnharmonicKappa3Affine.lean. Identified as G2's own follow-up; landed by a parallel session on the same branch.Total: 4 commits (2 proof + 2 retrospective), 0 sorry / 0 axiom / 0 native_decide on either piece.
Stacked-PR note
Base is
tide/gibbscov-algebra(PR #19) because both pieces use I2'sgibbsExpectation_smul. Retarget tomainafter #19 merges, then merge this PR.Test plan
lake build Laplace.OneD.AnharmonicKappa3— green (4.7s warm)lake build Laplace.OneD.AnharmonicKappa3Affine— greenscripts/sorries— 0 sorry, 0 #exit, 0 native_decide, 0 axiom on the new files🤖 Generated with Claude Code