-
Notifications
You must be signed in to change notification settings - Fork 2
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Thirty-nine blueprint chapter files are unreachable from every entry point
cleanupCode cleanup and style fixesCode cleanup and style fixesdocumentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#7220 In LionSR/TNLean;Paper-gap notes cite 220 declaration names that no longer exist
cleanupCode cleanup and style fixesCode cleanup and style fixesdocumentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#7219 In LionSR/TNLean;Upstream the generic sandwich and trace matrix lemmas to QICLean
cleanupCode cleanup and style fixesCode cleanup and style fixesproof-debtStructural proof debt tracked in docs/proof_debt_ledger.mdStructural proof debt tracked in docs/proof_debt_ledger.mdStatus: Open.#7217 In LionSR/TNLean;Move the channel-generic Kraus non-injectivity lemmas to QICLean
cleanupCode cleanup and style fixesCode cleanup and style fixesproof-debtStructural proof debt tracked in docs/proof_debt_ledger.mdStructural proof debt tracked in docs/proof_debt_ledger.mdStatus: Open.#7216 In LionSR/TNLean;Pages deploy assembler never reads the freshly built site-blueprint/paper-gaps component
bugSomething isn't workingSomething isn't workingciCI/CD workflow changesCI/CD workflow changesStatus: Open.#7215 In LionSR/TNLean;Blueprint declaration scanner miscomputes field indentation when a field carries an inline doc comment
blueprint-syncBlueprint out of sync with Lean codeBlueprint out of sync with Lean codebugSomething isn't workingSomething isn't workinginfrastructureDefinitions and basic lemmasDefinitions and basic lemmasStatus: Open.#7213 In LionSR/TNLean;Migrate IsPrimitiveMPS to reuse QICLean's channel-primitivity certificate directly
formalizationLean 4 formalization taskLean 4 formalization taskStatus: Open.#7181 In LionSR/TNLean;Write the migration-inventory audit note for the #7177 pass-through removals
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#7180 In LionSR/TNLean;Shorten exported BNT block-diagonal declaration names to clear long-line lint warnings
cleanupCode cleanup and style fixesCode cleanup and style fixesparent-hamiltonianParent Hamiltonian theory for MPS (RMP §IV.C)Parent Hamiltonian theory for MPS (RMP §IV.C)Status: Open.#7175 In LionSR/TNLean;Proof-automation ledger: repoint MatrixIsometryKronecker/MatrixReindex entries to QICLean
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#7174 In LionSR/TNLean;Paper-gaps: repoint docstring citations from local compatibility stubs to canonical QICLean URLs
1606.00608arXiv:1606.00608 (MPDO RFP)arXiv:1606.00608 (MPDO RFP)1703.09188arXiv:1703.09188 — Matrix Product UnitariesarXiv:1703.09188 — Matrix Product UnitariesdocumentationImprovements or additions to documentationImprovements or additions to documentationmpuMatrix Product Unitaries: structure, index, symmetries, and QCAMatrix Product Unitaries: structure, index, symmetries, and QCArfp-mpdoRenormalization fixed points and MPDO theoryRenormalization fixed points and MPDO theoryStatus: Open.#7173 In LionSR/TNLean;Paper-gaps: cpgsv17_pf_rank_one compatibility note misstates its verdict as resolved
1606.00608arXiv:1606.00608 (MPDO RFP)arXiv:1606.00608 (MPDO RFP)documentationImprovements or additions to documentationImprovements or additions to documentationrfp-mpdoRenormalization fixed points and MPDO theoryRenormalization fixed points and MPDO theoryStatus: Open.#7172 In LionSR/TNLean;