[orbitingflea]

Change

Depends on #1091 (refactor(Computability/WordRAM): scope the word-RAM statement syntax and ram_eval, head ae590c4: the scoping commit 7c68492 and a merge of upstream/main). This branch
contains that head; until #1091 merges, the diff here includes it.

Upstream merge. This branch merges upstream/main f86ebad through #1091's refreshed head
ae590c4. Upstream's new Code.rand constructor (#1141) gets one case in execWithin_append
(HeapSift.lean). The bridge follows #1141's change of instrOf to take an outOfBounds
argument: it translates the library program as S.programOf q (upstream's
q.map (S.instrOf q.length)) and uses upstream's step_matches_at with a proved lemma
isRandFree_of_step (a step that does not fault is not at a rand instruction, since
deterministic rand faults). dijkstra_logLinear and DijkstraAbstract.lean are unchanged.

This PR adds Dijkstra's algorithm with a binary heap on the word RAM, and a formal abstract for it.
Upstream has no issue about Dijkstra's algorithm (gh issue list --search Dijkstra --state all
finds none). This draft proposes the development.

Result. Cslib.Algorithms.WordRAM.Dijkstra.logLinearStatement : LogLinearStatement
(Complexity/Algorithms/WordRAM/Dijkstra/LogLinear.lean): there are a word-RAM program over the
exact basis, with a fixed number of registers, and a constant K such that the following holds.
For every directed graph with n vertices, m edges and natural-number weights (parallel edges
and self-loops allowed), given by adjacency lists with offsets, and every word size w with
8 (n + m + 2) (W + 2) < 2 ^ w (W the largest weight), the program halts after at most
K (m + 1) (⌊log₂ n⌋ + 1) instructions. It then holds the encoded distance from the source to
each vertex v at outAddr v (0 for unreachable, d + 1 for distance d). The proof gives
K = 230 with 27 registers. One program works for every word size.

Source and mapping. Dijkstra (1959), Numerische Mathematik 1, p. 270, states the problem:
"Problem 2. Find the path of minimum total length between two given nodes P and Q." It also says:
"In the solution presented, the minimal paths from P to the other nodes are constructed in order of
increasing length until Q is reached." Remark 1 on the same page: "The above
process can also be applied in the case where the length of a branch depends on the direction in
which it is traversed." (Quoted from the scan at
https://courses.cs.cornell.edu/cs2110/2017sp/online/shortestPath/1959dijkstra.pdf.) The bound is
in Jeff Erickson, Algorithms, 1st ed. (June 2019), Chapter 8 "Shortest Paths", Section 8.6
"Best-First: Dijkstra's Algorithm", subsection "No Negative Edges", p. 288 (free from the author at
https://jeffe.cs.illinois.edu/teaching/algorithms/; quoted from
https://jeffe.cs.illinois.edu/teaching/algorithms/book/08-sssp.pdf): "Altogether Dijkstra
performs at most E DecreaseKey operations, and at most V Insert and ExtractMin operations. Thus,
if we implement the underlying priority queue using a standard binary heap, which supports each
operation in O(log V) time, Dijkstra runs in O(E log V) time." (The procedure names are set in
small capitals there.) There G = (V, E, w) is "a weighted directed graph" (p. 273). The bound
is also in Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, 3rd ed. (2009),
Section 24.3 (CLRS2009), which we could not open.

How the Lean statement maps the source:

• V is n (the vertices are Fin n). E is m, the total length of the adjacency lists, so
  parallel edges count separately.
• log V becomes Nat.log 2 n + 1, that is ⌊log₂ n⌋ + 1. The + 1 keeps the factor positive
  for n ≤ 1.
• Weights are natural numbers, so they are nonnegative, as the subsection with the bound assumes
  ("No Negative Edges"). Edges are directed, as in Erickson's G and Dijkstra's Remark 1.
• The input is the adjacency-list representation, encoded as words: n, the source, the n + 1
  offsets of the lists in an edge array, then each edge as target and weight (encode).
• The model is the word RAM over the exact basis with w-bit words. One instruction is one step,
  whatever its operands. The bound counts every instruction executed, the final halt included.
• Quantifiers: one program p with r registers and one constant K, then all n, graphs,
  sources and word sizes that satisfy the word-size condition.
• Output: the distance from the source to every vertex, one memory cell per vertex past the
  input (outAddr). An unreachable vertex (distance ⊤) is encoded as 0, and distance d as
  d + 1.

The bound (m + 1) (⌊log₂ n⌋ + 1) has no n term and assumes no reachability. Erickson's
O(E log V) has no V term either, but his initialization InitSSSP (Section 8.3, p. 276) sets
dist(v) ← ∞ "for all vertices v ≠ s". Here memory past the input starts at 0, so the
per-vertex arrays need no initialization, and the offsets give the adjacency list of any vertex
directly. So the program touches only the vertices it reaches
(Dijkstra/HeapStatement.lean:19-21). The m + 1 keeps the bound positive for m = 0. This
accounting, with no initialization pass and an explicit constant, is ours, not the sources'.
Dijkstra (p. 269) restricts to graphs "where at least one path exists between any two nodes"; the
theorem does not.

Machine. The program is a Program .exact r: every operation computes its exact value, and an
instruction faults on x - y with y > x, on / and % by zero, and on a value that is not a
word. The algorithm is written as structured Code and compiled with Code.program. The
instruction bound is proved for the structured code with ExecWithin: rules for sequences,
branches and loops (with ExecWithin.loop_potential for the main loop), and symbolic interpretation
(ram_exact_eval, through ExecWithin.of_eval) for individual loop-free blocks. Exec.runs then
transfers the run and its step count to the compiled program. The only change to an existing
library implementation module is ExecWithin.loop_potential in
Complexity/Computability/WordRAM/Structured.lean. It is a loop rule with a potential function
that bounds the total cost of all iterations. The aggregators (Complexity.lean,
abstracts/ComplexityAbstracts.lean) and references.bib also change.

Files under Complexity/Algorithms/WordRAM/Dijkstra/:

• Statement: the problem (Instance, dist, maxWeight, encodeDist).
• HeapStatement, ListEncode: the adjacency-list input layout, LogLinearSpec and
  LogLinearStatement.
• Invariant: Dijkstra's invariant on the abstract distances.
• ExactNotation, HeapProgram: scoped syntax for exact-basis structured code, and the program.
• BinaryHeap, HeapSift, HeapRelax: correctness and cost of the heap and the relax step.
• LogLinear: the main theorem.

Abstract. abstracts/ComplexityAbstracts/DijkstraAbstract.lean states dijkstra_logLinear
with its own graph, distance, input and output layout, word-size condition and machine. Apart from
Runs, its machine definitions are those of WordRAMAbstract. #check_abstract passes with no
allowlist (218 root declarations, 229 dependencies). DijkstraBridge.lean proves that the
abstract's distance is the library's and that the abstract's machine runs as Cslib.WordRAM over
the exact basis. It then applies logLinearStatement.

Syntax in the bridge's imports. The bridge imports LogLinear, whose imports include
ExactNotation and Computability/WordRAM/Notation. These declare the syntax the programs are
written in. With the scoping commit, all their syntax rules, macro_rules and tactics are
scoped: Notation's to Cslib.WordRAM, and ExactNotation's (ram_exact[,
ram_exact_block%, ram_exact_stmt%, ram_exact_eval) to Cslib.Algorithms.WordRAM.Dijkstra.
Only the syntax category wramStmt and the syntax abbreviation wramBlock stay global, because
Lean has no scoped form for them. Outside those namespaces wramStmt has no rules, so they parse
nothing. DijkstraAbstract.lean opens neither namespace. A scan of the bridge's import closure
finds no other global syntax, macro_rules, elaborator or unification hint from these files.

Tests. ComplexityTests/WordRAMDijkstra.lean (in the test library's glob) checks:

• a three-vertex graph with a parallel edge and a shorter two-edge path: its input encoding and
  the word-size condition at w = 10;
• logLinearSpec applied to that graph: the run halts within 230 · 5 · 2 steps and the source's
  output cell holds 1;
• the interpreter on that graph: it finds the outputs [1, 4, 2] (distances 0, 3, 1) within the
  cost bound of heapDijkstra_spec (decide +kernel);
• the interpreter on a graph with two vertices and no edges: it finds [1, 0] (vertex 1
  unreachable) within the bound 200 · 1 · 2 + 27 of heapDijkstra_spec (decide +kernel).
  There are no named axiom guards: the global audit ComplexityTests/Axioms.lean covers these
  declarations, as for the guards removed in test: drop per-module named axiom guards that repeat the global audit #1004.

Not in this PR (follow-ups).

• The quadratic version (adjacency-matrix input, O(n²) time) and its files.

• Moving ExactNotation, appendCode and execWithin_append to Computability/WordRAM.

• Narrowing the @[expose] public section in LogLinear.

• Splitting HeapSift (863 lines).

• A ROADMAP note.

• Existing notions considered (upstream/main a512b10; CSLib 6ff325e and Mathlib 625d8914, as
  pinned in lake-manifest.json):

  • Problem and distance (Instance, Instance.Vertex, Instance.arrowWeight, Instance.dist,
    Instance.maxWeight, encodeDist): Mathlib's SimpleGraph.dist
    (Mathlib/Combinatorics/SimpleGraph/Metric.lean:206) is the length of a shortest walk in an
    undirected graph without weights, and Quiver.shortestPath
    (Mathlib/Combinatorics/Quiver/Arborescence.lean:105) minimizes the number of arrows.
    Upstream has no weighted graph or shortest-path distance: Cslib.InductiveCounting.Graph
    (Complexity/Algorithms/Reachability/InductiveCounting/Semantics.lean:48) is an unweighted
    Bool edge relation, the Graph of Complexity/Computability/Complexity/Problems/Graph.lean:91
    is an unweighted edge list, and Complexity/Foundations/Combinatorics/SimpleGraph/Metric.lean
    extends Mathlib's unweighted graph metric API. Mathlib's Digraph
    (Mathlib/Combinatorics/Digraph/Basic.lean:48) is an unweighted relation without parallel
    edges. CSLib has none either. So dist reuses Mathlib's Quiver.Path and
    Quiver.Path.addWeight (Mathlib/Combinatorics/Quiver/Path/Weight.lean:48) on the quiver
    whose arrows are the edges (Dijkstra/Statement.lean:67-79), with no new path type.
    maxWeight and encodeDist are this problem's size parameter and output convention.
  • Input encoding (ListInstance with lightest, toInstance, dist, m, maxWeight,
    offset, encode, outAddr; ListInstance.dbase): the input is a List ℕ placed by
    upstream's State.init, as for every upstream word-RAM program. Upstream has no adjacency-list
    encoding of a weighted graph; its graph encodings (the adjacency matrix of USTCONBridge, the
    edge list above) carry no weights. toInstance maps the lists to the weight-matrix
    Instance, so the distance is defined once.
  • Invariants and heap predicates (decodeDist, Instance.relax, Instance.Inv, edgeWord,
    edgesWord, heapKey, HeapShape, Ordered, UpOrdered, DownOrdered, HeapInv, and in
    LogLinear distOf, visitedOf, remaining, potential, OuterInv): invariants of this
    proof. The heap predicates describe three arrays in raw word-RAM memory (ℕ → ℕ). Upstream has
    no word-RAM binary heap: Complexity/Computability/WordRAM/Heap.lean is a footprint and frame
    calculus for memory, Complexity/Algorithms/WordRAM/VanEmdeBoas/ is a van Emde Boas tree with
    its own layout, and Queue and Stack are FIFO and LIFO. Batteries' BinaryHeap
    (Batteries/Data/BinaryHeap/Basic.lean:13) is a max-heap held in a Lean Array, not a
    predicate on machine memory. Its decreaseKey (Basic.lean:185) takes a heap index, and it
    keeps no position array from vertex to index, which Dijkstra's decrease-key needs.
  • Programs and register names (swapCode, siftUpBody, siftUp, siftDownChoose,
    siftDownSink, siftDownBody, siftDown, extractMin, pushNew, edgeBody, relaxEdges,
    heapRound, heapSetup, heapDijkstra; the 27 HeapReg abbrevs): the programs are
    Code .exact 27 values written in ram_exact[…]. The abbrevs name registers as elements of
    Fin 27, as upstream's word-RAM programs do (for example
    Complexity/Computability/WordRAM/PackedCount.lean:46-54 and
    Complexity/Algorithms/WordRAM/VanEmdeBoas/Program.lean:65-69).
  • appendCode: runs one structured program after another, nesting the Code.seq chain to the
    right as ram[…] nests it. Upstream has Code.seq and the notation, but no function that
    appends two Code values. Moving it to Computability/WordRAM is a listed follow-up.
  • LogLinearSpec, LogLinearStatement: the nearest upstream notions are
    Program.ComputesInTime (Complexity/Computability/WordRAM/Function.lean:61), whose program
    returns one word f a with halt, and Program.Answers and Program.DecidesInTime
    (Complexity/Computability/WordRAM/Time.lean:70, :196), which return one bit. The output
    here is n memory cells, which neither can state without packing them into one word or running
    once per vertex. The spec is built from upstream's Runs, step, Fits and State.init, and
    LogLinearStatement quantifies over programs as UniformComputableInTime does over
    Program.ComputesInTime (Function.lean:81).
  • The abstract's restated model (Graph, IsWalk, dist, numEdges, maxWeight, offset,
    encode, outAddr, encodeDist, AluOp, Instr, Program, State, Outcome, step,
    init, Runs): restated because upstream's abstract rules ask for it. Every public reference
    in an abstract must resolve to the abstract itself, a background library or an allowlisted
    module (.agents/skills/lean-abstract/SKILL.md:34-39), and problem definitions stay in each
    abstract, with only ComplexityAbstracts.Encoding and ComplexityAbstracts.Computation
    shared (:50); neither has a word RAM. Apart from Runs, the machine definitions are those of
    WordRAMAbstract. DijkstraBridge proves the correspondence with the library; its helpers
    WalkLaws, walkDist, haltsVia and stateOf serve only that proof.
  • Upstream's advisory parallel-definition notice: scripts/parallel_defs.py, run locally on
    this branch built at 1c0567e, with --base upstream/main (932e1bf), reports no candidate
    parallel definitions among the 102 examined declarations.

Validation and review

Tested revision: 1c0567e, which merges upstream/main f86ebad through #1091's head ae590c4.
git merge-tree --write-tree against upstream/main 932e1bf shows no conflict.

CI: fork CI (Lean Action CI) on 1c0567e passed:
https://github.com/orbitingflea/complexitylib2/actions/runs/40449722655

Local checks (LEAN_NUM_THREADS=2) at 1c0567e, all passed:

• scripts/check.sh (all six steps: build, mk_all --check, test, lint, lint-style,
  checkInitImports);
• python3 -B scripts/check_hygiene.py --check-simp, python3 -B scripts/check_tidy_surface.py,
  python3 -B scripts/check_changed_files.py --base upstream/main;
• lake build --wfail --iofail ComplexityAbstracts.DijkstraAbstract ComplexityAbstracts.DijkstraBridge;
• python3 -B scripts/build_abstracts.py --check (this PR adds no catalogue entry: 19 abstracts,
  29 headline theorems, as on upstream/main);
• python3 -m unittest discover -s scripts -p 'test_*.py' (353 tests, 7 skipped) and
  python3 -B -m unittest discover -s scripts -p 'test_*abstract*.py' (80 tests, 4 skipped);
• #print axioms for dijkstra_logLinear and logLinearStatement:
  [propext, Classical.choice, Quot.sound]. No sorry, new axiom or native_decide.

Review (all by AI agents):

• Earlier AI agent reviews of fork revisions (aff3d3a and later) led to the cut to the
  log-linear proof, a trimmed problem file, the tests, a complete syntax comment in the bridge and
  fixes to the abstract's wording.
• Final round, on 5768c1f: two independent AI agent reviews (Codex gpt-6.1-sol and Claude Opus
  5.5) found no code or mathematical blocker. Both asked for this description to quote the source
  and map it to the Lean statement, and Claude Opus 5.5 asked for an accurate AI disclosure.
  Codex asked for an accurate account of the cost proof. Claude Opus 5.5 also listed small code
  points. Revision b0e071e resolved them: ListEncode uses Mathlib's Fin.sum_univ_def
  instead of a private copy; execWithin_append is stated for any basis and register count;
  Invariant no longer sets backward.isDefEq.respectTransparency; the abstract's sentence on
  WordRAMAbstract now names Runs as the one new definition; and the edgeless test above was
  added. The description gained the source paragraph, the cost account and the AI disclosure.
• Third reviewer, on b0e071e: an independent AI agent review by Gemini 4 Argon
  (gemini-4-argon-high), verdict ready. Its non-blocking points: six Dijkstra modules lacked the
  ## References section of upstream's file template, Statement imported
  Complexity.Computability.WordRAM.Time without using it, and the public helper surface is
  large.
• Confirmation round, on b0e071e: Codex gpt-6.1-sol and Claude Opus 5.5 re-checked the branch and
  found the code clean. Their remaining points were all on this description: the existing notions
  considered, a verbatim source quotation for the bound, and the upstream hash.
• Changes since b0e071e, covered by the final confirmation below (5b25940, 3008f30, 1edeec0):
  • the six modules gained ## References (citing Dijkstra1959 and CLRS2009; ExactNotation
    points to the ram[ notation and Algolean2026);
  • the import of Complexity.Computability.WordRAM.Time moved from Statement to
    HeapStatement, whose LogLinearSpec uses it; Statement now imports
    Mathlib.Data.Fintype.Prod and Complexity.Init instead;
  • siftDownBody is defined from the new public siftDownChoose and siftDownSink, which
    replace the private copies chooseCode and sinkCode in HeapSift;
  • this description gained the existing notions considered, the quotation from Erickson and the
    current upstream hash.
    The public helper surface is listed above as a follow-up (moving appendCode and
    execWithin_append, narrowing the public section of LogLinear).
• Final confirmation, on 1edeec0 and this description: independent AI agent reviews by Codex
  gpt-6.1-sol (ready), Claude Opus 5.5 (ready after fixes to two line locators in this
  description) and Gemini 4 Argon (gemini-4-argon-high; ready). Their points on this description
  are applied here: one locator fixed (the other was already correct), and wording on the
  graph-metric file, Digraph and Batteries' decreaseKey.
• The reviews above covered revisions up to 1edeec0. The upstream merge and the port
  (d5cde69, eb3db42, af762a7): independent AI agent reviews by Codex gpt-6.1-sol, Claude Opus
  5.5 and Gemini 4 Argon (gemini-4-argon-high), all ready. Their non-blocking points are applied in
  1c0567e: the bridge's module doc now names step_matches_at and programOf, the rand case
  of execWithin_append names its fields dst src as upstream does, and this description gives
  HeapSift's new length. 1c0567e changes only that comment and those binder names.
• No human has reviewed this PR yet.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: no existing
  abstract or catalogue entry changes. This PR adds DijkstraAbstract and DijkstraBridge to
  ComplexityAbstracts.lean. It adds no catalogue.json entry and no README row. Whether the
  result is a headline is left to the maintainers.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): AI agent
  reviews only, as listed above (fork revisions aff3d3a and later; final round on 5768c1f;
  Gemini 4 Argon and the confirmation round on b0e071e). The theorem statement
  dijkstra_logLinear has not changed since those reviews. Revision b0e071e changed one sentence
  of the abstract's introduction (the WordRAMAbstract comparison above). After it, only
  eb3db42 and 1c0567e changed a file of this PR under abstracts/: DijkstraBridge.lean, for
  the upstream merge (see Change) and its module doc; DijkstraAbstract.lean is unchanged. No human review yet.
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: CI
  does not render the abstract because it is not in the catalogue. An AI agent rendered it
  locally with scripts/build_abstracts.py (render_entry on an in-memory entry) at 2419d5a
  (6 pages). That render was not rerun at 1edeec0, where one sentence of the introduction differs.

AI assistance

Written with Claude Code (Claude Opus 5.5), under Renfei Zhou's direction. Claude Code wrote the
Lean code, the proofs and this text. All reviews listed are AI agent reviews; no human has reviewed
this PR yet.

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[SamuelSchlesinger]

reviewer-jetski-5208-1098 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 1c0567ee177866fafbbeec56da89d20e30e894e9

Thank you, Renfei, for a careful first contribution. The development is well structured and the PR description is unusually thorough.

What is proved. logLinearStatement and the abstract's dijkstra_logLinear give one word-RAM program over the exact basis (27 registers) and one constant K with the following property. For every directed graph on Fin n with natural-number weights (parallel edges and self-loops allowed), given as adjacency lists with n + 1 offsets, every source s, and every word size w with 8 (n + m + 2) (W + 2) < 2 ^ w, the program halts after at most K (m + 1) (⌊log₂ n⌋ + 1) instructions, halt included. Each output cell outAddr v then holds encodeDist (dist s v). Memory past the input starts at zero, and the input is placed in memory for free. That is why the bound has no separate n term. The PR states this convention honestly, and it is the standard RAM convention. The word-size condition makes w = O(log (n + m + W)), which is enough for the largest finite distance (n - 1) W.

Abstract against the sources. I checked the following, and found no mismatch:

• DijkstraAbstract's machine (AluOp, AluOp.eval, Instr, State, Outcome, step, init) matches WordRAMAbstract text for text.
• IsWalk/dist (the infimum over walks in ℕ∞, ⊤ when no walk exists) correspond to the library's ListInstance.dist (the lightest-edge weight matrix with Quiver.Path.addWeight) through walkDist_eq.
• numEdges, maxWeight, offset, encode and outAddr match ListInstance definitionally.
• The abstract's quantifiers (∃ r p K, ∀ n G s w) match LogLinearStatement.
• #check_abstract runs under #guard_msgs with no allowlist. CI builds and audits it through ComplexityTests/Abstracts/All.lean.

The bridge's port to Code.rand/programOf (isRandFree_of_step, then upstream's step_matches_at) looks right. No existing abstract or catalogue entry changes. The PR adds no catalogue entry, so CI does not render the abstract. In my view the result plausibly meets the headline bar (explicit model and encoding, satisfiable hypotheses, an honest bound), but promoting it is an editorial decision for the maintainers.

Checked instance. In the test graph (n = 3, m = 4, W = 5), encode has 14 = n + 2m + 3 words at addresses 1..14, so outAddr v = 15 + v is the first cell past the input. The word-size condition is 8·9·7 = 504 < 2^10. The interpreter finds [1, 4, 2], that is, distances 0, 3, 1. In the edgeless test, [1, 0] correctly encodes an unreachable vertex. Edge cases: for n = 0 the statement is vacuous, since Fin 0 has no source, and for n = 1 the bound is K (m + 1).

Other checks.

• Sources. I checked the Dijkstra (1959) quotations against the linked scan and the Erickson p. 288 quotation against the linked PDF; both match. I did not consult CLRS.
• Hygiene. No sorry, axiom, native_decide or heartbeat overrides. The only set_option is a linter switch inside the ram_exact_eval macro, and [simp] is used only on the decodeDist/encodeDist round-trip lemmas.
• Reuse. The new syntax is scoped, as described. ExecWithin.loop_potential is the deterministic counterpart of the existing ExecRandWithin.loop_potential, not a duplicate. I found no parallel definitions.

Stacking. This branch contains #1091's head ae590c40 unchanged; Notation.lean is identical to that head. #1091 has its own agent approval at that SHA, so land #1091 first, or together with this PR. ci-checks is green at 1c0567ee177866fafbbeec56da89d20e30e894e9, and GitHub reports the branch mergeable.

Non-blocking requests.

• There is no linked issue. Please open a tracking issue, or ask a maintainer to, that records the follow-ups listed in the description: the quadratic version, moving ExactNotation/appendCode/execWithin_append into Computability/WordRAM, narrowing LogLinear's @[expose] section, splitting HeapSift, and the ROADMAP note. A PR description alone is not a durable record for them.
• Small nits are inline.

Limits of this review. I did not build locally; I relied on the green CI at this head. I read every public statement and definition, the abstract and the bridge in full, but only sampled the heap and relax proofs (HeapSift, HeapRelax, BinaryHeap), whose correctness Lean checks.

[SamuelSchlesinger]

nit: The PR description quotes Erickson, Algorithms, §8.6, p. 288, for the O(E log V) binary-heap bound, but says CLRS could not be consulted, and the references here cite CLRS only. The CLRS locator is right: 3rd ed., §24.3 analyses the binary min-heap version as O((V + E) lg V). Still, you could add an Erickson2019 key to references.bib and cite it here and in HeapStatement/LogLinear, so that the reference you actually checked appears in the abstract.

[SamuelSchlesinger]

nit, follow-up: appendCode and execWithin_append are basis-generic facts about structured Code, with nothing specific to Dijkstra. You already list moving them to Computability/WordRAM as a follow-up. Please record that in an issue, naming these two declarations and ExactNotation, so it doesn't get lost. It doesn't need to happen in this PR.

[SamuelSchlesinger]

nit: This docstring could state the result itself: from .init G.encode, the structured program reaches a state with the encoded distances in the output cells, within 200 (m + 1) (⌊log₂ n⌋ + 1) + 27 instructions, at every word size satisfying the condition. The module docstring already says this, but the declaration's hover text currently gives only the title.