Lemma 1.9 — Models 1.1 and 1.2 are equivalent with the same parameters

Proved

PredAdvice.lemma_1_9

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

data-structuresp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1shortest-pathsword-ram

For every directed graph $G$ and vertices $x,v$ : $\mathrm{dist}_{G^{\mathrm{rev}}}(v,x)=\mathrm{dist}_G(x,v)$ .
For every word width, every pair of programs, every planning and execution structure and every parameter tuple $(P,S,A,T,T_{\mathrm{plan}})$ : the data form a successor (advice routing) structure for $G$ in Model 1.2 if and only if they form a predecessor structure for $G^{\mathrm{rev}}$ in Model 1.1, and they form a predecessor structure for $G$ if and only if they form a successor structure for $G^{\mathrm{rev}}$ .

So Models 1.1 and 1.2 are equivalent with the same planning space, execution space, advice size, execution time and planning time; the goal is proved in the successor form and transferred.

Differences from the source:

encoding: equivalent with the same planning space, execution space, advice size, execution time and planning time → an iff for every parameter tuple with the same programs and structures, on G and on G^rev; reason: relies on the mission's common memory layout (fixed endpoint in cell 0, moving vertex in cell 1)
generalization: the lemma → also the identity dist_{G^rev}(v, x) = dist_G(x, v); reason: the displayed step of the proof
generalization: a directed unweighted graph (simple, p.6) → Mathlib's Digraph on a finite vertex type, which may have loops; reason: loops never lie on shortest walks and change no distance; loopless digraphs on n vertices are the special case

Preamble

import Mathlib
import Definitions.Def_PredAdvice_IsPredecessorStructure
import Definitions.Def_PredAdvice_IsSuccessorStructure

set_option autoImplicit false

Formal statement

namespace PredAdvice

open WordRAM

/-- **Lemma 1.9** (Kopelowitz, Korin, Roditty, *Using Small Advice to Compress the Predecessor Matrix*, STOC 2027 submission (manuscript sha256 0ae8a68d…), §1.3.1, p.7). Models 1.1 and 1.2 are equivalent on directed unweighted
graphs, with the same planning space, execution space, advice size, and execution time, and with the
same planning time: a predecessor structure for `G^rev` is a successor structure for `G` (with the
same programs, structures and parameters), and conversely; and `dist_{G^rev}(v, x) = dist_G(x, v)`.

**Formalization Note** "Equivalent with the same parameters" is an iff for every parameter tuple
`(P, S, A, T, T_plan)`, with literally the same programs and stored word lists. This rests on the
mission's common memory layout (fixed endpoint in cell `0`, moving vertex in cell `1`) for both
models. -/
theorem lemma_1_9 :
    (∀ (n : ℕ) (G : Digraph (Fin n)) (x v : Fin n), dist (rev G) v x = dist G x v) ∧
    (∀ (w : Width) (n : ℕ) (G : Digraph (Fin n))
      (plan query : Complexity.Program .multiplication) (PG DG : List (Word w)) (P S : ℝ)
      (A T Tplan : ℕ),
      (IsSuccessorStructure w G plan query PG DG P S A T Tplan ↔
        IsPredecessorStructure w (rev G) plan query PG DG P S A T Tplan) ∧
      (IsPredecessorStructure w G plan query PG DG P S A T Tplan ↔
        IsSuccessorStructure w (rev G) plan query PG DG P S A T Tplan)) := by sorry

end PredAdvice

Source

Kopelowitz, Korin, Roditty, Using Small Advice to Compress the Predecessor Matrix, STOC 2027 submission (manuscript sha256 0ae8a68d…), Lemma 1.9, p.7

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph