Transitive Imported Duplicates

Blueprint Summary🔗

Overview
Total entries1completed: 1; deps incomplete: 0; incomplete code: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed1Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage1Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (1)
  • «dup.imported.node»(Definition)
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
Entry index (1)
Definitions1completed: 1; deps incomplete: 0; incomplete code: 0; no proof: 0
Lean-only entries1
Definition Index (1)
  • «dup.imported.node»(Definition)
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
Metadata
Metadata audit
Missing owner1
Missing effort1
Untagged1
Missing owner (1)
  • «dup.imported.node»(Definition)
    Missing owner metadata.
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
Missing effort (1)
  • «dup.imported.node»(Definition)
    Missing effort metadata.
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
Untagged (1)
  • «dup.imported.node»(Definition)
    Missing tag metadata.
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
Structure and coverage
Fully closed1Local code and ancestor closure are both complete.
No prerequisites (1)
  • «dup.imported.node»(Definition)
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB
No dependents (1)
  • «dup.imported.node»(Definition)
    Associated lean decls (2)
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA
    • Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderB.importedNodeB