feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum by zhikaip · Pull Request #1610 · leanprover-community/physlib

zhikaip · 2026-09-02T21:46:32Z

Lorentz.Vector d and Lorentz.CoVector d are defs for Fin 1 ⊕ Fin d → ℝ and are applied directly as functions throughout the library (v μ, x (Sum.inl 0), …). Lean 4.33 enables backward.isDefEq.respectTransparency.types by default, under which such applications are not type-correct at implicit transparency (the note "function expected v μ" in error messages). Once a goal contains one under a binder, rw and simp can fail to match patterns that are visibly present. The release notes recommend marking the definitions involved @[implicit_reducible]; this PR does that for both types.

Lorentz.Vector.inner_eq_sum is added to simplify proofs previously going through equivEuclid, WithLp and PiLp.

as a result, all set_option backward.isDefEq.respectTransparency false and occurences of erw in these files can be removed

PR drafted by claude and finalised by myself

…eq_sum `Lorentz.Vector` and `Lorentz.CoVector` are plain `def`s applied directly as functions throughout the library. Under Lean 4.33's `backward.isDefEq.respectTransparency.types` such applications are not type-correct at implicit transparency, which stops `rw`/`simp` matching patterns containing them. Marking both `@[implicit_reducible]` is the fix recommended by the release notes. Adds `inner_eq_sum` for both types; `basis_inner`/`inner_basis` are reproved from it, and the `erw`s in `basis_apply`/`basis_repr_apply` become plain `rw`. In total 21 `respectTransparency` options become unnecessary (2 in Vector/Basic, 19 in the Vector/CoVector tensorial, representation and contraction files) and are removed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The `-Fintype.sum_sum_type` exclusions in `inner_eq_sum`, `basis_inner` and `inner_basis` were unnecessary. `CoVector.equivEuclid_apply` mirrors the existing `Vector.equivEuclid_apply` simp lemma, which removes the manual `rfl` from `CoVector.inner_eq_sum`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

The Euclidean inner product on `CoVector` has no consumers in the library, so these lemmas were speculative API. `CoVector` keeps only the `implicit_reducible` attribute, the `erw` removals and the docstring fix. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

github-actions · 2026-09-02T21:47:03Z

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).
A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.
The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

jstoobysmith · 2026-09-03T09:58:48Z

+  implicit-reducible lets such applications typecheck at implicit transparency, so that
+  `rw` and `simp` can match patterns containing them (see the Lean 4.33 release notes on
+  `backward.isDefEq.respectTransparency.types`). -/
+attribute [implicit_reducible] Vector


Would it not be better to do

@[implicit_reducible] def Vector ....

fixed, wondering if it's a good idea to keep the explanation in or remove them

Think it would be nice to keep it somewhere

zhikaip · 2026-09-03T17:50:41Z

-awaiting-author

jstoobysmith

Approved

All nine `set_option backward.isDefEq.respectTransparency false in` lines in `EMPotential.lean` are no longer needed after `Lorentz.Vector` was marked `implicit_reducible` (#1610); the file compiles without them. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

…netic potential (#1616) * feat(Electromagnetism): differentiability of the derivative of the electromagnetic potential Resolves the TODO in `EMPotential.lean` asking for results on the differentiability of the derivative of the electromagnetic potential. In `Physlib/Electromagnetism/Kinematics/EMPotential.lean`: - `contDiff_deriv_of_smooth`: `∂_ μ A x ν` is `C^n` for a smooth potential. - `contDiff_deriv_deriv`, `differentiable_deriv_deriv`, `differentiable_deriv_deriv_of_smooth`: the second derivatives `∂_ μ (∂_ ν A) x ρ` are `C^n` for a `C^{n+2}` potential, and differentiable for a `C^3` (or smooth) potential. - `deriv_differentiable`, `deriv_differentiable_of_smooth`, `deriv_contDiff`: the derivative tensor `A.deriv` is differentiable for a `C^2` potential and `C^n` for a `C^{n+1}` potential. - Fix the table of contents (the constructor-differentiability section was missing and two sections shared the number A.5). In `Physlib/Electromagnetism/Kinematics/FieldStrength.lean`: - Golf `fieldStrengthMatrix_differentiable` and `fieldStrengthMatrix_contDiff` to use `differentiable_deriv`/`contDiff_deriv` via `fun_prop` instead of re-deriving them inline. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> * refactor(EMPotential): rename derivative differentiability lemmas by object Lemmas about the derivative tensor `A.deriv` now carry the plain names `differentiable_deriv`, `differentiable_deriv_of_smooth`, `contDiff_deriv` (matching `differentiable_toFieldStrength`), while lemmas about a component `∂_ μ A x ν` carry a `_component` suffix (matching `differentiable_component`): - `differentiable_deriv` → `differentiable_deriv_component` - `differentiable_deriv_of_smooth` → `differentiable_deriv_component_of_smooth` - `contDiff_deriv` → `contDiff_deriv_component` - `contDiff_deriv_of_smooth` → `contDiff_deriv_component_of_smooth` - `contDiff_deriv_deriv` → `contDiff_deriv_deriv_component` - `differentiable_deriv_deriv` → `differentiable_deriv_deriv_component` - `differentiable_deriv_deriv_of_smooth` → `differentiable_deriv_deriv_component_of_smooth` - `deriv_differentiable` → `differentiable_deriv` - `deriv_differentiable_of_smooth` → `differentiable_deriv_of_smooth` - `deriv_contDiff` → `contDiff_deriv` No file outside `EMPotential.lean` referred to the old names. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> * feat(EMPotential): differentiability of the components of `∂_ μ (∂_ ν A)` Add the second statement shape for second derivatives of the potential, where the vector-valued derivative is formed first and the component taken afterwards: - `contDiff_deriv_deriv_apply` : `∂_ μ (∂_ ν A) x ρ` is `C^n` for a `C^{n+2}` potential. - `differentiable_deriv_deriv_apply` : differentiable for a `C^3` potential. - `differentiable_deriv_deriv_apply_of_smooth` : differentiable for a smooth potential. Proofs reduce to the `_component` lemmas via `SpaceTime.deriv_apply_eq`. The section docstring explains the `_component` / `_apply` distinction, and an over-long "Key results" line is re-wrapped. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> * chore(EMPotential): remove stale `respectTransparency` options All nine `set_option backward.isDefEq.respectTransparency false in` lines in `EMPotential.lean` are no longer needed after `Lorentz.Vector` was marked `implicit_reducible` (#1610); the file compiles without them. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> * refactor(EMPotential): drop derivative lemmas that `fun_prop` proves directly Remove the lemmas whose statements a bare `fun_prop` already proves from `SpaceTime.differentiable_deriv`/`SpaceTime.contDiff_deriv` and the `Lorentz.Vector` component lemmas, so they added nothing to the search: - `differentiable_deriv_component`, `contDiff_deriv_component` - `differentiable_deriv_deriv_component`, `differentiable_deriv_deriv_component_of_smooth` - `differentiable_deriv_deriv_apply` Kept are the lemmas `fun_prop` cannot derive on its own: the `_of_smooth` variants (`fun_prop` does not lower `ContDiff ℝ ∞`), the `C^{n+2}` second derivative lemmas (symbolic `n + 2` does not unify with `?m + 1`), and the derivative-tensor lemmas (need `unfold deriv`). Their proofs now obtain the needed finite-order hypothesis with `have` and finish by `fun_prop`. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> * refactor(EMPotential): drop `differentiable_component`, provable by `fun_prop` `Differentiable ℝ (fun x => A x μ)` for a differentiable potential is found by `fun_prop` directly, so the lemma is removed; its single by-name use in `ElectricField.lean` becomes `fun_prop`. Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

zhikaip and others added 3 commits September 2, 2026 15:40

github-actions Bot added the small label Sep 2, 2026

github-actions Bot added the t-relativity Relativity label Sep 2, 2026

jstoobysmith reviewed Sep 3, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 3, 2026

change implicit_reducible tag

2ea8f84

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Sep 3, 2026

jstoobysmith approved these changes Sep 3, 2026

View reviewed changes

zhikaip merged commit c17844a into master Sep 3, 2026
17 checks passed

zhikaip deleted the vector_implicit_reducible branch September 3, 2026 19:20

This was referenced Sep 3, 2026

refactor(Electromagnetism): replace fieldStrengthMatrix with index-evaluation components #1614

Merged

refactor(FieldStrength): remove basis-representation lemmas #1615

Merged

Navigation Menu

Uh oh!

feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum - #1610

feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum#1610
zhikaip merged 4 commits into
masterfrom
vector_implicit_reducible

zhikaip commented Sep 2, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 2, 2026

Uh oh!

jstoobysmith Sep 3, 2026

Uh oh!

zhikaip Sep 3, 2026

Uh oh!

jstoobysmith Sep 3, 2026

Uh oh!

zhikaip commented Sep 3, 2026

Uh oh!

jstoobysmith left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

zhikaip commented Sep 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Sep 2, 2026

Uh oh!

jstoobysmith Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

zhikaip Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

zhikaip commented Sep 3, 2026

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

zhikaip commented Sep 2, 2026 •

edited

Loading