Rename and split QED anomaly cancellation plane definitions for clarity#1047

Draft

Copilot wants to merge 22 commits into

masterfrom

copilot/improve-variable-naming-basis-linear

Commits on Apr 20, 2026

Initial plan
Copilot
authored
Extract charge splitting definitions to ChargeSplits.lean

Copilot
and
jstoobysmith
authored
Extract symmetric plane (Section B) into SymmPlane.lean

Copilot
and
jstoobysmith
authored
Extract shifted plane (Section C) into ShiftPlane.lean

Copilot
and
jstoobysmith
authored
Extract charge splitting definitions into ChargeSplits.lean

Copilot
and
jstoobysmith
authored
Extract symmetric plane (Section B) into SymmPlane.lean

Copilot
and
jstoobysmith
authored
Extract shifted plane section into ShiftPlane.lean with renamed identifiers

Copilot
and
jstoobysmith
authored
Refactor Odd/BasisLinear.lean: extract sections A-C, rename to Psymm/Pshift

Copilot
and
jstoobysmith
authored
Rewrite Even/BasisLinear.lean: extract sections A-C to submodules, rename identifiers

Copilot
and
jstoobysmith
authored
Rename plane definitions and split BasisLinear files for QED anomaly cancellation

Copilot
and
jstoobysmith
authored
Add SymmPlane.lean: symmetric plane for even anomaly cancellation

Copilot
and
jstoobysmith
authored
feat: extract shifted plane for even case into ShiftPlane.lean

Copilot
and
jstoobysmith
authored
Rewrite SymmPlane.lean: include symmetric split defs and use correct imports

Copilot
and
jstoobysmith
authored
refactor: rewrite ShiftPlane.lean with correct naming and complete content

Copilot
and
jstoobysmith
authored
refactor(Even/BasisLinear): keep only sections E and F with renamed identifiers

Copilot
and
jstoobysmith
authored
refactor: Odd/BasisLinear.lean to only contain sections E and F with renamed identifiers

Copilot
and
jstoobysmith
authored
Address review: rename Psymm→symmPlane, Pshift→shiftPlane, remove ChargeSplits, move charge splits into plane files, move mixed cubic ACC into ShiftPlane

Copilot
and
jstoobysmith
authored

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rename and split QED anomaly cancellation plane definitions for clarity#1047

Rename and split QED anomaly cancellation plane definitions for clarity#1047
Copilot wants to merge 22 commits into
masterfrom
copilot/improve-variable-naming-basis-linear

Commits on Apr 20, 2026

Initial plan

Extract charge splitting definitions to ChargeSplits.lean

Extract symmetric plane (Section B) into SymmPlane.lean

Extract shifted plane (Section C) into ShiftPlane.lean

Extract charge splitting definitions into ChargeSplits.lean

Extract symmetric plane (Section B) into SymmPlane.lean

Extract shifted plane section into ShiftPlane.lean with renamed identifiers

Refactor Odd/BasisLinear.lean: extract sections A-C, rename to Psymm/Pshift

Rewrite Even/BasisLinear.lean: extract sections A-C to submodules, rename identifiers

Rename plane definitions and split BasisLinear files for QED anomaly cancellation

Add SymmPlane.lean: symmetric plane for even anomaly cancellation

feat: extract shifted plane for even case into ShiftPlane.lean

Rewrite SymmPlane.lean: include symmetric split defs and use correct imports

refactor: rewrite ShiftPlane.lean with correct naming and complete content

refactor(Even/BasisLinear): keep only sections E and F with renamed identifiers

refactor: Odd/BasisLinear.lean to only contain sections E and F with renamed identifiers

Address review: rename Psymm→symmPlane, Pshift→shiftPlane, remove ChargeSplits, move charge splits into plane files, move mixed cubic ACC into ShiftPlane

Commits on Apr 21, 2026

refactor(Even/BasisLinear): rename identifiers for clarity

refactor(Odd): comprehensive rename of QED anomaly cancellation Odd case

Fix remaining doc comment with old P/P! names in Even/Parameterization.lean

Refactor QED anomaly cancellation: rename dirs, sections, and identifiers

Fix typos: Spltting → Splitting in Planes/ files