PathIncidences.lean`

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.PathIncidences.Opened.openAt line 18
Source documentation
Open one cyclic passage into two interval endpoints.
```
def openAt (c : O) : EntropyStages.Pairing O where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.Opened.openAt_fixed_iff line 30
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.Opened.openAt_unmatched_card line 37
def OAI.TorsionFreeZeroDivisors.PathIncidences.cyclePairing line 58
Source documentation
Cyclic consecutive edge incidences. succ is the permutation of edge positions; opening its passage at one position handles an interval path.
```
def cyclePairing {E : Type*} (succ : Equiv.Perm E) : EntropyStages.Pairing (E × Bool) where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.cyclePairing_free line 64
def OAI.TorsionFreeZeroDivisors.PathIncidences.pathPairing line 69
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.pathPairing_card line 74
def OAI.TorsionFreeZeroDivisors.PathIncidences.port line 91
Source documentation
Initial and terminal half-edge of an occurrence, respectively.
```
def port (x : E × Bool) : D := if x.2 then reverse (edge x.1) else edge x.1
```
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.partner_turn line 93
def OAI.TorsionFreeZeroDivisors.PathIncidences.passages line 117
Source documentation
The incidence passage data is derived from the actual adjacency and nonbacktracking conditions, not assumed as an extra vertex-count estimate.
```
def passages
    (hvertex : ∀ i, cut ≠ some (succ i) → origin (edge (succ i)) = origin (reverse (edge i)))
    (hreduced : ∀ i, cut ≠ some (succ i) → edge (succ i) ≠ reverse (edge i)) :
    IncidenceStages.Passages origin (port reverse edge) where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages, OAI.TorsionFreeZeroDivisors.PathIncidences.port
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.card_toNat line 146
def OAI.TorsionFreeZeroDivisors.PathIncidences.familyPairing line 150
Source documentation
Disjoint union of the passages of the individual path components.
```
def familyPairing {I : Type*} {O : I → Type*} (P : ∀ i, EntropyStages.Pairing (O i)) :
    EntropyStages.Pairing (Sigma O) where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing
def OAI.TorsionFreeZeroDivisors.PathIncidences.unmatchedEquiv line 157
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.family_unmatched_card line 166
def OAI.TorsionFreeZeroDivisors.PathIncidences.familyPort line 179
def OAI.TorsionFreeZeroDivisors.PathIncidences.familyPassages line 181
theorem OAI.TorsionFreeZeroDivisors.PathIncidences.family_vertex_bound line 191
Source documentation
The exact occurrence balance for any union of immersed circles and intervals.
```
theorem family_vertex_bound :
    (∑ v : V, IncidenceStages.Passages.maxMultiplicity
      (origin := origin) (port := familyPort reverse edge) v) ≤
…
```
Mentions: OAI.TorsionFreeZeroDivisors.IncidenceStages.Passages.maxMultiplicity, OAI.TorsionFreeZeroDivisors.PathIncidences.port, OAI.TorsionFreeZeroDivisors.PathIncidences.familyPort
abbrev OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveD line 218
abbrev OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveV line 219
def OAI.TorsionFreeZeroDivisors.StageSubgraphs.stage line 223
Source documentation
The actual multiplicity stage has precisely its incident vertices. No inactive vertices are counted or forced to embed.
```
def stage (m : D → ℕ) (hm : ∀ d, m (Γ.reverse d) = m d) (j : ℕ) :
    PortGraph (ActiveV Γ m j) (ActiveD m j) where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveV, OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveD
def OAI.TorsionFreeZeroDivisors.StageSubgraphs.maxAt line 230
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.active_iff line 234
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.vertex_card line 238
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.sum_vertex_card line 243
def OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges line 263
Source documentation
Literal undirected stage edges; both orientations name a single edge.
```
def edges : Finset (Sym2 D) := Finset.univ.image (fun d => s(d,Γ.reverse d))
```
def OAI.TorsionFreeZeroDivisors.StageSubgraphs.edgeName line 264
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.fiber_card line 267
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.two_edges line 290
Source documentation
A fixed-point-free port involution has exactly two darts per edge.
```
theorem two_edges : 2*(edges Γ).card = Fintype.card D := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.sum_dart_card line 299
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.sum_edge_card line 315
Source documentation
Counting actual stage edges with multiplicity, not expected edges.
```
theorem sum_edge_card (m : D → ℕ) (hr : ∀ d, m (Γ.reverse d) = m d)
    (M H : ℕ) (hm : ∀ d, m d ≤ M) (hH : ∑ d, m d = 2*H) :
    (∑ j : Fin M, (edges (stage Γ m hr j.val)).card) = H := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges, OAI.TorsionFreeZeroDivisors.StageSubgraphs.stage
def OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity line 327
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity_reverse line 332
Source documentation
Source traversal multiplicity agrees on the two orientations.
```
theorem multiplicity_reverse (d : D) :
    multiplicity Γ edge (Γ.reverse d) = multiplicity Γ edge d := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.sum_multiplicity line 357
Source documentation
Each edge occurrence contributes one incidence in each orientation.
```
theorem sum_multiplicity : (∑ d : D, multiplicity Γ edge d) =
    2*(∑ i, Fintype.card (E i)) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.family_vertex_total line 375
Source documentation
Exact vertex inequality for the actual stages of the immersed family, derived from the literal consecutive passages.
```
theorem family_vertex_total (M : ℕ) (hm : ∀ d, multiplicity Γ edge d ≤ M) :
    (∑ j : Fin M, Fintype.card (ActiveV Γ (multiplicity Γ edge) j.val)) ≤
      (∑ i, Fintype.card (E i)) + ∑ i, if (cut i).isSome then 1 else 0 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity, OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveV
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.family_edge_total line 383
Source documentation
Every traversal contributes exactly one undirected edge over all stages.
```
theorem family_edge_total (M : ℕ) (hm : ∀ d, multiplicity Γ edge d ≤ M) :
    (∑ j : Fin M, (edges (stage Γ (multiplicity Γ edge)
      (multiplicity_reverse Γ edge) j.val)).card) = ∑ i, Fintype.card (E i) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity, OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges, OAI.TorsionFreeZeroDivisors.StageSubgraphs.stage, OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity_reverse
theorem OAI.TorsionFreeZeroDivisors.StageSubgraphs.family_exponent_nonpos line 391
Source documentation
The n-exponent of actual stage embeddings is nonpositive; the initial vertex saving is claimed only at the first stage of every rooted interval.
```
theorem family_exponent_nonpos (M : ℕ) (hM : 0 < M)
    (hm : ∀ d, multiplicity Γ edge d ≤ M) :
    (∑ j : Fin M, ((Fintype.card (ActiveV Γ (multiplicity Γ edge) j.val) : ℤ) -
      (edges (stage Γ (multiplicity Γ edge) (multiplicity_reverse Γ edge) j.val)).card -
      if j.val = 0 then (∑ i, if (cut i).isSome then 1 else 0 : ℕ) else 0)) ≤ 0 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity, OAI.TorsionFreeZeroDivisors.StageSubgraphs.ActiveV, OAI.TorsionFreeZeroDivisors.StageSubgraphs.edges, OAI.TorsionFreeZeroDivisors.StageSubgraphs.stage, OAI.TorsionFreeZeroDivisors.StageSubgraphs.multiplicity_reverse