TokenBoundary.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact vertex tests express a generator through incoming coefficients.

theorem OAI.HarmonicArtin.ParabolicIntersections.generator_token_boundary line 16
Source documentation
A boundary for the token of a generator, retaining the precise source level and cochain support. This is the first step of Lemma 7.3.
```
theorem generator_token_boundary (E : BasedComplex Q (K := ℂ) I) (hE : E.IsMinimal Q)
…
```