DependencyExpansion.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Finite dependency expansions with two edge sorts. The certificate checks progress and local branching at every actual node; the global count follows from these local conditions.

def OAI.EditApproximation.dependencyWordCount line 13
theorem OAI.EditApproximation.dependencyWordCount_succ line 16
theorem OAI.EditApproximation.dependencyPathBudget_mono line 25
theorem OAI.EditApproximation.dependencyPathBudget_zero_zero line 33
theorem OAI.EditApproximation.dependencyPathBudget_succ_zero line 36
theorem OAI.EditApproximation.dependencyPathBudget_zero_succ line 45
theorem OAI.EditApproximation.dependencyPathBudget_succ_succ line 54
theorem OAI.EditApproximation.dependencyPathBudget_recurrence line 80
inductive OAI.EditApproximation.DependencyExpansion line 96
Source documentation
Node labels carry remaining physical depth and remaining rank. Children in the first and second arrays have distinct edge sorts.
```
inductive DependencyExpansion where
…
```
def OAI.EditApproximation.DependencyExpansion.depth line 103
def OAI.EditApproximation.DependencyExpansion.rank line 106
def OAI.EditApproximation.DependencyExpansion.nodeCount line 109
def OAI.EditApproximation.DependencyExpansion.Valid line 115
Source documentation
Every same edge strictly decreases physical depth and never increases rank. Every earlier edge strictly decreases rank and never increases depth. No global count is part of this certificate.
```
def Valid (a b : ℕ) : DependencyExpansion → Prop
  | .node d k m n same earlier =>
      m ≤ a ∧ n ≤ b ∧
      (∀ i, (same i).depth < d ∧ (same i).rank ≤ k ∧ Valid a b (same i)) ∧
      (∀ i, (earlier i).depth ≤ d ∧ (earlier i).rank < k ∧ Valid a b (earlier i))
```
Mentions: OAI.EditApproximation.DependencyExpansion, OAI.EditApproximation.DependencyExpansion.depth, OAI.EditApproximation.DependencyExpansion.rank
theorem OAI.EditApproximation.DependencyExpansion.nodeCount_le_budget line 121
theorem OAI.EditApproximation.DependencyExpansion.nodeCount_le_budget_of_le line 169
def OAI.EditApproximation.DependencyExpansion.nodeCountAtOrAbove line 178
Source documentation
Literal count of nodes whose remaining physical depth is at least floor. Descendants are inspected even when the current node fails the test; pruning below the threshold is a consequence of Valid.
```
def nodeCountAtOrAbove (floor : ℕ) : DependencyExpansion → ℕ
  | .node d _ _ _ same earlier =>
      (if floor ≤ d then 1 else 0) +
        (∑ i, nodeCountAtOrAbove floor (same i)) +
        ∑ i, nodeCountAtOrAbove floor (earlier i)

/-- Literal count of nodes at one remaining physical depth. -/
```
Mentions: OAI.EditApproximation.DependencyExpansion

def OAI.EditApproximation.DependencyExpansion.nodeCountAtDepth line 185

Source documentation

Literal count of nodes at one remaining physical depth.

def nodeCountAtDepth (target : ℕ) : DependencyExpansion → ℕ
  | .node d _ _ _ same earlier =>
      (if d = target then 1 else 0) +
        (∑ i, nodeCountAtDepth target (same i)) +
        ∑ i, nodeCountAtDepth target (earlier i)

Mentions: OAI.EditApproximation.DependencyExpansion

theorem OAI.EditApproximation.DependencyExpansion.nodeCountAtOrAbove_eq_zero line 191
theorem OAI.EditApproximation.DependencyExpansion.nodeCountAtOrAbove_le_budget line 213
Source documentation
The path budget for a depth threshold uses only the available descent above that threshold, independently of the total depth of the expansion.
```
theorem nodeCountAtOrAbove_le_budget (a b floor : ℕ) (tree : DependencyExpansion)
    (h : Valid a b tree) :
    nodeCountAtOrAbove floor tree ≤
      dependencyPathBudget (tree.depth - floor) tree.rank a b := by
…
```
Mentions: OAI.EditApproximation.DependencyExpansion, OAI.EditApproximation.DependencyExpansion.Valid, OAI.EditApproximation.DependencyExpansion.nodeCountAtOrAbove, OAI.EditApproximation.dependencyPathBudget
theorem OAI.EditApproximation.DependencyExpansion.nodeCountAtDepth_le_atOrAbove line 278
def OAI.EditApproximation.DependencyExpansion.nodeCountThroughDescent line 296
Source documentation
All nodes reached with physical descent at most j, including those reached through earlier-index edges that themselves decrease depth.
```
def nodeCountThroughDescent (j : ℕ) (tree : DependencyExpansion) : ℕ :=
…
```
Mentions: OAI.EditApproximation.DependencyExpansion
def OAI.EditApproximation.DependencyExpansion.layerNodeCount line 300
Source documentation
Nodes at physical descent exactly j.
```
def layerNodeCount (j : ℕ) (tree : DependencyExpansion) : ℕ :=
…
```
Mentions: OAI.EditApproximation.DependencyExpansion
theorem OAI.EditApproximation.DependencyExpansion.nodeCountThroughDescent_le_budget line 303
theorem OAI.EditApproximation.DependencyExpansion.layerNodeCount_le_throughDescent line 309
theorem OAI.EditApproximation.DependencyExpansion.layerNodeCount_le_budget line 316
theorem OAI.EditApproximation.DependencyExpansion.nodeCountAtDepth_sum line 322
theorem OAI.EditApproximation.DependencyExpansion.layerNodeCount_sum line 354
Source documentation
The actual layers partition the expansion. This lets weighted initial-state charges be summed layer by layer without using the total depth bound for every layer.
```
theorem layerNodeCount_sum (a b : ℕ) (tree : DependencyExpansion) (h : Valid a b tree) :
    (∑ j ∈ range (tree.depth + 1), layerNodeCount j tree) = tree.nodeCount := by
…
```
Mentions: OAI.EditApproximation.DependencyExpansion, OAI.EditApproximation.DependencyExpansion.Valid, OAI.EditApproximation.DependencyExpansion.layerNodeCount
def OAI.EditApproximation.DependencyExpansion.depthWeightedCount line 369
Source documentation
Charge every actual node by a function of its remaining physical depth, as needed for length-dependent initial-state evaluation.
```
def depthWeightedCount (weight : ℕ → ℕ) : DependencyExpansion → ℕ
  | .node d _ _ _ same earlier => weight d +
      (∑ i, depthWeightedCount weight (same i)) +
      ∑ i, depthWeightedCount weight (earlier i)
```
Mentions: OAI.EditApproximation.DependencyExpansion
theorem OAI.EditApproximation.DependencyExpansion.depthWeightedCount_eq_depth_sum line 374
theorem OAI.EditApproximation.DependencyExpansion.depthWeightedCount_eq_layer_sum line 408

def OAI.EditApproximation.DependencyExpansion.build line 428

Source documentation

Unfold actual finite successor arrays. Local progress makes the construction terminate even when earlier edges also descend physically.

def build {ι : Type*} (d r m n : ι → ℕ)
    (s : (x : ι) → Fin (m x) → ι) (e : (x : ι) → Fin (n x) → ι)
    (hs : ∀ x i, d (s x i) < d x ∧ r (s x i) ≤ r x)
    (he : ∀ x i, d (e x i) ≤ d x ∧ r (e x i) < r x) (root : ι) : DependencyExpansion :=
…

Mentions: OAI.EditApproximation.DependencyExpansion

theorem OAI.EditApproximation.DependencyExpansion.build_depth line 447
theorem OAI.EditApproximation.DependencyExpansion.build_rank line 451
theorem OAI.EditApproximation.DependencyExpansion.build_valid line 455
theorem OAI.EditApproximation.DependencyExpansion.build_nodeCount_le line 486
Source documentation
A global node bound derived directly from actual successor arrays, their two local cardinality bounds, and their local progress proofs.
```
theorem build_nodeCount_le (a b : ℕ) (hm : ∀ x, m x ≤ a) (hn : ∀ x, n x ≤ b) (root : ι) :
    (build d r m n s e hs he root).nodeCount ≤ dependencyPathBudget (d root) (r root) a b := by
…
```
Mentions: OAI.EditApproximation.DependencyExpansion.build, OAI.EditApproximation.DependencyExpansion.nodeCount, OAI.EditApproximation.dependencyPathBudget
theorem OAI.EditApproximation.DependencyExpansion.build_layerNodeCount_le line 491