Patterns.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The finite path-pattern domain

A component is the list of its positive assigned-path amounts. An empty component is an unused clique vertex. Components are ordered and identified with their reversals, as in manuscript Lemma finite:coverage.

def OAI.CycleClique.Construction.amountSequences line 17

Source documentation

Positive amount sequences with at most the indicated number of edges and total amount at most the budget.

def amountSequences : ℕ → ℕ → List (List ℕ)
  | 0, _ => [[]]
  | e + 1, b => [] :: (List.range b).flatMap (fun q =>
      (amountSequences e (b - (q + 1))).map (fun p => (q + 1) :: p))

theorem OAI.CycleClique.Construction.mem_amountSequences line 22
def OAI.CycleClique.Construction.LexLE line 69
instance OAI.CycleClique.Construction.(instance at line 71) line 71
def OAI.CycleClique.Construction.pathPatterns line 77
Source documentation
The compact checker's exact pattern recursion, including extensions of components which do not themselves meet the ordering restriction.
```
def pathPatterns (t b : ℕ) (first : List ℕ := []) : List (List (List ℕ)) :=
…
```
def OAI.CycleClique.Construction.patternCount line 86

def OAI.CycleClique.Construction.pathPatternsFuel line 90

Source documentation

Structurally recursive evaluator for the same domain. The fuel is bounded by the number of remaining clique vertices.

def pathPatternsFuel : ℕ → ℕ → ℕ → List ℕ → List (List (List ℕ))
  | _, 0, _, _ => [[]]
  | 0, _ + 1, _, _ => []
  | f + 1, t + 1, b, first =>
    ((amountSequences t b).filter (fun p => decide (LexLE first p ∧ LexLE p p.reverse))).flatMap
      (fun p => (pathPatternsFuel f (t - p.length) (b - p.sum) p).map (fun P => p :: P))

Mentions: OAI.CycleClique.Construction.amountSequences, OAI.CycleClique.Construction.LexLE

theorem OAI.CycleClique.Construction.pathPatterns_eq_fuel line 97

def OAI.CycleClique.Construction.patternNumberFuel line 115

Source documentation

Count components recursively without constructing a single long flattened list. This keeps kernel reductions shallow.

def patternNumberFuel : ℕ → ℕ → ℕ → List ℕ → ℕ
  | _, 0, _, _ => 1
  | 0, _ + 1, _, _ => 0
  | f + 1, t + 1, b, first =>
    (((amountSequences t b).filter (fun p => decide (LexLE first p ∧ LexLE p p.reverse))).map
      (fun p => patternNumberFuel f (t - p.length) (b - p.sum) p)).sum

Mentions: OAI.CycleClique.Construction.amountSequences, OAI.CycleClique.Construction.LexLE

theorem OAI.CycleClique.Construction.pathPatternsFuel_length line 122
def OAI.CycleClique.Construction.amountSequenceSum line 134
Source documentation
Sum over amount sequences by their short branching recursion, rather than reducing a list whose length can approach the recursion-depth limit.
```
def amountSequenceSum : ℕ → ℕ → (List ℕ → ℕ) → ℕ
  | 0, _, F => F []
  | e + 1, b, F => F [] + ((List.range b).map (fun q =>
      amountSequenceSum e (b - (q + 1)) (fun p => F ((q + 1) :: p)))).sum
```
theorem OAI.CycleClique.Construction.sum_flatMap_nat line 139
theorem OAI.CycleClique.Construction.amountSequenceSum_eq line 145
theorem OAI.CycleClique.Construction.sum_map_filter line 152
def OAI.CycleClique.Construction.patternNumberShallow line 158
theorem OAI.CycleClique.Construction.patternNumberFuel_eq_shallow line 165
def OAI.CycleClique.Construction.patternVertices line 176
def OAI.CycleClique.Construction.patternAmount line 178
def OAI.CycleClique.Construction.PatternValid line 180
theorem OAI.CycleClique.Construction.mem_pathPatterns line 187
Source documentation
Exact coverage of the canonical domain, independently of the graph obstruction checker. Each component uses one more clique vertex than edges.
```
theorem mem_pathPatterns {t b : ℕ} {first : List ℕ} {P : List (List ℕ)} :
    P ∈ pathPatterns t b first ↔
      patternVertices P = t ∧ patternAmount P ≤ b ∧ PatternValid first P := by
…
```
Mentions: OAI.CycleClique.Construction.pathPatterns, OAI.CycleClique.Construction.patternVertices, OAI.CycleClique.Construction.patternAmount, OAI.CycleClique.Construction.PatternValid