OAI/Analysis/MutuallyUnbiased/Certificate/IntegerMerge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Evaluation-preserving sparse integer merge. Its soundness needs no sorting hypothesis: ordering is only used to make generated witnesses short. Each merge can be checked independently by a finite integer-list equality.

  1. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_append line 13
  2. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_perm line 16
  3. def OAI.MUB6.Certificate.Integer.Sparse.scale line 21
  4. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_scale line 23
  5. def OAI.MUB6.Certificate.Integer.Sparse.mergeFuel line 33
  6. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_mergeFuel line 44
  7. def OAI.MUB6.Certificate.Integer.Sparse.merge line 71
  8. theorem OAI.MUB6.Certificate.Integer.Sparse.eval_merge line 74