Prove the dimension-2 and dimension-3 SIC-POVM benchmarks

[DomTheDeveloper]

Summary

Closes the four low-dimensional benchmark placeholders in FormalConjectures/OpenQuantumProblems/23.lean:

• qubitSICFamily_pairwise
• hasSICPOVM_two
• hesseFamily_pairwise
• hasSICPOVM_three

The dimension-2 proof verifies the tetrahedral qubit family by exact finite algebra. The dimension-3 proof checks all distinct pairs in the nine-vector Hesse family, using explicit identities for the cube root of unity and the normalization constants.

This adapts the low-dimensional finite-verification strategy from the earlier unmerged upstream work in google-deepmind#3652 to the current compressed definitions and Mathlib version.

Verification

The focused audit:

1. builds the exact local import dependency;
2. compiles the canonical FormalConjectures/OpenQuantumProblems/23.lean source;
3. appends #print axioms to the canonical source in the same Lean compilation;
4. rejects sorryAx, Lean.ofReduceBool, and Lean.trustCompiler.

Final focused result: green.

OpenQuantumProblem23.qubitSICFamily_pairwise
  [propext, Classical.choice, Quot.sound]
OpenQuantumProblem23.hasSICPOVM_two
  [propext, Classical.choice, Quot.sound]
OpenQuantumProblem23.hesseFamily_pairwise
  [propext, Classical.choice, Quot.sound]
OpenQuantumProblem23.hasSICPOVM_three
  [propext, Classical.choice, Quot.sound]

Status

Kept as a draft until the repository-wide lake --wfail build is green.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[DomTheDeveloper]

Focused canonical Lean compile and exact in-source axiom audit are green. Requesting the full repository lake --wfail build while keeping this PR in draft.

[DomTheDeveloper]

The strict focused gate inspected the current source declarations directly, avoiding stale cached OLEANs. No sorryAx, Lean.ofReduceBool, or Lean.trustCompiler appears in any of the four exact theorem dependency chains.

[DomTheDeveloper]

Keeping this draft until the full repository build finishes; no merge is being attempted.