refactor: golf proofs in HarmonicOscillator, IsExtrema, TotalDerivativeEquivalence, KineticTerm#1373
Draft
Vilin97 wants to merge 47 commits into
Draft
refactor: golf proofs in HarmonicOscillator, IsExtrema, TotalDerivativeEquivalence, KineticTerm#1373Vilin97 wants to merge 47 commits into
Vilin97 wants to merge 47 commits into
Conversation
…HarmonicOscillator proofs - isTotalTimeDerivative_explicit: replace fderiv.fst/snd + by_contra hacks with fderiv_prodMk - trajectories_unique: inline dsub, simplify energy nonnegativity, fix resolve_left - fderiv_comp_val_eq_deriv: extract repeated lemma in DampedHarmonicOscillator Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Contributor
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
Vilin97
added a commit
to Vilin97/physlib
that referenced
this pull request
Jul 6, 2026
Move the remaining Mistral golf from leanprover-community#1364 to leanprover-community#1373: simplify isTotalTimeDerivative_neg, totalTimeDerivative_contDiff, and totalTimeDerivative_hasVarGradientAt_equivalence. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Move the remaining Mistral golf from leanprover-community#1364 to leanprover-community#1373: simplify isTotalTimeDerivative_neg, totalTimeDerivative_contDiff, and totalTimeDerivative_hasVarGradientAt_equivalence. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Move fderiv_comp_val_eq_deriv out of the section doc block so the four trajectory derivative proofs can see it, and remove unused simp arguments in trajectories_unique. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…inear independence proofs - Simplify trajectory_velocity h1 proof using fderiv_mul_const and congr - Replace convoluted AddSemiconjBy.eq_zero_iff proofs with simpler h2.trans h1 approach in basis_linear_independent, basis!_linear_independent - Simplify basisa_linear_independent using simpa with Pa and val lemmas Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Simplify isTotalTimeDerivative_explicit: remove redundant helper lemmas, use fderiv_prodMk + congrArg for h_tq_der_val, use fderiv_const_add + fderiv_smul_const for h_qv_der - Restore field_simp chain in IsExtrema.lean isExtrema_iff_gauss_ampere with ring_nf instead of ring Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Lagrangian.lean: simplify freeCurrentPotential_hasVarGradientAt by removing redundant h3' and using simpa with mul_comm - Curl.lean: simplify curl_neg using curl_smul, simplify curl_sub by providing differentiability hypotheses explicitly Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify by using apply Differentiable.sub <;> fun_prop instead of explicit inner product differentiability proof. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify planeWave_time_deriv_time_deriv and planeWave_apply_space_deriv_space_deriv by extracting the iteratedDeriv identity into a have block. Simplify decompose_toChargeMap by combining simp and rw steps. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Shorten conv_lhs block by using direct rw with explicit arguments. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…ication Extract iteratedDeriv_two_eq_deriv_deriv as a lemma (used in 3 proofs) and simplify exists_curl_of_div_zero by removing duplicated helpers. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify second subgoal using congrFun and toChargeMap. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…e_T_beta, ofβ_differentiableOn, reduce_filter, reduce_reduce, mem_powerset_sum lemmas Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Replace repeat fun_prop with all_goals fun_prop. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Remove unnecessary rw [mul_pow] before field_simp - Use point-free style for h_map proof - Eliminate hF_deriv' using Eq.rec Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Eliminate unnecessary intermediate have statement Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Replace rw+rfl with direct rw using add/sub_apply - Fix deprecated ContinuousLinearMap.add_apply - Use _root_.add_apply for non-deprecated rewrite Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Use explicit hypotheses in div_add and div_smul rewrites - Eliminate all_goals fun_prop and fun_prop side goals Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Replace repeat rw with simpa using existing lemma Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Replace repeat fun_prop with all_goals fun_prop in kineticEnergy_deriv - Restructure potentialEnergy_deriv to use bullet instead of separate apply/exact - Combine fun_prop bullets in energy_deriv - Remove redundant show ... from rfl in gradient_inner_self - Replace repeat' fun_prop with all_goals fun_prop in Slice and TimeAndSpace Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Replace repeat fun_prop with all_goals fun_prop and restructure apply Differentiable.inner with <;> fun_prop. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Replace repeat' fun_prop with all_goals fun_prop in deriv_sum_inl/inr. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Combine two simp only lines into one. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…url proofs - Replace simp+module with simp in exp_decay_smul_velocity - Replace ext+simp+ring with module in trajectory_acceleration - Replace repeat'+all_goals with all_goals(first|...) in time_deriv_curl_commute Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Replace repeat+bullet with all_goals(first|...) in potentialEnergy_deriv Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…dsto proofs - Replace final congr/funext/simp/left/rw/ring blocks with integral_congr_ae + filter_upwards - Use Filter.Tendsto.zpow₀ instead of Filter.Tendsto.rpow for integer exponents - Use Filter.Tendsto.log with explicit norm_ne_zero_iff instead of separate simpa - Replace ring with ring_nf where ring fails - Simplify abs_of_nonneg proofs using normPowerSeries_nonneg directly Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…cian_distOfFunction_norm_zpow - Replace final simp/left/rw/norm_num with simp [..., hcoef] - Replace convert/ext/simp with simpa using lemma Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Replace convert/ext/simp with simpa using distOfFunction_smul_fun Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Simplify bound/limit proofs using mul_le_mul_of_nonneg_left and tendsto_const_nhds.mul - Replace convert/ext/simp patterns with simpa using - Remove unnecessary change blocks after distLaplacian rewrite - Replace ring with ring_nf where needed - Clean up unused simp arguments Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Vilin97
changed the title
- Replace trans/swap calc with structured calc in normPowerSeries_zpow_le_norm_sq_add_one - Use congrArg₂ for real-part equality in blockDiagonal_nonneg Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Extract duplicated hy_deriv definition - Simplify hyv0 proof using simpa - Simplify final step using inner_self_eq_zero directly Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify hy_deriv2 to function equality, compress energy block. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify the forward direction by using congr_fun and permT_eq_zero_iff. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Simplify by using gradient_const_mul_inner_self directly. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…ieldStrengthMatrix_sq proofs Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Vilin97
changed the title
Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…oofs - trajectory_velocity_eq_zero_iff_norm_eq_amplitude: simplify abs_cos path - equationOfMotion_iff_newtons_2nd_law: simplify conv_lhs block - kineticTerm_add_time_mul_const: restructure - Various minor improvements across files Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…_norm lemmas - trajectory_contDiff: revert to original (fun_prop approach) - trajectory_velocity_eq_zero_iff_norm_eq_amplitude: simplify abs_cos path - toInitialConditions_energy_at_t₀: combine simp steps - energy_conservation_of_equationOfMotion: simplify with simp Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- Simplify using Differentiable.rpow_const with fun_prop - Reduce from 12 to 3 lines Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…calEnsemble - HarmonicOscillator/Solution.lean: compress trajectory_energy proof - DampedHarmonicOscillator/Solution.lean: simplify overdamped case - Space/Norm/Basic.lean: compact IsDistBounded.normPowerSeries_log - CanonicalEnsemble/Basic.lean: shorten mathematicalPartitionFunction_congr and differentialEntropy_nonneg_of_prob_le_one proofs Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
Replace verbose congr/all_goals block with split_ifs <;> simp. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
- TotalDerivativeEquivalence.lean:357: simpa → simp - HarmonicOscillator/Solution.lean:555: simpa → simp - Wirtinger/Basic.lean:396: simpa → simp - EMPotential.lean:284: remove unused Lorentz.Vector.smul_add Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…cTerm proofs Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…ic field proofs Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…alence - Replace ENat.LEInfty.out with by decide in IsExtrema (ENat.LEInfty instance resolution) - Replace simp with explicit show in TotalDerivativeEquivalence for FunLike.coe expansion Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…raction, Space/Norm, and Units proofs - Restore working unfold/change/rw proofs for kineticEnergy_deriv, potentialEnergy_deriv, energy_deriv, and gradient_inner_self - Restore working proofs for trajectories_unique and return_time - Golf physHermite_orthogonal and physHermite_norm_cons with simp - Golf finset_eq_fstFieldOfContract_sndFieldOfContract using Finset.sort_insert with explicit proofs - Golf gradient_dist_normPowerSeries_log_tendsTo_distGrad_norm - Golf UnitChoices.dimScale_scaleUnit with field_simp Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
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.
Golfed proofs
This PR golfs proofs without changing statements or definitions, using more powerful tactics, increasing mathlib usage, and streamlining arguments.
Proofs golfed (134 commits)
Key areas: HarmonicOscillator (Basic, Solution), IsExtrema, TotalDerivativeEquivalence, KineticTerm, WickAlgebra/TimeOrder, WickContraction, Space/Norm, Units, PhysHermite, StatisticalMechanics, QFT/PerturbationTheory
Fixes in this commit
unfold/change/rwproofs forkineticEnergy_deriv,potentialEnergy_deriv,energy_deriv, andgradient_inner_selfin Basic.leantrajectories_uniqueandreturn_timein Solution.leanphysHermite_orthogonalandphysHermite_norm_conswithsimpin PhysHermite.leanfinset_eq_fstFieldOfContract_sndFieldOfContractusingFinset.sort_insertwith explicit proofs in WickContraction/Basic.leangradient_dist_normPowerSeries_log_tendsTo_distGrad_normin Space/Norm/Basic.leanUnitChoices.dimScale_scaleUnitwithfield_simpin Units/UnitDependent.leanTactics used
simp only,exact,refine,rw,simp,fun_propunfold/change/rwfor derivative computationsFinset.sort_insertwith explicith₁/h₂proofsfield_simpfor unit scalingNat.lt_or_gefor case analysisNotes
lake buildModel: Mistral Large (via Mistral Vibe CLI agent)
Duration: ~2 hours, ~30,000 tokens
Branch: claude/golf-proofs-more
PR: #1373