feat: Refactor downstream use away from FieldStrengthMatrix#1288

Open

NicolaBernini wants to merge 23 commits into

leanprover-community:masterfrom

NicolaBernini:feat/refactor-downstream-use-away-from-fieldStrengthMatrix-27June2026

Commits on Jun 26, 2026

feat: Refactor downstream use away from FieldStrengthMatrix
NicolaBernini
committed
style: Wrap electric field simp list

NicolaBernini
and
Claude Opus 4.8
committed
fix: Relate field strength components to basis coefficients

NicolaBernini
and
Claude Opus 4.8
committed
merge: Resolve master conflicts for field strength evaluation

NicolaBernini
and
Claude Opus 4.8
committed
fix: Open tensor notation in electric field

NicolaBernini
and
Claude Opus 4.8
committed

Commits on Jun 27, 2026

fix: Use field strength component API in electric field

NicolaBernini
and
Claude Opus 4.8
committed
fix: Define field strength component by basis coefficient

NicolaBernini
and
Claude Opus 4.8
committed
fix: Remove duplicate field strength simp lemmas

NicolaBernini
and
Claude Opus 4.8
committed

Commits on Jun 28, 2026

refactor: Use field strength evaluations directly

NicolaBernini
and
Claude Opus 4.8
committed
fix: Avoid compound indices in tensor notation

NicolaBernini
and
Claude Opus 4.8
committed
fix: Rewrite field strength matrix conversions explicitly

NicolaBernini
and
Claude Opus 4.8
committed

Commits on Jun 29, 2026

fix: Simplify electric field smoothness proofs

NicolaBernini
and
Claude Opus 4.8
committed
fix: Avoid timeout in electric field smoothness proofs

NicolaBernini
and
Claude Opus 4.8
committed
merge: Update PR 1288 with master

NicolaBernini
and
Claude Opus 4.8
committed
fix: Make magnetic field matrix cases explicit

NicolaBernini
and
Claude Opus 4.8
committed
fix: Avoid magnetic field simp loop

NicolaBernini
and
Claude Opus 4.8
committed

Commits on Jun 30, 2026

fix: Normalize magnetic field index cases

NicolaBernini
and
Claude Opus 4.8
committed
Add sliding pendulum configuration space

NicolaBernini
and
Claude Opus 4.8
committed
fix: Close kinetic term normalization

NicolaBernini
and
Claude Opus 4.8
committed
fix: Close kinetic term residual equality

NicolaBernini
and
Claude Opus 4.8
committed
fix: Rewrite diagonal field strength in kinetic term

NicolaBernini
and
Claude Opus 4.8
committed

Commits on Jul 1, 2026

fix: Rewrite diagonal field strength in Hamiltonian

NicolaBernini
and
Claude Opus 4.8
committed
fix: Address Hamiltonian diagonal branch

NicolaBernini
and
Claude Opus 4.8
committed