AlgebraicFramework: Jordan/JB/JBW hierarchy, Stinespring dilation, trace-class infrastructure - #3

Closed

TomOleDiem wants to merge 81 commits into

pr/algebraic-framework-pack

Commits on Aug 11, 2026

refactor(QED): name even anomaly-cancellation planes (#1507)
catlover-bot
authored
2310526
feat(QuantumMechanics/Hydrogen): prove angularMomentum_commutation_lrl (#1509)

TomOleDiem
and
claude
authored
cf1d86d

Commits on Aug 12, 2026

Add initial condensed matter directory structure (#1498)

WahajAyub
and
codex
authored
1d839cd
docs(quantum-info): add qubit API map (#1501)
Robby955
authored
f3da8ce
docs(QuantumMechanics): add Hilbert space tensor product API-map (#1512)
gloges
authored
c6e61dc

Commits on Aug 13, 2026

docs(cosmology): add FLRW API map (#1513)
Robby955
authored
0db6a7b

Commits on Aug 14, 2026

Commits on Aug 15, 2026

Commits on Aug 17, 2026

chore: Bump 4.33 (#1521)

NicolasRouquette
and
claude
authored
a50684a
Ladder Operators & Harmonic Oscillator (#1522)

authored
84507e3
Pauli matrices: vector identities and self-adjoint decomposition (#1524)

authored
6fb892c
Add PR size labeling workflow (#1527)
Alex-Zughaid
authored
fdebdbb

Commits on Aug 18, 2026

docs(units): add units and dimensions API map (#1516)

Robby955
and
claude
authored
19378fb
Stone theorem for norm-continuous unitary one-parameter groups (#1510)

authored
4e15f2b
Migrating NoAlphaImport Python Script to Lean (#1545)

FergusMunro
and
FergusMunro
authored
ef9a592

Commits on Aug 19, 2026

Commits on Aug 20, 2026

feat(Relativity): add evalT_evalT (#1546)

catlover-bot
and
codex
authored
9328f56
Add coordinate-axis boosts in SL(2, ℂ) (#1547)
nateabr
authored
6437336
feat(Relativity): add pointwise succSuccAbove commutation (#1548)

catlover-bot
and
codex
authored
823a7fe
feat(Units): add scaling API for ISQ unit types (#1551)

catlover-bot
and
codex
authored
49ee90e
docs(reference-frame): reference frame API map (#1553)
Robby955
authored
7194c0a
feat(OperatorAlgebra): start the operator algebra formalization (#1550)

TomOleDiem
and
claude
authored
e3e9d9b
docs(temperature): temperature API map (#1554)
Robby955
authored
de0e7cb

Commits on Aug 21, 2026

Migrating alpha file import to lean + adding testing (#1552)

FergusMunro
and
FergusMunro
authored
665cf2b

Commits on Aug 22, 2026

chore: remove 53 defeq set_option (#1557)
zhikaip
authored
8edacb9
feat(Mathematics): shared gradient lemmas, used by the oscillators (#1560)

aadarwal
and
claude
authored
846bc68
Fix tensor product documentation examples (#1562)
utkarshr3144
authored
7b6e0fe

Commits on Aug 23, 2026

Commits on Aug 24, 2026

Fix position operator documentation (#1563)
utkarshr3144
authored
1bf7760
fix(tensors): correct cyclic permutation elaboration (#1567)

Robby955
and
Claude Opus 4.8
authored
e3cc997
feat(ClassicalMechanics): the simple pendulum's dynamics, Lagrangian and equation of motion (#1564)
aadarwal
authored
485cb13
The Jordan product on observables (#1559)

TomOleDiem
and
Claude Opus 4.8
authored
4a4de62

Commits on Aug 25, 2026

The static theorem for reversible dynamics on Hilbert spaces (#1556)

TomOleDiem
and
Claude Opus 4.8
authored
8f9a40b
feat(Mathematics): Real.completeEllipticK, Legendre's complete elliptic integral of the first kind (#1573)

authored
6be0ec0
feat(ClassicalMechanics): simple pendulum conservation, equilibria and shift invariance (#1569)

authored
f6d7fe3

Commits on Aug 27, 2026

Commits on Aug 28, 2026

Commits on Aug 30, 2026

feat(ClassicalMechanics): the small-angle regime of the simple pendulum as a harmonic oscillator (#1572)
aadarwal
authored
e7e13e6
Add lattice QFT stub module (#1589)

Rahul-pamula
and
Claude Opus 4.8
authored
686d93d

Commits on Aug 31, 2026

Update README with library sections and descriptions (#1596)
jstoobysmith
authored
12e16cf

Commits on Sep 1, 2026

Commits on Sep 2, 2026

refactor(ClassicalMechanics): switch to derivVec for simple-pendulum velocity (#1604)
zhikaip
authored
e209ba1
refactor(ClassicalMechanics): rigid-body velocities and momentum valued in the displacement space (#1603)
zhikaip
authored
4b8202e
feat(OperatorAlgebra): reorganize states, observables, and measurement (#1608)

TomOleDiem
and
claude
authored
119fd70
EVJJI theorem twoState_entropy_eq (#1605)

oe-parks
and
Claude Opus 5
authored
170a753
fix(OperatorAlgebra): rebase PR #1607 onto master post-#1608 merge (#1607)

TomOleDiem
and
claude
authored
a4ba9ef

Commits on Sep 3, 2026

feat(Units): component lemmas for the Exponent power of a dimension (#1600)

NicolasRouquette
and
claude
authored
60b4473
fix(Tensors): rank the tensor action above the Tensorial action (#1611)

zhikaip
and
claude
authored
bbb33d2
feat: review claims via comments (#1601)

Alex-Zughaid
and
claude
authored
c9ae1ba
feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum (#1610)

zhikaip
and
claude
authored
c17844a

Commits on Sep 5, 2026

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

zhikaip
and
claude
authored
6a09b2d

Commits on Sep 7, 2026

Commits on Sep 8, 2026

Commits on Sep 9, 2026

Improve how references are used throughout Physlib (#1613)

authored
715f2ac
feat(PhyslibAlpha): the Norton dome (#1619)

zhikaip
and
claude
authored
142f41c
Replace OperatorAlgebra with AlgebraicFramework

TomOleDiem
and
claude
committed
79b62ac
Fix CI lint failures: unusedArguments and spelling

TomOleDiem
and
claude
committed
4ac9011
docs(OrderUnit): standardize module documentation layout across the folder

TomOleDiem
and
claude
committed
6aa6e75

Commits on Sep 13, 2026