Clifford project

Blueprint Summary🔗

Overview
Total entries75completed: 51; deps incomplete: 2; sorries: 14; no proof: 6
Ready now18Entries with an actionable next formalization step.
Fully closed51Local code and prerequisite closure are both complete.
Actionable priorities8Entries ready now and already unlocking downstream work.
Current blockers14Missing external or incomplete Lean declarations.
Missing informal coverage45Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (8)
  • D_mul(Lemma)
    Ready for proof work.
    owner: Daan Plankeneffort: smallstage: proofstatement: formalizeddirect uses: 5downstream unlocks: 6proof: Lean code incomplete
    Associated lean decls (1)
  • Pauli_group(Definition)
    Ready for statement work.
    owner: William Hasleystage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 6
    Associated lean decls (1)
  • D_pow_nsmul(Lemma)
    Ready for proof work.
    owner: Joppe Stokvisstage: proofstatement: formalizeddirect uses: 3downstream unlocks: 5proof: Lean code incomplete
    Associated lean decls (1)
  • Weyl_representation_def(Definition)
    Ready for statement work.
    effort: smallstage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 3
  • D_add_nsmul(Lemma)
    Ready for proof work.
    owner: Carli Bruinsmastage: proofstatement: formalizeddirect uses: 2downstream unlocks: 2proof: Lean code incomplete
    Associated lean decls (1)
  • D_pow_d_eq_one(Lemma)
    Ready for proof work.
    owner: William Hasleyeffort: smallstage: proofstatement: formalizeddirect uses: 2downstream unlocks: 2proof: Lean code incomplete
    Associated lean decls (1)
  • D_conj(Lemma)
    Ready for proof work.
    owner: Gina Muusseffort: smallstage: proofstatement: formalizeddirect uses: 1downstream unlocks: 1proof: Lean code incomplete
    Associated lean decls (1)
  • D_p_neq_D_q(Lemma)
    Ready for proof work.
    owner: Carli Bruinsmaeffort: mediumstage: proofstatement: formalizeddirect uses: 1downstream unlocks: 1proof: Lean code incomplete
    Associated lean decls (1)
Current blockers (14)
  • Clifford_group_action(Lemma)
    Declaration with sorry: cliffordGroupAction [theorem/lemma; contains sorry; in proof; refs: 1]
  • X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow(Lemma)
    Declaration with sorry: X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_conj(Lemma)
    Declaration with sorry: conjTranspose_D [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_pow_nsmul(Lemma)
    Declaration with sorry: D_pow_nsmul [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_pow_d_eq_one(Lemma)
    Declaration with sorry: D_pow_d_eq_one [theorem/lemma; contains sorry; in proof; refs: 1]
  • X_inv_pow(Lemma)
    Declaration with sorry: X_inv_pow' [theorem/lemma; contains sorry; in proof; refs: 1]
  • order_omega(Lemma)
    Declaration with sorry: order_omega [theorem/lemma; contains sorry; in proof; refs: 2]
  • D_mul(Lemma)
    Declaration with sorry: D_mul [theorem/lemma; contains sorry; in proof; refs: 1]
  • tau_star_pow(Lemma)
    Declaration with sorry: tau_star_pow [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_add_nsmul(Lemma)
    Declaration with sorry: D_add_nsmul [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_p_neq_D_q(Lemma)
    Declaration with sorry: D_p_neq_D_q [theorem/lemma; contains sorry; in proof; refs: 1]
  • D_mod_d(Lemma)
    Declaration with sorry: D_mod_d [theorem/lemma; contains sorry; in proof; refs: 1]
  • Z_inv_pow(Lemma)
    Declaration with sorry: Z_inv_pow' [theorem/lemma; contains sorry; in proof; refs: 1]
  • Pauli_group(Definition)
    Declaration with sorry: pauliGroup [definition; contains sorry; in proof; refs: 2]
Missing informal coverage (45)
Entry index (75)
Definitions10completed: 6; deps incomplete: 1; sorries: 1; no proof: 0
Lemmas60completed: 45; deps incomplete: 0; sorries: 13; no proof: 2
Theorems4completed: 0; deps incomplete: 1; sorries: 0; no proof: 3
Corollaries1completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Lean-only entries23
Informal-only entries8
Definition Index (10)
Theorem / Proposition / Lemma / Corollary Index (65)
By parent groups (7)
Structure of the Clifford group. (2)
Core properties of the single-qudit Pauli matrices. (9)
Core properties of the single-qudit Pauli group. (6)
Basic properties of the symplectic inner product. (8)
Weyl representation produces the Clifford group. (3)
Roots of unity and their basic properties. (10)
Definition of the Clifford group. (1)
Dependency insights
Statement-used entries9Entries reused in statement dependencies.
Proof-used entries20Entries reused in proof-only dependencies.
Tracked parent groups7Grouped health rollups for parents with more than one child entry.
Most used in statements (9)
  • tau(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
    Associated lean decls (1)
  • omega(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
    Associated lean decls (1)
  • symplectic_inner_product(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 8
    Associated lean decls (1)
  • Weyl_representation_def(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  • displacement(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 8
    Associated lean decls (1)
  • Clifford_group(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 3direct uses: 5downstream unlocks: 5
    Associated lean decls (1)
  • Pauli_X(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 9
    Associated lean decls (1)
  • Pauli_Z(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 9
    Associated lean decls (1)
  • Pauli_group(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    Associated lean decls (1)
Most used in proofs (20)
  • D_mul(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 5statement uses: 0direct uses: 5downstream unlocks: 6
    Associated lean decls (1)
  • Clifford_group(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 3statement uses: 2direct uses: 5downstream unlocks: 5
    Associated lean decls (1)
  • D_pow_nsmul(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 5
    Associated lean decls (1)
  • symp_antisymmetric(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
    Associated lean decls (1)
  • tau_sq_eq_omega(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
    Associated lean decls (1)
  • symplectic_inner_product(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 8
    Associated lean decls (1)
  • displacement(Definition)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 8
    Associated lean decls (1)
  • self_eq_zero(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
    Associated lean decls (1)
  • D_add_nsmul(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • D_pow_d_eq_one(Lemma)
    Reverse dependencies recorded in proof dependencies.
    proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • Show all 10 more proof-used entries
    • Pauli_X(Definition)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 9
      Associated lean decls (1)
    • Pauli_Z(Definition)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 9
      Associated lean decls (1)
    • D_conj(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • D_p_neq_D_q(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • Weyl_representation_action(Theorem)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
    • symp_add_left(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • symp_adjoint(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • symp_det(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • symp_smul_right(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • tau_pow_d_eq_one_of_odd(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (2)
Group health (7)
  • Core properties of the single-qudit Pauli group.displacement_core
    Grouped view over entries sharing the same parent.
    total: 8closed: 1local-only: 0ready: 7blocked: 0incomplete Lean: 7unlock score: 29
    Next: D_mul stage: proofdownstream unlocks: 6
  • Structure of the Clifford group.Structure_core
    Grouped view over entries sharing the same parent.
    total: 3closed: 0local-only: 0ready: 2blocked: 1incomplete Lean: 0unlock score: 0
    Next: Clifford_group_size stage: proofdownstream unlocks: 0
  • Roots of unity and their basic properties.roots_of_unity
    Grouped view over entries sharing the same parent.
    total: 12closed: 11local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 26
    Next: tau_star stage: proofdownstream unlocks: 0
  • Definition of the Clifford group.Clifford_core
    Grouped view over entries sharing the same parent.
    total: 2closed: 0local-only: 1ready: 1blocked: 0incomplete Lean: 1unlock score: 5
    Next: Clifford_group_action stage: proofdownstream unlocks: 0
  • Weyl representation produces the Clifford group.Weyl_representation
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 1blocked: 3incomplete Lean: 0unlock score: 4
    Next: Weyl_representation_def stage: statementdownstream unlocks: 3
  • Basic properties of the symplectic inner product.symplectic_form
    Grouped view over entries sharing the same parent.
    total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 21
    Next: no ready child currently unlocks downstream work.
  • Core properties of the single-qudit Pauli matrices.Pauli_core
    Grouped view over entries sharing the same parent.
    total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 18
    Next: no ready child currently unlocks downstream work.
Metadata
Owners in use7Distinct owners referenced by the current blueprint entries.
Owner rollups (7)
  • William HasleyWilliam_Hasley
    entries: 16actionable: 4quick wins: 0linked PRs: 0
  • Carli BruinsmaCarli_Bruinsma
    entries: 6actionable: 2quick wins: 0linked PRs: 0
  • Maris OzolsMaris_Ozols
    entries: 12actionable: 1quick wins: 0linked PRs: 0
  • Gina MuussGina_Muuss
    entries: 4actionable: 1quick wins: 0linked PRs: 0
  • Daan PlankenDaan_Planken
    entries: 3actionable: 1quick wins: 0linked PRs: 0
  • Joppe StokvisJoppe_Stokvis
    entries: 2actionable: 1quick wins: 0linked PRs: 0
  • Christian SchaffnerChristian_Schaffner
    entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner31
Missing effort38
Untagged75
Missing owner (31)
Missing effort (38)
Untagged (75)
Structure and coverage
Informal-only8Statements with no associated Lean code yet.
Ready to formalize18Entries with an actionable next formalization step.
Formalized, ancestors open2Local Lean work is done, but prerequisite closure is still open.
Fully closed51Local code and ancestor closure are both complete.
Blocked or incomplete4Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (14)
  • Weyl_representation_unitarity(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 11statement deps: 1proof deps: 10direct uses: 0downstream unlocks: 0
  • clifford_symplectic_action(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 11statement deps: 2proof deps: 9direct uses: 0downstream unlocks: 0
  • Clifford_structure(Corollary)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 1proof deps: 9direct uses: 0downstream unlocks: 0
  • Weyl_representation_action(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 6statement deps: 1proof deps: 5direct uses: 1downstream unlocks: 1
  • Clifford_group_structure(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  • displacement(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 8
    Associated lean decls (1)
  • D_pow_nsmul(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 5
    Associated lean decls (1)
  • D_mul(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 6
    Associated lean decls (1)
  • Pauli_group(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
    Associated lean decls (1)
  • D_mod_d(Lemma)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
    Associated lean decls (1)
  • Show all 4 more heaviest-prerequisite entries
    • D_pow_d_eq_one(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 2
      Associated lean decls (1)
    • Clifford_group(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 5
      Associated lean decls (1)
    • Clifford_group_action(Lemma)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
      Associated lean decls (1)
    • Pauli_Z(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
      Associated lean decls (1)
No prerequisites (61)
No dependents (51)
Proof debt hotspots (2)
  • Core properties of the single-qudit Pauli group.displacement_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 7incomplete decls: 7missing decls: 0total debt: 7
  • Definition of the Clifford group.Clifford_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1