Tide: generic algebra for gibbsExpectation and gibbsCov#19
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>
4 tasks
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
Laplace/Gibbs.lean(1D) andLaplace/Multi/Basic.lean(multi):gibbsExpectation_smul/zero/add/const(multi-side_constnewly added; 1D pre-existing) andgibbsCov_symm/smul_left/smul_right/const_left/const_right/add_left/add_right/zero_left/zero_right.gibbsCov_const_*is unconditional via aZ = 0case-split — nohZhypothesis at consumer sites. OnlygibbsCov_add_*carryIntegrablehypotheses (four each, on the pre-divided weighted observables).Quartic.lean/TwoD/PureQuartic.lean/TwoD/SemiDegenerate.lean/TwoD/AddSeparable.lean.245 lines of Lean (commit
41a7b41); 321-line LaTeX retrospective (commitb844d7a). Single session, zerosorry, zeroaxiom, zeronative_decide. Fulllake buildclean.Tide log:
sri/projects/primer/tide-log/2026-05-07-tide-gibbscov-algebra.mdGPT consult:
sri/projects/primer/tide-log/gpt55_tide_gibbscov_algebra_v1.mdRetrospective:
retrospectives/2026-05-07-tide-gibbscov-algebra.texTest plan
lake buildcleanscripts/sorriesclean (0 sorry, 0 #exit, 0 native_decide, 0 axiom)🤖 Generated with Claude Code