Semantic correctness of the distinguished-point algorithm

This module proves the semantic correctness of the six-step distinguished-point procedure for evaluating a fixed iterate f^[T] x using walk length K:

1. Scan (scan, scan_spec): walk K steps from x, recording the first distinguished point c = f^[d] x with d ≤ K if one occurs, and ending at u = f^[K] x.
2. Lookup: read the pre-shifted payload z c = f^[T - K] c.
3. Correction (correctionStep, correction_run): apply f for K - d steps from z c to obtain f^[K - d] (f^[T - K] (f^[d] x)) = f^[T] x (shifted_payload).
4. Period walk (periodWalk, periodWalk_spec): in a separate register, walk up to K steps from u = f^[K] x to find its minimal return period 1 ≤ λ ≤ K when the prefix repeats.
5. Residue and cycle walk (walkStep, walk_run): walk R λ = (T - K) % λ steps from u.
6. Output (distinguishedPower, distinguishedPower_correct): return the corrected checkpoint value when the scan hit H, and the cycle-walk value otherwise.

The set H of distinguished points is abstract: the proof assumes only that every trajectory prefix x, f x, …, f^[K] x of K + 1 pairwise distinct states meets H.

Main definitions

• Cslib.FunctionalGraph.runStages: sequential execution of k indexed stages.
• Cslib.FunctionalGraph.ScanState, Cslib.FunctionalGraph.scanStep, Cslib.FunctionalGraph.scan: the K-step distinguished-point prefix scan.
• Cslib.FunctionalGraph.correctionStep: the forward-correction stage.
• Cslib.FunctionalGraph.PeriodState, Cslib.FunctionalGraph.periodStep, Cslib.FunctionalGraph.periodWalk: the short-cycle period walk in a separate register.
• Cslib.FunctionalGraph.walkStep: the bounded cycle-walk stage.
• Cslib.FunctionalGraph.distinguishedPower: the six-step distinguished-point procedure.

Main results

• Cslib.FunctionalGraph.shifted_payload: forward correction of a backward-shifted checkpoint payload recovers f^[T] x.
• Cslib.FunctionalGraph.scan_spec: invariant and specification of the prefix scan.
• Cslib.FunctionalGraph.correction_run: exact step count of the forward correction.
• Cslib.FunctionalGraph.periodWalk_spec: exact first return time of the period walk.
• Cslib.FunctionalGraph.walk_run: exact step count of the cycle walk.
• Cslib.FunctionalGraph.distinguishedPower_correct: semantic correctness of the distinguished-point procedure.

References

• Adapted from lean/Proofs/{Reconstruction,DistinguishedPoints}.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

theorem Cslib.FunctionalGraph.shifted_payload {α : Type u} {f : α → α} {x : α} {d K T : ℕ} (hd : d ≤ K) (hT : K ≤ T) : f^[K - d] (f^[T - K] (f^[d] x)) = f^[T] x

A checkpoint at time d ≤ K permits forward-only correction of the backward-shifted payload f^[T - K] (f^[d] x) when K ≤ T.

def Cslib.FunctionalGraph.runStages {β : Type v} (step : ℕ → β → β) : ℕ → β → β

Apply indexed stages 0, …, k - 1 in order.

@[simp]

theorem Cslib.FunctionalGraph.runStages_zero {β : Type v} (step : ℕ → β → β) (b : β) : runStages step 0 b = b

Running no stages leaves the state unchanged.

@[simp]

theorem Cslib.FunctionalGraph.runStages_succ {β : Type v} (step : ℕ → β → β) (k : ℕ) (b : β) : runStages step (k + 1) b = step k (runStages step k b)

Running k + 1 stages runs the first k and then stage k.

Step 1: Prefix scan

structure Cslib.FunctionalGraph.ScanState (α : Type u) : Type u

The state (u, found, d, c) maintained during the distinguished-point prefix scan.

• u : α

  Current trajectory state.

• found : Bool

  Whether a distinguished point has been encountered so far.

• d : ℕ

  Index of the first distinguished point encountered.

• c : α

  The first distinguished point encountered.

def Cslib.FunctionalGraph.scanStep {α : Type u} (f : α → α) (H : α → Prop) [DecidablePred H] (K i : ℕ) (σ : ScanState α) : ScanState α

Scan stage i: record the first distinguished point, then advance u unless i = K.

def Cslib.FunctionalGraph.scan {α : Type u} (f : α → α) (H : α → Prop) [DecidablePred H] (K : ℕ) (x : α) : ScanState α

Run stages i = 0, 1, …, K of the scan starting from (x, false, 0, x).

theorem Cslib.FunctionalGraph.scan_spec {α : Type u} (f : α → α) (H : α → Prop) [DecidablePred H] (K : ℕ) (x : α) : (scan f H K x).u = f^[K] x ∧ ((scan f H K x).found = true ↔ ∃ i ≤ K, H (f^[i] x)) ∧ ((scan f H K x).found = true → (scan f H K x).d ≤ K ∧ H (f^[(scan f H K x).d] x) ∧ (∀ i < (scan f H K x).d, ¬H (f^[i] x)) ∧ (scan f H K x).c = f^[(scan f H K x).d] x)

The scan ends at f^[K] x and records the first distinguished point among x, f x, …, f^[K] x whenever one exists.

Step 3: Forward correction

def Cslib.FunctionalGraph.correctionStep {α : Type u} (f : α → α) (d i : ℕ) (v : α) : α

Correction stage i: apply f exactly when d ≤ i.

theorem Cslib.FunctionalGraph.correction_run {α : Type u} (f : α → α) (d k : ℕ) (v : α) : runStages (correctionStep f d) k v = f^[k - d] v

Running k correction stages applies f exactly k - d times.

Step 4: Period walk in a separate register

structure Cslib.FunctionalGraph.PeriodState (α : Type u) : Type u

The configuration (w, found, period) of the short-cycle period walk.

• w : α

  Current walking state.

• found : Bool

  Whether a return to the starting state y has been observed.

• period : ℕ

  Recorded return period (initialized to dummy value 1).

def Cslib.FunctionalGraph.periodStep {α : Type u} (f : α → α) [DecidableEq α] (y : α) (i : ℕ) (σ : PeriodState α) : PeriodState α

Period stage i (step j = i + 1): advance w and record i + 1 on the first return to y.

def Cslib.FunctionalGraph.periodWalk {α : Type u} (f : α → α) [DecidableEq α] (K : ℕ) (y : α) : PeriodState α

Run K stages of the period walk from y.

theorem Cslib.FunctionalGraph.periodWalk_spec {α : Type u} (f : α → α) [DecidableEq α] (K : ℕ) (y : α) (h : ∃ (p : ℕ), 1 ≤ p ∧ p ≤ K ∧ f^[p] y = y) : 1 ≤ (periodWalk f K y).period ∧ (periodWalk f K y).period ≤ K ∧ Function.IsPeriodicPt f (periodWalk f K y).period y ∧ ∀ (j : ℕ), 1 ≤ j → j < (periodWalk f K y).period → f^[j] y ≠ y

If y returns to itself within K positive steps, periodWalk f K y records the least positive return time 1 ≤ λ ≤ K.

Step 5: Cycle walk

def Cslib.FunctionalGraph.walkStep {α : Type u} (f : α → α) (r i : ℕ) (v : α) : α

Cycle-walk stage i: apply f exactly when i < r.

theorem Cslib.FunctionalGraph.walk_run {α : Type u} (f : α → α) (r k : ℕ) (v : α) : runStages (walkStep f r) k v = f^[min r k] v

Running k cycle-walk stages applies f exactly min r k times.

The complete distinguished-point procedure

def Cslib.FunctionalGraph.distinguishedPower {α : Type u} (f : α → α) (H : α → Prop) [DecidablePred H] [DecidableEq α] (K T : ℕ) (z : α → α) (R : ℕ → ℕ) (x : α) : α

The six-step distinguished-point procedure for f^[T] with walk length K, payload table z, and residue table R. For T < K it unrolls T steps; otherwise it scans K steps, corrects the payload z σ.c forward, walks the period of σ.u = f^[K] x in a separate register, advances σ.u by R w.period steps, and selects the checkpoint branch iff the scan hit H.

theorem Cslib.FunctionalGraph.distinguishedPower_correct {α : Type u} (f : α → α) (H : α → Prop) [DecidablePred H] [DecidableEq α] (K T : ℕ) (z : α → α) (R : ℕ → ℕ) (hhit : ∀ (y : α), (∀ i ≤ K, ∀ j ≤ K, f^[i] y = f^[j] y → i = j) → ∃ i ≤ K, H (f^[i] y)) (hz : ∀ (h : α), H h → z h = f^[T - K] h) (hR : ∀ (l : ℕ), 1 ≤ l → l ≤ K → R l = (T - K) % l) (x : α) : distinguishedPower f H K T z R x = f^[T] x

Semantic correctness of the distinguished-point algorithm. If every prefix of K + 1 pairwise distinct states meets H, the payloads satisfy z h = f^[T - K] h on H, and the residues satisfy R l = (T - K) % l for 1 ≤ l ≤ K, then distinguishedPower f H K T z R x = f^[T] x for every input x.