ForestPathCounting.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Counting all realizable numbered path families

The union is over every finite acyclic graph, not a single graph with fixed numerical coefficients. A typed forest shape and two endpoints per segment determine the entire family of numbered paths.

structure OAI.TwoPointCorrelations.ForestPathData line 19
Source documentation
A finite realization of the regular segments in one column.
```
structure ForestPathData (N segments : ℕ) where
…
```
def OAI.TwoPointCorrelations.ForestPathData.pattern line 38
def OAI.TwoPointCorrelations.ForestPathData.shape line 41
def OAI.TwoPointCorrelations.ForestPathData.index line 46
abbrev OAI.TwoPointCorrelations.ForestPathData.Code line 53
def OAI.TwoPointCorrelations.ForestPathData.code line 56
theorem OAI.TwoPointCorrelations.ForestPathData.pattern_eq_of_code_eq line 60
Source documentation
No numerical vertex label survives in the code.
```
theorem pattern_eq_of_code_eq (d e : ForestPathData N segments) (h : d.code = e.code) :
    d.pattern = e.pattern := by
…
```
Mentions: OAI.TwoPointCorrelations.ForestPathData
theorem OAI.TwoPointCorrelations.ForestPathData.card_code_le line 75
def OAI.TwoPointCorrelations.RealizableForestPaths line 87
Source documentation
This range includes the union over all finite graph realizations.
```
def RealizableForestPaths (N segments : ℕ) :=
…
```
def OAI.TwoPointCorrelations.realizableForestPathCode line 90
theorem OAI.TwoPointCorrelations.realizableForestPathCode_injective line 94
theorem OAI.TwoPointCorrelations.card_realizable_forest_paths line 103
Source documentation
A coefficient-independent bound for all reduced regular path families.
```
theorem card_realizable_forest_paths (N segments : ℕ) :
    Nat.card (RealizableForestPaths N segments) ≤
      2 ^ (3 * N + 1) * N ^ (2 * segments) := by
…
```
Mentions: OAI.TwoPointCorrelations.RealizableForestPaths