Rename and split QED anomaly cancellation plane definitions for clarity

[Copilot]

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. The AsCharges suffix now consistently distinguishes the Charges inclusion from the LinSols inclusion:

• Symmetric plane (symmBasisAsCharges / symmPlaneAsCharges / symmPlane): basis vectors pair charges at positions from the symmetric split ((n+1) + n odd, n.succ + n.succ even)
• Shifted plane (shiftBasisAsCharges / shiftPlaneAsCharges / shiftPlane): 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)).LinSols  := ∑ i, f i • basis i

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

The combined-basis helpers in Basis.lean are also renamed:

• basisa → basis, basisaAsBasis → basisAsBasis
• Pa → basisCharge (a charge in the span of the combined basis)
• Pa' → spanBasis (a LinSols in the span of the combined basis)
• swapShift_as_add → linSolRep_swap_evenShift_eq_add / linSolRep_swap_oddShift_eq_add (Mathlib-style)

File organisation

Each monolithic BasisLinear.lean (~1000 lines) is split into sub-modules. The subdirectory is renamed Planes/ and the top-level file is renamed Basis.lean:

• Planes/SymmPlane.lean — symmetric charge splits, symmetric plane basis (symmBasisAsCharges / symmBasis), inclusion (symmPlaneAsCharges / symmPlane), ACC proofs; sections labelled A. and B.
• Planes/ShiftPlane.lean — shifted charge splits (sections A.1–A.2), shifted plane basis and inclusion (section B., shiftBasisAsCharges / shiftBasis / shiftPlaneAsCharges / shiftPlane), ACC proofs; shiftBasis_linear_independent placed directly after shiftBasis
• Basis.lean (formerly BasisLinear.lean) — combined basis (basis, basisCharge, spanBasis), span theorem, mixed cubic ACC lemmas (symmPlane_symmPlane_shiftBasisAsCharges_accCube, shiftPlane_shiftPlane_symmBasisAsCharges_accCube), imports above

Charge index splitting definitions are co-located with their corresponding plane (no separate ChargeSplits file).

Documentation

Module docs explain the naming motivation. Section numbering is sequential within each file (A.1, A.2, B.1, … in ShiftPlane.lean; 1., 2., 3. in Basis.lean).

Status

All renames and file splits are complete for both Odd and Even cases, including Odd/Parameterization.lean and Even/Parameterization.lean, with Physlib.lean imports updated.

[jstoobysmith]

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

[jstoobysmith]

shiftPlaneLinSol.

[Copilot]

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

[jstoobysmith]

symmPlaneLinSols

[Copilot]

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

[jstoobysmith]

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

[Copilot]

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]

@copilot Address the review.

[jstoobysmith]

@copilot address the concerns in the review of this PR

[Copilot]

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.

[jstoobysmith]

Given comments for the Even case, also all apply for the odd case.

[jstoobysmith]

Make these headers more descriptive

[Copilot]

Made section headers more descriptive (e.g. "The basis vectors as LinSols" instead of "The vectors as linear solutions"). Applied in commit 5f7d373.

[jstoobysmith]

Make a new section

[Copilot]

Added a new section break before the shiftPlaneAsCharges definition (the inclusion into charges), separating it from the shiftBasis LinSols results. Applied in commit 5f7d373.

[jstoobysmith]

Would rename to shiftPlaneAsCharges

[Copilot]

Renamed shiftPlane (Charges version) → shiftPlaneAsCharges. Similarly symmPlane (Charges) → symmPlaneAsCharges. Applied to both Even and Odd in commit 5f7d373.

[jstoobysmith]

would rename to shiftPlane. Similar with all of the examples in the other files.

[Copilot]

Renamed shiftPlaneLinSols → shiftPlane (and analogously symmPlaneLinSols → symmPlane) throughout all Even and Odd files. Commit 5f7d373.

[jstoobysmith]

Needs moving up to other results on shiftBasis

[Copilot]

Moved shiftBasis_linear_independent up to be right after the shiftBasis definition (now section C.5/C.6), before shiftPlaneAsCharges. Applied to both Even and Odd in commit 5f7d373.

[jstoobysmith]

Give this a better name, more in line with Mathlib conventions.

[Copilot]

Renamed swapShift_as_add → linSolRep_swap_evenShift_eq_add (Even) and linSolRep_swap_oddShift_eq_add (Odd), following Mathlib naming conventions. Commit 5f7d373.

[jstoobysmith]

Rename this basis now

[Copilot]

Renamed basisa → basis (and basisaAsBasis → basisAsBasis, basisa_linear_independent → basis_linear_independent, basisa_card → basis_card). Commit 5f7d373.

[jstoobysmith]

Fix numbering. I would also rename this file Basis.

[Copilot]

Fixed section numbering (E./F. → 1./2.) and renamed the file BasisLinear.lean → Basis.lean for both Even and Odd. All imports updated. Commit 5f7d373.

[jstoobysmith]

I would give a more descriptive name to Pa an Pa'. Similar to the names given below.

[Copilot]

Renamed Pa → basisCharge and Pa' → basisLinSol (descriptive names: "a charge in the span of the combined basis" / "a LinSols in the span"). All associated lemmas renamed accordingly (basisCharge_evenShiftFst, basisLinSol_eq, etc.). Commit 5f7d373.

[jstoobysmith]

@copilot fix the review comments above.

[Copilot]

Given comments for the Even case, also all apply for the odd case.

All review comments have been applied to both Even and Odd cases in commit 5f7d373.

@copilot fix the review comments above.

All review comments addressed in commit 5f7d373. Key changes: renamed shiftPlane/symmPlane (Charges) to shiftPlaneAsCharges/symmPlaneAsCharges; shiftPlaneLinSols/symmPlaneLinSols to shiftPlane/symmPlane; basisa → basis; Pa/Pa' → basisCharge/basisLinSol; fixed section numbering; moved shiftBasis_linear_independent up; renamed BasisLinear.lean → Basis.lean; renamed swapShift_as_add to Mathlib-style names. All applied to both Even and Odd cases.

[jstoobysmith]

Again comments given for the Even case but should carry over to the Odd case aswell.

[jstoobysmith]

maybe spanBasis would be better here.

[Copilot]

Renamed basisLinSol → spanBasis (with associated lemmas spanBasis_symmPlane_shiftPlane, spanBasis_eq, spanBasis_elim_eq_iff) in both Even and Odd cases. Commit 7ee7905.

[jstoobysmith]

These numberings should start at e.g. A.1.

[Copilot]

Fixed — sections now start at A.1. in ShiftPlane.lean (A.2→A.1, A.3→A.2 for Even; A.2→A.1, A.3→A.2, A.4→A.3 for Odd). Applied to both Even and Odd. Commit 7ee7905.

[jstoobysmith]

Rename this section to B. don't use second plane here.

[Copilot]

Renamed to ## B. The shifted plane and renumbered all subsections C.x → B.x in both Even and Odd ShiftPlane.lean. Commit 7ee7905.

[jstoobysmith]

These results should likely go in the Basis.lean file

[Copilot]

Moved symmPlane_symmPlane_shiftBasisAsCharges_accCube and shiftPlane_shiftPlane_symmBasisAsCharges_accCube from ShiftPlane.lean to a new ## 3. Mixed cubic anomaly cancellation conditions involving both planes section in Basis.lean. Applied to both Even and Odd. Commit 7ee7905.

[jstoobysmith]

I would rename the directory these results are in to Planes.

[Copilot]

Renamed BasisLinear/ → Planes/ for both Even and Odd (files are now at Even/Planes/SymmPlane.lean, Even/Planes/ShiftPlane.lean, etc.). All imports updated. Commit 7ee7905.

[jstoobysmith]

@copilot Address the review comments above.

[Copilot]

Again comments given for the Even case but should carry over to the Odd case aswell.

All changes applied to both Even and Odd cases in commit 7ee7905.

@copilot Address the review comments above.

All review comments addressed in commit 7ee7905: basisLinSol → spanBasis; section numbering fixed (A.1, A.2, ...); section "C. second plane" → "B. The shifted plane" with B.x subsections; mixed cubic ACC lemmas moved to Basis.lean; BasisLinear/ directory renamed to Planes/. All applied to both Even and Odd cases.