Navigation through a compressed checkpoint forest

For a transient target y, an anchor a (ForestAnchor f H L y a) is either y itself when y ∈ forestMarks f H, or the lower endpoint a of a compressed edge IsForestEdge f H a d of length d ≤ 2 * L whose last-predecessor key f^[d - 1] a is reached from y within k ≤ 2 * L steps while transientDepth f y ≤ transientDepth f a. On checkpointHull f H, every vertex has a unique anchor (exists_forest_anchor, forestAnchor_unique), and any mark reaching y must pass through a (forest_anchor_contains).

Combining a short 2 * L-step prefix check from x, a selected prefix mark h ∈ forestMarks f H (sound and complete for hitting H within < 2 * L steps), an anchor a for y with a short 2 * L-step verification prefix from a to y, and subtree interval containment low a ≤ low h ∧ low h ≤ high a yields an exact characterization of reachability ∃ t, f^[t] x = y (forest_navigation_spec).

ForestEdgeTable packages the compressed edges of all non-root marks into a finite table of at most (forestMarks f H).card entries with injective last-predecessor keys (key_injective), characterizing ForestAnchor by key lookup and depth comparison (ForestEdgeTable.anchor_iff).

Main definitions

• Cslib.FunctionalGraph.ForestAnchor: candidate lower endpoint for a target y, obtained either as a mark y ∈ forestMarks f H or via a depth-filtered last-predecessor key of a short compressed edge.
• Cslib.FunctionalGraph.ForestEdgeTable: finite table storing one short compressed edge per non-root mark in forestMarks f H.
• Cslib.FunctionalGraph.ForestEdgeTable.key: the last predecessor f^[length j - 1] (start j) of the j-th compressed edge.

Main results

• Cslib.FunctionalGraph.exists_forest_anchor: every state in checkpointHull f H has an anchor.
• Cslib.FunctionalGraph.forestAnchor_unique: the anchor of any state in checkpointHull f H is unique.
• Cslib.FunctionalGraph.forest_anchor_contains: on checkpointHull f H, an anchor is a mark reaching y in at most 2 * L steps through which every mark reaching y must pass.
• Cslib.FunctionalGraph.forest_navigation_spec: exact transient reachability via two selected records, interval labels, and short orbit prefixes.
• Cslib.FunctionalGraph.exists_forest_edge_table: existence of ForestEdgeTable f H L.
• Cslib.FunctionalGraph.ForestEdgeTable.key_injective: the last-predecessor keys of the table are pairwise distinct.
• Cslib.FunctionalGraph.ForestEdgeTable.anchor_iff: characterization of ForestAnchor via table keys.

References

• Adapted from lean/Proofs/ForestNavigation.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.FunctionalGraph.ForestAnchor {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) (y a : α) : Prop

A candidate lower endpoint obtained from a marked target or a depth-filtered edge key.

theorem Cslib.FunctionalGraph.exists_forest_anchor {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) (hL : 0 < L) (hcover : ∀ (x : α), Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H) {y : α} (hy : y ∈ checkpointHull f H) : ∃ (a : α), ForestAnchor f H L y a

If every orbit repeats among its first L states or meets H within 2 * L steps, every state of checkpointHull f H has an anchor.

theorem Cslib.FunctionalGraph.forestAnchor_unique {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) {y a₁ a₂ : α} (hy : y ∈ checkpointHull f H) (h₁ : ForestAnchor f H L y a₁) (h₂ : ForestAnchor f H L y a₂) : a₁ = a₂

Every state in checkpointHull f H has at most one anchor.

theorem Cslib.FunctionalGraph.forest_anchor_contains {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) {y a : α} (hy : y ∈ checkpointHull f H) (ha : ForestAnchor f H L y a) : a ∈ forestMarks f H ∧ (∃ i ≤ 2 * L, f^[i] a = y) ∧ ∀ h ∈ forestMarks f H, (∃ (t : ℕ), f^[t] h = y) → ∃ (t : ℕ), f^[t] h = a

All eligible keys are safe on hull points; selection need not choose the first key.

theorem Cslib.FunctionalGraph.forest_navigation_spec {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) (hL : 0 < L) (hcover : ∀ (x : α), Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H) (low high : α → Fin (Nat.card α)) (hinterval : ∀ (x y : α), low y ≤ low x ∧ low x ≤ high y ↔ ∃ t ≤ transientDepth f x, f^[t] x = y) (x y h a : α) (hy : 0 < transientDepth f y) (foundH foundA : Bool) (hHsound : foundH = true → h ∈ forestMarks f H ∧ ∃ d ≤ 2 * L, f^[d] x = h) (hHcomplete : (∃ d ≤ 2 * L, f^[d] x ∈ forestMarks f H) → foundH = true) (hAsound : foundA = true → ForestAnchor f H L y a) (hAcomplete : (∃ (b : α), ForestAnchor f H L y b) → foundA = true) : (∃ (t : ℕ), f^[t] x = y) ↔ (∃ i ≤ 2 * L, f^[i] x = y) ∨ foundH = true ∧ foundA = true ∧ (∃ i ≤ 2 * L, f^[i] a = y) ∧ low a ≤ low h ∧ low h ≤ high a

Exact transient reachability using two selected records and one verification prefix.

structure Cslib.FunctionalGraph.ForestEdgeTable {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) : Type u

The finite table stores one short edge for each nonroot marked vertex.

• count : ℕ

  Number of stored compressed edges.

• start : Fin self.count → α

  Lower marked endpoint of each compressed edge.

• length : Fin self.count → ℕ

  Step length of each compressed edge.

• edge (j : Fin self.count) : IsForestEdge f H (self.start j) (self.length j)

  Every entry is a valid compressed edge.

• short (j : Fin self.count) : self.length j ≤ 2 * L

  Every compressed edge has length at most 2 * L.

• start_injective : Function.Injective self.start

  Lower endpoints are pairwise distinct.

• complete (a : α) : a ∈ forestMarks f H → 0 < transientDepth f a → ∃ (j : Fin self.count), self.start j = a

  Every non-root mark in forestMarks f H appears in the table.

• card_le : self.count ≤ (forestMarks f H).card

  The number of edges is at most (forestMarks f H).card.

theorem Cslib.FunctionalGraph.exists_forest_edge_table {α : Type u} [Finite α] (f : α → α) (H : Finset α) (L : ℕ) (hL : 0 < L) (hcover : ∀ (x : α), Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H) : Nonempty (ForestEdgeTable f H L)

If every orbit repeats among its first L states or meets H within 2 * L steps, a table of short compressed edges for the non-root marks exists.

def Cslib.FunctionalGraph.ForestEdgeTable.key {α : Type u} [Finite α] {f : α → α} {H : Finset α} {L : ℕ} (table : ForestEdgeTable f H L) (j : Fin table.count) : α

The last predecessor before the upper endpoint of the j-th compressed edge.

theorem Cslib.FunctionalGraph.ForestEdgeTable.key_injective {α : Type u} [Finite α] {f : α → α} {H : Finset α} {L : ℕ} (table : ForestEdgeTable f H L) : Function.Injective table.key

Distinct table entries have distinct last-predecessor keys.

theorem Cslib.FunctionalGraph.ForestEdgeTable.anchor_iff {α : Type u} [Finite α] {f : α → α} {H : Finset α} {L : ℕ} (table : ForestEdgeTable f H L) (y a : α) : ForestAnchor f H L y a ↔ y ∈ forestMarks f H ∧ a = y ∨ ∃ (j : Fin table.count) (k : ℕ), table.start j = a ∧ k ≤ 2 * L ∧ transientDepth f y ≤ transientDepth f a ∧ f^[k] y = table.key j

The edge dictionary and the depth filter characterize exactly the edge-anchor candidates.