Audit immutable qubit and qutrit SIC proofs

[DomTheDeveloper]

Purpose

Runs a clean audit from current main against the immutable SIC proof commit:

7aeef3c2aca76d413f94d13ebf6044e9b6c1d712

The workflow checks out that exact commit, compiles the canonical OpenQuantumProblems/23.lean source, and audits:

• qubitSICFamily_pairwise;
• hasSICPOVM_two;
• hesseFamily_pairwise;
• hasSICPOVM_three.

The axiom gate rejects sorryAx, Lean.ofReduce, Lean.ofReduceBool, and Lean.trustCompiler.

This is audit-only and should not merge.

[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.