refactor: golf Physlib proofs — proof-body only, no new declarations (~−4,390 lines, 109 files)#1263
Merged
jstoobysmith merged 129 commits intoJun 29, 2026
Merged
Conversation
Add `conj_row_dotProduct_row`, the entrywise orthonormality of the rows of a CKM (unitary) matrix (`∑ₖ conj (Vᵢₖ) * Vⱼₖ = δᵢⱼ`), and use it to replace the nine near-identical ~8-line proofs of `uRow_normalized`, `cRow_normalized`, `tRow_normalized`, `uRow_cRow_orthog`, `uRow_tRow_orthog`, `cRow_uRow_orthog`, `cRow_tRow_orthog`, `tRow_uRow_orthog`, `tRow_cRow_orthog` with one-line specializations. Statements are unchanged; net -54 lines. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Replace the three-way `fin_cases i` case split closing with `exact h0/h1/h2` by `fin_cases i <;> assumption`. Statement unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
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 |
Add `phaseShiftApply_apply`, the general `(i, j)` entry of a phase-shifted CKM matrix, and use it to replace the nine near-identical ~11-line component proofs `ud`, `us`, `ub`, `cd`, `cs`, `cb`, `td`, `ts`, `tb` with two-line proofs. Statements are unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
…lemma Add `cexp_phase_mul_eq_norm` (`cexp ((p + q) I) * z = ‖z‖` when `p + q = -arg z`) and use it, together with the `phaseShiftApply.*` entry lemmas, to replace the six near-identical ~12-line proofs `shift_ud_phase_zero`, `shift_us_phase_zero`, `shift_ub_phase_zero`, `shift_cs_phase_zero`, `shift_cb_phase_zero`, `shift_tb_phase_zero` with two-line proofs. Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Add `npow_proj` (an additive, `1`-vanishing dimension exponent respects powers) and use it to replace the five identical inductions `npow_length`, `npow_time`, `npow_mass`, `npow_charge`, `npow_temperature` with one-line proofs. Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Add `div_proj` (an additive, inverse-negating dimension exponent respects division) and use it to replace the five identical proofs `div_length`, `div_time`, `div_mass`, `div_charge`, `div_temperature` with one-line proofs. Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Add `tensorBasis_toMatrix_symm_expand`, the expansion of the inverse of the canonical `tensorProduct`-basis-to-matrix equivalence, and use it to replace the ten near-identical proofs `leftLeftToMatrix_symm_expand_tmul`, ..., `leftRightToMatrix_symm_expand_tmul` with one-line specializations (each is definitionally an instance of the helper). Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Add `sum_filter_neg_lt` (a multiset of integers with a negative element has a negative-part sum < 0) and use it, together with Mathlib's `Multiset.single_le_sum` and the `numChiral*_eq_sum_sub_numAntiChiral*` lemmas, to golf the fifteen `chiralIndicesOf*_noneg/_sum_eq_three/_le_three_of_noExotics` proofs (each from ~12-28 lines to ~3). Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
…red lemma Add `tensorBasis_toMatrix_symm_expand` (complex) and `tensorBasis_toMatrixRe_symm_expand` (real) — the expansion of the inverse of the canonical tensorProduct-basis-to-matrix equivalence — and use them to replace the four `*ToMatrix_symm_expand_tmul` proofs in `ComplexTensor/Matrix/Pre.lean` and the four `*ToMatrixRe_symm_expand_tmul` proofs in `RealTensor/Matrix/Pre.lean` with one-line specializations. Statements unchanged. (Same shape as the helper already added in `ComplexTensor/Weyl/Two.lean`; could be hoisted to a shared file in a follow-up.) Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Add `submultiset_sum_le_three` (a sub-multiset of nonnegative integers summing to 3 has sum ≤ 3) and use it with `Multiset.map_le_map` and the existing noneg/sum-of-three lemmas to replace the five `chiralIndicesOf*_subset_sum_le_three_of_noExotics` proofs with term-mode one-liners. Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Replace the eight explicit `match`-on-`ChargeSpectrum` proofs (`ofPotentialTerm'_μ_finset`, `_β_finset`, `_W2_finset`, `_W3_finset`, `_W4_finset`, `_K2_finset`, `_topYukawa_finset`, `_bottomYukawa_finset`) with a single `rcases x with ⟨_ | qHd, _ | qHu, Q5, Q10⟩ <;> simp [ofPotentialTerm']`. Statements unchanged. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PA9j1z8zhVsdFWKQPf2tRZ
Collapse the five near-identical numChiral{D,L,Q,U,E}_eq_sum_sub_numAntiChiral
proofs into one private helper `sum_filter_nonneg_eq_sum_sub` on `Multiset ℤ`
(sum of nonnegative part = total sum − sum of negative part), with each lemma a
one-line application.
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace the three identical 8-line constructor proofs of
isDimensionallyCorrect_fun_{iff,left,right} with `simp only
[IsDimensionallyCorrect, funext_iff]; rfl`, since each iff is just the
function-extensionality unfolding of `IsDimensionallyCorrect`.
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Replace the repeated ~6-line `simp only [...]` numeral/Fin normalization list in each of the seven Bᵢ_cubic lemmas with a short `simp [Bᵢ, ...]` that lets the default simp set handle the arithmetic, keeping only the structural reduction lemmas. Behaviour and the `backward.isDefEq.respectTransparency` guards are preserved. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Extract a private helper `γ_sq_mul_det` for the Lorentz-factor identity `(γβ)² − (γβ)²β² = 1` and use `linear_combination` to replace duplicated `ring_nf`/`field_simp` blocks in `boost`; collapse the eight `boost_zero_*` lemmas to one-line term proofs; simplify `boost_inverse` and `boost_transpose_eq_self` dispatch. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Extract the duplicated 23-line "a time-fixing Lorentz transform is block-diagonal" argument into a private helper `fromBlocks_spatial_eq`, used in both the `invFun` and `right_inv` fields of `ofSpecialOrthogonal`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Collapse the `apply X.inner; · fun_prop; · fun_prop` proofs of inner_apply_differentiableAt/differentiable, inner_contDiff and inner_apply_contDiff to `apply X.inner <;> fun_prop`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…pers Extract private helpers `schwartzCompSmulSphere` (+ `_apply`), `normPowerSeries_rpow_tendsto`, `ae_of_forall_ne_zero`, and `distOfFunction_const_mul_zpow_smul_repr_eq` to remove duplicated Schwartz-map constructions, `rpow` limit blocks, a.e.-on-complement-of-zero arguments, and scalar-pull-out steps across the radial-power lemmas. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Extract a private helper `integrable_smul_proj_of_radial_power`, parametrised by a projection, to share the "reduce to radial-power integrability" block between `integrable_space` and `integrable_time_space`, and tidy the tail rewrites in `integrable_mul_inv_pow`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…fun_prop` Mechanical golf of six two-goal `fun_prop` dispatches across WaveEquation.Basic, FDerivCurry, HarmonicOscillator.Eigenfunction, Time.Derivatives and CanonicalEnsemble.Basic. Each module still builds. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Extract a private helper `norm_sum_pow_div_factorial_le_exp_norm` (partial exponential sums are bounded by `exp ‖z‖`) and use it to shorten the bound, norm-of-exp and positivity steps in `orthogonal_exp_of_mem_orthogonal`; deduplicate the integrability fact in `zero_of_orthogonal_mk`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
In superCommute_crPart_crPart and superCommute_anPart_anPart, replace the eight
`apply superCommute_{create,annihilate}_…; · rfl; · rfl` blocks with
`apply … <;> rfl`.
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
In CrAnSection and Space.EuclideanGroup.Basic, replace `<construct>; · simp; · simp` with `<construct> <;> simp`. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Add `eventuallyEq_of_eq_on_cthickening` (packaging the repeated thickening/interior locality argument) and a private `postcomp` (localization is preserved by pointwise post-composition). Rewrite div/div_comp_repr/grad/ gradient/deriv/fderiv/adjFDeriv to use the former and mul_left/mul_right/ smul_left/fst/snd to delegate to the latter. No statements changed. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Reuse `eventuallyEq_of_eq_on_cthickening` in `adjFDeriv_apply`, hoist repeated IsTestFunction sub-proofs into local `have`s, deduplicate the twice-invoked `exists_sSup_image_eq_and_ge` in `unique`, make `smul_right` delegate to the byte-identical `smul_left`, and collapse the test-function-preserving helpers to term mode. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Shorten `fundamental_theorem_of_variational_calculus'`: replace the manual Cauchy–Schwarz calc with `neg_le_of_abs_le`/`nlinarith`, inline the `ContDiffBump` construction, and collapse the continuity/positivity/support `have`s to term mode. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Collapse the four near-identical group-action proofs (contrContrToMatrix_ρ, coCoToMatrix_ρ, contrCoToMatrix_ρ, coContrToMatrix_ρ) into one private helper `tensorBasis_toMatrix_map` plus short specializations. The helper works at scalar level (pointwise on matrix entries) to sidestep the Matrix/Pi instance mismatch. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Collapse the four near-identical group-action proofs into one private helper `tensorBasis_toMatrixRe_map` plus short specializations, mirroring the complex case. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Streamline the cross-product proof. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Streamline the gauge-action proof. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…ination (−23) Replace the by_cases case analysis with a single linear_combination certificate. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…agneticField (−20) Streamline the gradient-Lagrangian proof. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…er (−19) Add private iteratedDerivList_differentiable; streamline the contDiff/commute proofs. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…helpers (−13) Add private allowsTerm_topYukawa_of_form/allowsTerm_bottomYukawa_of_form helpers. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…adient (−9) Streamline the Euler-Lagrange proof. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Vilin97
changed the title
# Conflicts: # Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean # Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean # Physlib/CondensedMatter/TightBindingChain/Basic.lean # Physlib/Relativity/Tensors/RealTensor/ToComplex.lean # Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean # Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean
…nly edits Per request: eliminate every new top-level declaration introduced by the golfing pass so the PR only modifies proof bodies of existing (master) statements. Each removed helper was either inlined as a proof-local `have`/`let` at its use site (keeping the golf) or, where it was genuine cross-proof de-duplication, the affected proofs were reverted to master's original bodies. - 86 added declarations across 46 files removed; every modified file now has a declaration set byte-identical to origin/master (verified: no added/removed names, no signature/binder/attribute changes). - HasVarAdjoint: inlined the cross-file `eventuallyEq_of_eq_on_cthickening` locality helper (was reused from IsLocalizedfunctionTransform). - Style/lint fixes for CI: wrapped 10 over-length lines and replaced 2 non-terminal `simp`s with their `simp only` expansions. Full `lake build` passes (4322 jobs); style linter, sorry_lint, check_dup_tags, check_file_imports, and runPhyslibLinters all clean. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
# Conflicts: # Physlib/Relativity/Tensors/Constructors.lean # Physlib/Relativity/Tensors/Contraction/Basic.lean # Physlib/Relativity/Tensors/Dual.lean # Physlib/Relativity/Tensors/Product.lean
Vilin97
changed the title
| mul_one, Nat.ofNat_pos, Nat.add_div_right, Nat.add_mod_right, Nat.reduceMod, Nat.mod_succ, | ||
| Fin.sum_univ_three, Nat.zero_div, Fin.zero_eta, zero_mul, zero_add, Fin.mk_one, Fin.reduceFinMk, | ||
| Nat.reduceDiv, one_mul, Nat.reduceAdd, neg_mul, mul_neg] | ||
| simp [B₂, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat, |
Member
There was a problem hiding this comment.
These changes I'm not so comfortable with. Should really be simp only ...
| head_val'] | ||
| change _ + _ * _ * 0 = _ | ||
| rw [exp_add] | ||
| simp [phaseShiftApply_coe, mul_apply, Fin.sum_univ_three] |
| by_contra hl | ||
| rw [not_le] at hl | ||
| obtain ⟨c, hc⟩ := h | ||
| have key : ∀ v : ℝ, ((0 < P.μ2 ∧ v ≤ 0) ∨ |
Member
There was a problem hiding this comment.
There are lots of have key ... would be nice if they had more descriptive names
| aesop | ||
|
|
||
| /-- The defining identity of the Lorentz factor: `(γ β)² (1 - β²) = 1` when `|β| < 1`. -/ | ||
| private lemma γ_sq_mul_det {β : ℝ} (hβ : |β| < 1) : (γ β) ^ 2 - (γ β) ^ 2 * β ^ 2 = 1 := by |
Resolve conflict in Physlib/Mathematics/InnerProductSpace/Basic.lean (isBoundedBilinearMap_inner'.bound) by taking the upstream proof, which our golf had left essentially unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- DimSevenPlane (B₀_cubic..B₆_cubic) and CKMMatrix.Basic (ud..tb):
restore the explicit `simp only [...]` proofs instead of bare `simp`,
as requested ("should really be simp only"). These files now match
upstream exactly.
- LorentzGroup/Boosts/Basic: remove the added `private lemma
γ_sq_mul_det` (flagged "Added lemma" — the PR adds no new declarations)
and inline it as a single local `have hγ` shared by both use sites in
the `boost` membership proof.
- Rename all 29 golf-introduced generic `have key : ...` hypotheses
across 14 files to descriptive names reflecting their statements
(e.g. `c_le_of_attainable`, `attainable_nonneg`, `fderiv_comp_val_eq_deriv`,
`sum_add_compl_eq_three`).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
Author
|
@jstoobysmith , addressed comments, can you allow the CI to run please? |
Collaborator
The descriptive names that replaced `have key` pushed 8 lines past the 100-column limit, failing the "Python based style linter" CI job (DampedHarmonicOscillator/Solution ×4, PhysHermite, VariationalCalculus, RadialAngularMeasure). Wrap them; no semantic change. `lint-style.py` now exits 0 and the four modules still build. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Contributor
Author
|
I think it should pass now |
jstoobysmith
approved these changes
Jun 29, 2026
jstoobysmith
left a comment
jstoobysmith
left a comment
Member
There was a problem hiding this comment.
These changes now look good. Many thanks - I have approved.
jstoobysmith
added
ready-to-merge
Member
|
@Vilin97 Would you mind fixing the merge conflicts, and then this looks ready to go! Many thanks. |
Resolve conflicts in Physlib/SpaceAndTime/Space/Norm/{Basic,IteratedLaplacian}.lean
by taking the upstream versions: upstream refactored the `distLaplacian_*`
helper API (renamed `distLaplacian_fundamentalSolution_norm_zpow_of_three_le`
-> `...norm_zpow`, changed the `distLaplacian_distOfFunction_norm_zpow`
signature `d := 2*m` -> `2*m+1`), so our golf's old call signatures are stale.
These helpers are used only in these two files.
Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
Contributor
Author
|
done |
Member
|
Merged :). |
Contributor
Author
🏌️ check-golf reportComparing base Result: ✅ Statements preserved. Every changed declaration kept its statement; only proofs / bodies changed.
Of the golfed proofs/bodies above, the trivial reshapes were:
🔧 Definition bodies changed (data may have changed, type unchanged) (8)The defining term outside
✅ Proofs golfed (553)
✅ Definition proofs golfed (data unchanged) (15)
↩️ Only a newline removed (tokens unchanged) (1)
➡️ Tactics joined by `;` (6)
Generated by |
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
3 participants
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
A golfing pass over Physlib proofs: making proofs genuinely shorter and simpler by
streamlining arguments, increasing Mathlib usage, using more powerful tactics, and removing
redundant steps — modifying only the proof bodies of existing statements.
No new declarations are introduced. Every statement (name, signature, binders, attributes)
is byte-identical to
master; the diff touches proof bodies only. Where an earlier draft hadextracted shared helper lemmas, those have been folded back in — either inlined as proof-local
have/letterms or by streamlining each site directly — so the PR adds nothing to the public(or private) API surface.
Net ≈ −4,390 lines across 109 files. The full project builds (
lake build), and the stylelinter,
sorry_lint,check_dup_tags,check_file_imports, andrunPhyslibLintersare allclean.
Approach
simp,fun_prop,gcongr,positivity,field_simp,linarith/nlinarith,linear_combination,omega,grind).have/rw/classical/differentiability scaffolding; prefer term mode whereit is shorter.
Fin.succAbove_*,HasDerivAt.fun_sum, change-of-variables for integrability).Notable proof golfs (statements unchanged)
CanonicalEnsemble/Lemmas,CanonicalEnsemble/Finite,Temperature/Basic(thermodynamic-relation and derivative proofs).TimeAndSpace/Basic,Space/ConstantSliceDist,Space/Norm/Basic,Space/Integrals/RadialAngularMeasure,Space/Derivatives/*(Schwartz/integrability anditerated-derivative bookkeeping).
RealTensor/Metrics/Pre,RealTensor/Metrics/Basic,RealTensor/Vector/Tensorial,LorentzGroup/Boosts/Generalized,LorentzGroup/Orthochronous,SL2C/Basic,Causality/LightLike.DampedHarmonicOscillator/Solution,HamiltonsEquations,HarmonicOscillator/TISE.Fin(routesuccAbove_succAbove_predAboveIthrough Mathlib),VariationalCalculus/HasVarAdjDeriv,List,List/InsertionSort,SpecialFunctions/PhysHermite,DataStructures/FourTree/*.CKMMatrix/*,Quanta/{FiveQuanta,TenQuanta},ChargeSpectrum/*,Fluxes/{Basic,NoExotics/ChiralIndices}.Kinematics/{ElectricField,MagneticField,FieldStrength,GaugeTransformation},Vacuum/{HarmonicWave,IsPlaneWave},Dynamics/*,Distributional/*.QED/AnomalyCancellation/LineInPlaneCond,TwoHDM/GramMatrix,IdealGas/Basic,Units/{Dimension,Examples},NavierStokes/Momentum, plus localized streamlining elsewhere.Statements are byte-identical to
master; no new declarations, and nosorry/axiom/native_decideintroduced.