ConstructedBoundaryAssembly.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Discharging the published assembly interface

The three maps are the constructed analytic cycle index maps. Their two naturality squares follow from spatial inclusion, with explicit reindexing of the manuscript's vertex sets.

theorem OAI.CoarseAssembly.constructedBoundaryIndex_natural_base line 32
theorem OAI.CoarseAssembly.constructedBoundaryIndex_natural_total line 66
def OAI.CoarseAssembly.constructedBoundaryAssembly line 104
Source documentation
The published interface is now supplied by the constructed analytic index.
```
def constructedBoundaryAssembly : PublishedBoundaryAssemblyInput where
…
```
Mentions: OAI.CoarseAssembly.PublishedBoundaryAssemblyInput