Clifford project

Blueprint Summary🔗

Overview
Total entries64completed: 45; deps incomplete: 2; sorries: 9; no proof: 6
Ready now9Entries whose next formalization step is currently unblocked.
Fully closed45Local code and prerequisite closure are both complete.
Actionable priorities7Entries ready now and already unlocking downstream work.
Current blockers9Missing external or incomplete Lean declarations.
Missing informal coverage35Entries with Lean code but missing an informal statement or proof block.
Ready next (7)
  • 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)
  • tau_sq_eq_omega(Lemma)
    Ready for proof work.
    owner: Christian Schaffnereffort: smallstage: proofstatement: formalizeddirect uses: 3downstream unlocks: 3proof: 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_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)
  • symp_adjoint(Lemma)
    Ready for proof work.
    owner: William Hasleyeffort: mediumstage: proofstatement: formalizeddirect uses: 1downstream unlocks: 1proof: Lean code incomplete
    Associated lean decls (5)
Current blockers (9)
Missing informal coverage (35)
Entry index (64)
Definitions10completed: 6; deps incomplete: 1; sorries: 1; no proof: 0
Lemmas49completed: 39; deps incomplete: 1; sorries: 8; no proof: 1
Theorems4completed: 0; deps incomplete: 0; sorries: 0; no proof: 4
Corollaries1completed: 0; deps incomplete: 0; sorries: 0; no proof: 1
Lean-only entries16
Informal-only entries8
Definition Index (10)
Theorem / Proposition / Lemma / Corollary Index (54)
By parent groups (7)
Structure of the Clifford group. (2)
Core properties of the single-qudit Pauli matrices. (7)
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. (9)
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 (5)
    • symp_det(Lemma)
      Reverse dependencies recorded in proof dependencies.
      proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (4)
    • 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 (1)
Group health (7)
  • Core properties of the single-qudit Pauli group.displacement_core
    Grouped view over entries sharing the same parent.
    total: 8closed: 2local-only: 1ready: 5blocked: 0incomplete Lean: 5unlock 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: no ready child currently unlocks downstream work.
  • Roots of unity and their basic properties.roots_of_unity
    Grouped view over entries sharing the same parent.
    total: 11closed: 10local-only: 0ready: 1blocked: 0incomplete Lean: 1unlock score: 26
    Next: tau_sq_eq_omega stage: proofdownstream unlocks: 3
  • Basic properties of the symplectic inner product.symplectic_form
    Grouped view over entries sharing the same parent.
    total: 9closed: 8local-only: 0ready: 1blocked: 0incomplete Lean: 1unlock score: 21
    Next: symp_adjoint stage: proofdownstream unlocks: 1
  • Core properties of the single-qudit Pauli matrices.Pauli_core
    Grouped view over entries sharing the same parent.
    total: 9closed: 8local-only: 0ready: 1blocked: 0incomplete Lean: 1unlock score: 18
    Next: no ready child currently unlocks downstream work.
  • 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: no ready child currently unlocks downstream work.
  • 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
Metadata
Owners in use7Distinct owners referenced by the current blueprint entries.
Owner rollups (7)
  • William HasleyWilliam_Hasley
    entries: 8actionable: 3quick wins: 0linked PRs: 0
  • Gina MuussGina_Muuss
    entries: 5actionable: 1quick wins: 0linked PRs: 0
  • Daan PlankenDaan_Planken
    entries: 3actionable: 1quick wins: 0linked PRs: 0
  • Christian SchaffnerChristian_Schaffner
    entries: 1actionable: 1quick wins: 0linked PRs: 0
  • Maris OzolsMaris_Ozols
    entries: 12actionable: 0quick wins: 0linked PRs: 0
  • Carli BruinsmaCarli_Bruinsma
    entries: 9actionable: 0quick wins: 0linked PRs: 0
  • Joppe StokvisJoppe_Stokvis
    entries: 2actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner24
Missing effort32
Untagged64
Missing owner (24)
  • Clifford_group_size(Lemma)
    Missing owner metadata.
    effort: medium
  • Clifford_group_structure(Theorem)
    Missing owner metadata.
    effort: large
  • Clifford_structure(Corollary)
    Missing owner metadata.
    effort: small
  • Weyl_representation_action(Theorem)
    Missing owner metadata.
    effort: large
  • Weyl_representation_def(Definition)
    Missing owner metadata.
    effort: small
  • Weyl_representation_unitarity(Theorem)
    Missing owner metadata.
    effort: large
  • X_inv_pow(Lemma)
    Missing owner metadata.
    Associated lean decls (1)
  • X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow(Lemma)
    Missing owner metadata.
    Associated lean decls (1)
  • X_pow_eq_mod_d(Lemma)
    Missing owner metadata.
    Associated lean decls (1)
  • Z_inv(Lemma)
    Missing owner metadata.
    Associated lean decls (1)
  • Show all 14 more entries missing owner
    • Z_inv_pow(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • Z_pow_eq_mod_d(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • Z_pow_n(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • clifford_symplectic_action(Theorem)
      Missing owner metadata.
      effort: large
    • dimension_again(Lemma)
      Missing owner metadata.
    • dimension_again2(Lemma)
      Missing owner metadata.
    • non_zero_dimension(Lemma)
      Missing owner metadata.
    • omega_pow_k_mod_d_eq_pow_k_int(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • omega_pow_k_mod_d_eq_pow_k_zmod(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • order_omega(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • semidirect_product(Definition)
      Missing owner metadata.
    • symplectic_dimension(Lemma)
      Missing owner metadata.
    • tau_star(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
    • zero_le_c_mod_d(Lemma)
      Missing owner metadata.
      Associated lean decls (1)
Missing effort (32)
  • D_add_nsmul(Lemma)
    Missing effort metadata.
    owner: Carli Bruinsma
    Associated lean decls (1)
  • D_pow_nsmul(Lemma)
    Missing effort metadata.
    owner: Joppe Stokvis
    Associated lean decls (1)
  • Pauli_X(Definition)
    Missing effort metadata.
    owner: Maris Ozols
    Associated lean decls (1)
  • Pauli_Z(Definition)
    Missing effort metadata.
    owner: Maris Ozols
    Associated lean decls (1)
  • Pauli_group(Definition)
    Missing effort metadata.
    owner: William Hasley
    Associated lean decls (1)
  • X_dagger(Lemma)
    Missing effort metadata.
    owner: Gina Muuss
    Associated lean decls (1)
  • X_inv_pow(Lemma)
    Missing effort metadata.
    Associated lean decls (1)
  • X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow(Lemma)
    Missing effort metadata.
    Associated lean decls (1)
  • X_pow_d_eq_one(Lemma)
    Missing effort metadata.
    owner: Gina Muuss
    Associated lean decls (1)
  • X_pow_eq_mod_d(Lemma)
    Missing effort metadata.
    Associated lean decls (1)
  • Show all 22 more entries missing effort
Untagged (64)
Structure and coverage
Informal-only8Statements with no associated Lean code yet.
Ready to formalize9Entries whose next step is currently unblocked.
Formalized, ancestors open2Local Lean work is done, but prerequisite closure is still open.
Fully closed45Local code and ancestor closure are both complete.
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 (50)
No dependents (40)
Proof debt hotspots (5)
  • Core properties of the single-qudit Pauli group.displacement_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 5incomplete decls: 5missing decls: 0total debt: 5
  • Basic properties of the symplectic inner product.symplectic_form
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • Core properties of the single-qudit Pauli matrices.Pauli_core
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1
  • 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
  • Roots of unity and their basic properties.roots_of_unity
    Grouped proof/code debt derived from the current incomplete-declaration snapshots.
    affected entries: 1incomplete decls: 1missing decls: 0total debt: 1