Short, nonmerging segments between refined checkpoints

Between refined checkpoints in forestMarks f H, every non-root mark x ∈ forestMarks f H (0 < transientDepth f x) has a unique compressed forest edge IsForestEdge f H x d ending at the first positive-time visit to forestMarks f H (IsForestEdge.unique). When H satisfies the L-step checkpoint covering property (Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H), every compressed edge has length d ≤ 2 * L (exists_short_forest_edge), and every state in checkpointHull f H either belongs to forestMarks f H or lies on a compressed edge of length at most 2 * L (forest_hull_partition).

Because unmarked vertices in the hull have at most one transient hull predecessor (forestPredecessor_unique), two compressed edges cannot merge in their interiors (forest_edge_interior_inj), so each compressed edge is uniquely identified by its last predecessor f^[d - 1] x before its upper endpoint (forest_edge_last_injective).

Main definitions

• Cslib.FunctionalGraph.IsForestEdge: compressed edge from a mark x ∈ forestMarks f H to the next mark f^[d] x ∈ forestMarks f H along the transient path.

Main results

• Cslib.FunctionalGraph.IsForestEdge.unique: the length d of a compressed edge from x is unique.
• Cslib.FunctionalGraph.exists_short_forest_edge: every non-root mark has a compressed edge of length at most 2 * L.
• Cslib.FunctionalGraph.forest_edge_interior_inj: interiors of compressed edges are disjoint.
• Cslib.FunctionalGraph.forest_edge_last_injective: the last predecessor f^[d - 1] x uniquely identifies (x, d).
• Cslib.FunctionalGraph.forest_hull_partition: every state in checkpointHull f H is either a mark or lies on a compressed edge of length at most 2 * L.
• Cslib.FunctionalGraph.forest_segment_contains_of_depth: depth filtering ensures any matching last-predecessor key on a short prefix identifies the containing compressed edge.
• Cslib.FunctionalGraph.forest_reaches_through_edge: any mark reaching the interior of a compressed edge passes through its lower endpoint.
• Cslib.FunctionalGraph.checkpoint_before_distant_target: any transient target at distance greater than 2 * L is preceded by a checkpoint in H within fewer than 2 * L steps.

References

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

theorem Cslib.FunctionalGraph.forest_cycle_entry_mem {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} (hx : x ∈ checkpointHull f H) : f^[transientDepth f x] x ∈ forestMarks f H

The cycle entry f^[transientDepth f x] x of a hull state x is marked.

theorem Cslib.FunctionalGraph.forest_iterate_mem_sources {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} (hx : x ∈ checkpointHull f H) {i : ℕ} (hi : i < transientDepth f x) : f^[i] x ∈ forestSources f H

For a hull state x and i < transientDepth f x, the state f^[i] x is a forest source.

structure Cslib.FunctionalGraph.IsForestEdge {α : Type u} [Finite α] (f : α → α) (H : Finset α) (x : α) (d : ℕ) : Prop

A compressed edge ends at the next mark, no later than cycle entry.

• start_mem : x ∈ forestMarks f H

  The starting vertex is a refined mark.

• pos : 0 < d

  The edge has positive length.

• le_depth : d ≤ transientDepth f x

  The edge does not cross the cycle entry of x.

• end_mem : f^[d] x ∈ forestMarks f H

  The upper endpoint is a refined mark.

• interior (i : ℕ) : 0 < i → i < d → f^[i] x ∉ forestMarks f H

  No intermediate vertex is a refined mark.

theorem Cslib.FunctionalGraph.IsForestEdge.source {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} {d : ℕ} (h : IsForestEdge f H x d) {i : ℕ} (hi : i < d) : f^[i] x ∈ forestSources f H

Every state f^[i] x with i < d on a compressed edge is a forest source.

theorem Cslib.FunctionalGraph.IsForestEdge.unique {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x : α} {d₁ d₂ : ℕ} (h₁ : IsForestEdge f H x d₁) (h₂ : IsForestEdge f H x d₂) : d₁ = d₂

The length of a compressed edge from x is unique.

theorem Cslib.FunctionalGraph.exists_short_forest_edge {α : Type u} [Finite α] (f : α → α) (H : Finset α) {L : ℕ} (_hL : 0 < L) (hcover : ∀ (x : α), Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H) {x : α} (hx : x ∈ forestMarks f H) (hd : 0 < transientDepth f x) : ∃ d ≤ 2 * L, IsForestEdge f H x d

Applying checkpoint coverage after one step bounds each compressed edge by 2 * L.

theorem Cslib.FunctionalGraph.forest_edge_interior_inj {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x y : α} {d e : ℕ} (hx : IsForestEdge f H x d) (hy : IsForestEdge f H y e) {i j : ℕ} (hi : i < d) (hj : j < e) (he : f^[i] x = f^[j] y) : x = y ∧ i = j

Interiors of compressed edges are disjoint, including their starting marks.

theorem Cslib.FunctionalGraph.forest_edge_last_injective {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x y : α} {d e : ℕ} (hx : IsForestEdge f H x d) (hy : IsForestEdge f H y e) (he : f^[d - 1] x = f^[e - 1] y) : x = y ∧ d = e

Last-predecessor keys identify compressed edges uniquely.

theorem Cslib.FunctionalGraph.forest_hull_partition {α : 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) : y ∈ forestMarks f H ∨ ∃ (a : α) (d : ℕ) (i : ℕ), IsForestEdge f H a d ∧ d ≤ 2 * L ∧ i < d ∧ f^[i] a = y

Every hull point is marked or belongs to a short compressed edge.

theorem Cslib.FunctionalGraph.forest_segment_contains_of_depth {α : Type u} [Finite α] (f : α → α) (H : Finset α) {a y : α} {d k : ℕ} (ha : IsForestEdge f H a d) (hy : y ∈ checkpointHull f H) (hdepth : transientDepth f y ≤ transientDepth f a) (he : f^[k] y = f^[d - 1] a) : ∃ i < d, f^[i] a = y

Depth filtering makes any eligible last-predecessor match identify the containing edge.

theorem Cslib.FunctionalGraph.forest_reaches_through_edge {α : Type u} [Finite α] (f : α → α) (H : Finset α) {a h : α} {d i t : ℕ} (ha : IsForestEdge f H a d) (hh : h ∈ forestMarks f H) (hi : i < d) (he : f^[t] h = f^[i] a) : ∃ (u : ℕ), f^[u] h = a

A marked vertex reaches an edge interior only by passing its lower marked endpoint.

theorem Cslib.FunctionalGraph.forest_transient_reachable_mem {α : Type u} [Finite α] (f : α → α) (H : Finset α) {x y : α} (hx : x ∈ checkpointHull f H) (hy : 0 < transientDepth f y) (hr : ∃ (t : ℕ), f^[t] x = y) : y ∈ checkpointHull f H

A state of positive transient depth that is reachable from a hull state lies in the hull.

theorem Cslib.FunctionalGraph.checkpoint_before_distant_target {α : Type u} [Finite α] (f : α → α) (H : Finset α) {L : ℕ} (hcover : ∀ (x : α), Repeats f x L ∨ ∃ t < 2 * L, f^[t] x ∈ H) {x y : α} (hy : 0 < transientDepth f y) (hr : ∃ (t : ℕ), f^[t] x = y) (hfar : ∀ i ≤ 2 * L, f^[i] x ≠ y) : ∃ d < 2 * L, f^[d] x ∈ H ∧ ∃ (u : ℕ), f^[u] (f^[d] x) = y

A transient target beyond the inspected prefix lies above a prefix checkpoint.