auto-task(PlaneSeven.B): remove B₀–B₆ definitions in favour of a single B : Fin 7 → Charges

[jstoobysmith]

Summary

Completes the TODO in
Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Ordinary/DimSevenPlane.lean:

Remove the definitions of elements (SM 3).Charges B₀, B₁ etc, here [use] only
B : Fin 7 → (SM 3).Charges.

The seven separate top-level definitions B₀, B₁, …, B₆ are removed. The basis of the
dimension-7 plane is now provided solely by the single function
B : Fin 7 → (SM 3).Charges, defined directly by inlining each basis element as an arm
of its match. The helper lemmas (Bᵢ_cubic, Bᵢ_Bi_cubic) and
basis_linear_independent are restated/adjusted to refer to B 0, …, B 6 instead of the
removed Bᵢ; the underlying proof tactics are unchanged apart from unfolding B in place
of the individual definitions. The TODO marker is deleted.

No change to statements or proofs of the public results B_in_accCube, B_sum_is_sol,
basis_linear_independent, or seven_dim_plane_exists.

How to review

• Confirm the seven def B₀ … def B₆ are gone and the file defines a single
  abbrev B : Fin 7 → (SM 3).Charges (grep: grep -nE 'def B[₀-₆]|abbrev B' <file>
  shows only the abbrev B line).
• Confirm the TODO "..." note is removed.
• lake build Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane
  succeeds with no errors and no warnings.
• No sorry, and #print axioms SMRHN.SM.seven_dim_plane_exists reports only
  propext, Classical.choice, Quot.sound (no new axioms).

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.