refactor: golf proofs in HarmonicOscillator, IsExtrema, TotalDerivativeEquivalence, KineticTerm#1373

Draft

Vilin97 wants to merge 47 commits into

leanprover-community:masterfrom

Vilin97:golf-proofs

Commits on Jul 6, 2026

refactor: golf TotalDerivativeEquivalence, HarmonicOscillator, DampedHarmonicOscillator proofs

Vilin97
and
mistral-vibe
committed
refactor: golf total-derivative equivalence proofs

committed
fix: repair damped helper extraction

Vilin97
and
Claude Opus 4.8
committed
refactor: golf HarmonicOscillator trajectory_velocity proof and QFT linear independence proofs

Vilin97
and
mistral-vibe
committed

Commits on Jul 7, 2026

Commits on Jul 8, 2026

Commits on Jul 9, 2026

refactor: golf HarmonicOscillator Solution and KineticTerm proofs

Vilin97
and
mistral-vibe
committed

Commits on Jul 10, 2026

Commits on Jul 11, 2026

fix: restore compilation of HarmonicOscillator, PhysHermite, WickContraction, Space/Norm, and Units proofs

Vilin97
and
mistral-vibe
committed