Rename and split QED anomaly cancellation plane definitions for clarity by Copilot · Pull Request #1047 · leanprover-community/physlib

Copilot · 2026-04-20T13:33:18Z

The two planes in Odd/BasisLinear and Even/BasisLinear used non-descriptive naming (basis/P/P' vs basis!/P!/P!') with no indication of what distinguishes them. The ! suffix convention was particularly opaque.

Naming

Renamed definitions after the charge-index splitting each plane is built from:

Symmetric plane (symmBasisAsCharges/symmPlane/symmPlaneLinSols): basis vectors pair charges at positions from the symmetric split ((n+1) + n odd, n.succ + n.succ even)
Shifted plane (shiftBasisAsCharges/shiftPlane/shiftPlaneLinSols): basis vectors pair charges at positions from the shifted split (1 + n + n odd, 1 + (n + n + 1) even)

-- Before
def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i
def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basis!AsCharges i

-- After
def symmPlane (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • symmBasisAsCharges i
def shiftPlane (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • shiftBasisAsCharges i

File splitting

Each monolithic BasisLinear.lean (~1000 lines) is split into sub-modules:

BasisLinear/SymmPlane.lean — symmetric charge splits, symmetric plane basis, inclusion, ACC proofs
BasisLinear/ShiftPlane.lean — shifted charge splits, shifted plane basis, inclusion, ACC proofs, mixed cubic ACCs
BasisLinear.lean — combined basis, span theorem (imports above)

Charge index splitting definitions are co-located with their corresponding plane (no separate ChargeSplits file). Mixed cubic ACC results live in ShiftPlane.lean which imports SymmPlane.lean and has access to both planes' definitions.

Documentation

Module docs now explain the naming motivation — each plane is named after which charge-index splitting its basis vectors are built from.

Status

⚠️ Partial: Core renames and file splits are complete for both Odd and Even cases. Mechanical renaming in Odd/Parameterization.lean and Even/Parameterization.lean proof bodies is incomplete, and Physlib.lean imports need updating.

Extract Section A (charge splitting definitions) from Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean into a new file Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear/ChargeSplits.lean. The new file contains all definitions and lemmas from the theDeltas section: oddFst, oddSnd, oddMid, oddShiftFst, oddShiftSnd, oddShiftZero, oddShiftShiftZero, oddShiftShiftFst, oddShiftShiftMid, oddShiftShiftSnd, and all lemmas relating the splittings together. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Extract Section B (the first/symmetric plane) from Odd/BasisLinear.lean into a new file at Odd/BasisLinear/SymmPlane.lean, renaming all identifiers with symm- prefixes (e.g. basisAsCharges → symmBasisAsCharges, P → Psymm, basis → symmBasis, etc.) and updating all internal references accordingly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Extract the shifted plane content (lines 494-747) from BasisLinear.lean into a new file BasisLinear/ShiftPlane.lean, following the same pattern as SymmPlane.lean. All names are updated: - basis! → shiftBasis - P! → Pshift Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Extract Section A (charge splitting definitions) from Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean into a new file Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear/ChargeSplits.lean. This includes: - A.1: evenFst, evenSnd, ext_even, sum_even - A.2: n_cond₂, evenShiftFst, evenShiftSnd, evenShiftZero, evenShiftLast, sum_evenShift - A.3: All relating lemmas between the two splittings Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Extract Section B (lines 221-474) from BasisLinear.lean into a new file BasisLinear/SymmPlane.lean, renaming all definitions with symm prefix (e.g. basisAsCharges → symmBasisAsCharges, P → Psymm, etc.) and updating all internal references and documentation accordingly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…ifiers Extract Section C (the shifted plane) from BasisLinear.lean into its own file at BasisLinear/ShiftPlane.lean. All identifiers are renamed to use and the evenShftSnd typo is fixed to evenShiftSnd. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…Pshift - Remove sections A, B, C (now in ChargeSplits, SymmPlane, ShiftPlane) - Import SymmPlane and ShiftPlane publicly - Update module doc to reflect new structure Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…name identifiers - Changed imports to public import SymmPlane and ShiftPlane submodules - Removed sections A (ChargeSplits), B (SymmPlane), C (ShiftPlane) - Kept sections D, E, F with updated references - Fixed typo Pa_evenShitZero → Pa_evenShiftZero - Renamed Pa_zero! → Pa_zero_shift - Partially updated Even/LineInCubic.lean references Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…cancellation Rename first plane: basis/P/P' → symmBasis/Psymm/Psymm' (symmetric plane) Rename second plane: basis!/P!/P!' → shiftBasis/Pshift/Pshift' (shifted plane) Split into ChargeSplits.lean, SymmPlane.lean, ShiftPlane.lean sub-files Update downstream references in LineInCubic and Parameterization files Agent-Logs-Url: https://github.com/leanprover-community/physlib/sessions/b925f308-353b-4b1d-9802-a285d5d40e54 Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

jstoobysmith

I've given you some comments for the Even case. The analogous comments hold for the odd case.

jstoobysmith · 2026-04-20T14:27:52Z

+-/
+
+/-- A point in the span of the shifted plane basis as a charge. -/
+def Pshift (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • shiftBasisAsCharges i


shiftPlane would be a better renaming.

Renamed Pshift → shiftPlane in both Even and Odd cases. See commit e03833b.

jstoobysmith · 2026-04-20T14:28:08Z

+-/
+
+/-- A point in the span of the shifted plane basis. -/
+def Pshift' (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • shiftBasis i


shiftPlaneLinSol.

Renamed Pshift' → shiftPlaneLinSols in both Even and Odd cases. See commit e03833b.

jstoobysmith · 2026-04-20T14:28:41Z

+-/
+
+/-- A point in the span of the symmetric plane basis as a charge. -/
+def Psymm (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • symmBasisAsCharges i


symmPlane better name.

Renamed Psymm → symmPlane in both Even and Odd cases. See commit e03833b.

jstoobysmith · 2026-04-20T14:28:54Z

+-/
+
+/-- A point in the span of the symmetric plane basis. -/
+def Psymm' (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • symmBasis i


symmPlaneLinSols

Renamed Psymm' → symmPlaneLinSols in both Even and Odd cases. See commit e03833b.

jstoobysmith · 2026-04-20T14:29:40Z

 set_option backward.isDefEq.respectTransparency false in
-lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
-    accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
+lemma Psymm_Psymm_shiftBasis_accCube (g : Fin n.succ → ℚ) (j : Fin n) :


These results should go into the appropriately named file.

Moved the mixed cubic ACC results (symmPlane_symmPlane_shiftBasisAsCharges_accCube and shiftPlane_shiftPlane_symmBasisAsCharges_accCube) from BasisLinear.lean into ShiftPlane.lean, which imports SymmPlane and thus has access to both planes' definitions. See commit e03833b.

jstoobysmith · 2026-04-20T14:31:15Z

+
+/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the first `n.succ`,
+  casted into `Fin (2 * n.succ)`. -/
+def evenFst (j : Fin n.succ) : Fin (2 * n.succ) :=


These should go into the appropriate file with the corresponding plane. There is no need to make a new file for these.

Removed the ChargeSplits.lean files. The symmetric charge splits (evenFst/evenSnd/oddFst/oddSnd) are now in SymmPlane.lean and the shifted charge splits (evenShiftFst/oddShiftFst etc.) are in ShiftPlane.lean. See commit e03833b.

jstoobysmith · 2026-04-20T14:32:27Z

@copilot Address the review.

jstoobysmith · 2026-04-20T14:55:38Z

@copilot address the concerns in the review of this PR

Extract section A.1 (even split definitions) and section B (first plane) from BasisLinear.lean into a new SymmPlane.lean file with renamed definitions: - basisAsCharges → symmBasisAsCharges - basis → symmBasis - P → symmPlane - P' → symmPlaneLinSols - basis_linear_independent → symmBasis_linear_independent and all related lemma names updated accordingly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Extract sections A.2, A.3, C, and D from BasisLinear.lean into a new ShiftPlane.lean module with descriptive renamings: - basis! (LinSols) → shiftBasis - P! → shiftPlane Also fixes the evenShftSnd typo to evenShiftSnd. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…imports Include Section A.1 (symmetric split: odd_shift_eq, oddFst, oddSnd, oddMid, sum_odd) directly in SymmPlane.lean alongside Section B (symmetric plane). Import from BasisLinear and VectorLike directly instead of ChargeSplits. Apply all renamings consistently: - P → symmPlane, P' → symmPlaneLinSols - basisAsCharges → symmBasisAsCharges, basis → symmBasis - All lemma names updated to match (e.g. P_oddFst → symmPlane_oddFst) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…ntent Replace the existing ShiftPlane.lean with a version that: - Imports SymmPlane instead of ChargeSplits - Includes sections A.2-A.4 (shifted split, shifted-shifted split, relating lemmas) - Adds section D (mixed cubic ACC: symmPlane_symmPlane_shiftBasisAsCharges_accCube) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…dentifiers Rewrite BasisLinear.lean to contain only the combined basis (sections E and F), importing SymmPlane and ShiftPlane via the ShiftPlane transitive import. All identifiers are renamed to the new convention: - P → symmPlane, P! → shiftPlane - P' → symmPlaneLinSols, P!' → shiftPlaneLinSols - basis → symmBasis, basis! → shiftBasis - Pa_zero! → Pa_zero_shift - Pa_evenShitZero → Pa_evenShiftZero (typo fix) - span_basis_swap! → span_basis_swapShift Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…renamed identifiers imports from ShiftPlane and renamed identifiers (symmPlane, shiftPlane, symmPlaneLinSols, shiftPlaneLinSols, symmBasis, shiftBasis, etc.). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

…rgeSplits, move charge splits into plane files, move mixed cubic ACC into ShiftPlane Renames applied: - Psymm/P → symmPlane, Psymm'/P' → symmPlaneLinSols - Pshift/P! → shiftPlane, Pshift'/P!' → shiftPlaneLinSols - basisAsCharges → symmBasisAsCharges, basis!AsCharges → shiftBasisAsCharges - basis → symmBasis, basis! → shiftBasis File restructuring: - Removed ChargeSplits.lean (charge splits moved into SymmPlane/ShiftPlane) - Mixed cubic ACC results moved from BasisLinear.lean into ShiftPlane.lean - ShiftPlane imports SymmPlane, BasisLinear imports ShiftPlane Agent-Logs-Url: https://github.com/leanprover-community/physlib/sessions/aa00691e-9564-4dcd-b911-c97145618373 Co-authored-by: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>

Copilot · 2026-04-20T15:48:04Z

I've given you some comments for the Even case. The analogous comments hold for the odd case.

Applied all review feedback to both Even and Odd cases in commit e03833b:

Psymm/P → symmPlane, Psymm'/P' → symmPlaneLinSols
Pshift/P! → shiftPlane, Pshift'/P!' → shiftPlaneLinSols
Removed ChargeSplits.lean, moved charge splits into the appropriate plane files
Moved mixed cubic ACC results into ShiftPlane.lean

Note: The renaming in Even/Parameterization.lean and Odd/Parameterization.lean proof bodies is partially incomplete — a few P g/P! f references remain in those files.

Initial plan

ec61389

Copilot AI assigned Copilot and jstoobysmith Apr 20, 2026

Copilot started work on behalf of jstoobysmith April 20, 2026 13:33 View session

Copilot AI linked an issue Apr 20, 2026 that may be closed by this pull request

Naming in Anomaly Cancellation for QED #1046

Open

Copilot AI and others added 9 commits April 20, 2026 13:40

Copilot AI changed the title ~~[WIP] Refactor variable names in Anomaly Cancellation for QED~~ Rename and split QED anomaly cancellation plane definitions for clarity Apr 20, 2026

Copilot finished work on behalf of jstoobysmith April 20, 2026 14:26

Copilot AI requested a review from jstoobysmith April 20, 2026 14:26

jstoobysmith reviewed Apr 20, 2026

View reviewed changes

Copilot started work on behalf of jstoobysmith April 20, 2026 14:55 View session

Copilot AI and others added 7 commits April 20, 2026 15:03

Copilot finished work on behalf of jstoobysmith April 20, 2026 15:49

Copilot AI requested a review from jstoobysmith April 20, 2026 15:49

Conversation

Copilot AI commented Apr 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Naming

File splitting

Documentation

Status

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Apr 20, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Apr 20, 2026

Uh oh!

jstoobysmith commented Apr 20, 2026

Uh oh!

Copilot AI commented Apr 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Copilot AI commented Apr 20, 2026 •

edited

Loading