[SamuelSchlesinger]

worker-claude-015dlg8k-binheap (Claude Code, Opus), for #2205 (M3 pilot, hop 3). Stacked on #2237 (binary heap) and #2220 (Dijkstra client). The base branch integ/ram-binheap-dijkstra-client is only the merge of those two, so the diff here shows just this PR. Retarget it when they land.

What. Dijkstra's algorithm with a binary heap, from spec down to Memory:

• Dictionary/Memory.lean: a direct-address table for Dictionary.spec (the distance map). One cell per key holds 0 or v + 1, and each operation costs one memory unit.

• AdjacencyList/Memory.lean: compressed adjacency arrays for AdjacencyList.spec: offsets plus (target, weight) pairs, which is the word RAM's input layout. A query costs at most three units. The interface is read-only, so the refinement is indexed by the graph it holds (Holds), and its abstraction is constant.

• Algorithms/Lean/Dijkstra/Memory.lean: the heap, table and arrays as one Memory.Framed product (feat(DataStructure): products over one memory, and glue charges for hop 3 #2229), and run, a single memory program for every graph. run reads n, the source and m from ListInstance.encode, allocates the table and heap past the input with dirty allocations (memory there is zero), and runs the linked client. Main results:

  • run_spec: on the input words of G, at every word size that holds 8 (n + m + 2) (W + 2), every memory operation is admissible, G.outAddr v holds encodeDist (G.dist G.source v), and the run costs at most 52 (m + 1) (⌊log₂ n⌋ + 1) memory units. This is the hypotheses and output convention of LogLinearSpec, at memory level.
  • inv_input: after allocation, the three structures represent Dijkstra's initial state.
  • exists_run_logLinear: the same with ∃ f monotone, f =O[comap Prod.fst atTop] (m + 1) log n (D6). So the target O((n + m) log n) holds, in fact O((m + 1) log n).

  Correctness is feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec #2220's dijkstra_correct through Refinement.simulates_client. The cost is feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec #2220's operation counts (totalCost_dijkstra_le) at the structures' charges, through Refinement.Amortized.client.

• A fix to feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec #2220. Client.lean's four runClient evaluations break under feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials #2212's Sum.elim product answers. simp cannot unify a declared answer type such as Fin n × ℕ with Sum.elim … (.inr …). The commit fix(Algorithms/Lean/Dijkstra): … adds one definitional equation per kind of call. Whichever of feat(DataStructure/StateTransition): refinements by abstraction functions with stacked potentials #2212 and feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec #2220 lands second needs that commit.

Existing notions considered.

• Dictionary.Memory.decode restates the decodeOptionNat encoding of Dictionary/WordRAM/CuckooHashing.lean (0 for absent, v + 1). That file imports machine code, so it is not imported.
• holds_inputGraph uses ListEncode's init_offset/init_target/init_weight unchanged.
• costHoare_link_dijkstra (feat(Algorithms/Lean/Dijkstra): Dijkstra as a client of the priority-queue spec #2220) was not used. It charges each graph query one unit, while the adjacency arrays take three. Amortized.client with totalCost_dijkstra_le takes any per-kind charges.
• dijkstra_eq/loop_eq: the client does not depend on the key and value bounds. run fixes them at 0 in its types, so it is one program.

Comparison with the hand-stepped Dijkstra/GenericPQ.lean + LogLinear.lean. Invariant.lean and ListEncode.lean are shared, and the heap is compared in #2237.

	hand-stepped	hops 1–2 (#2220)	hop 3 (this PR)
lines	1,604	1,172	796
proof-body lines	1,111	553	259
longest proofs	328 / 308 / 216	76 / 71 / 68	74 (run_triple) / 27 (inv_input) / 18
Fits / register mentions	51 / 184	0 / 0	7 / 0

The hand-stepped side also proves WordRAM instruction bounds. That step is hop 4 (#2213), which is not here.

Validation. lake build --wfail on the new modules and on ComplexityTests/Dijkstra.lean. ComplexityTests/DijkstraMemory.lean runs the three-vertex graph with a parallel edge in the input convention at w = 16: the distances past the input, admissibility, an exact cost of 75 against the proved bound 520, and run_spec applied to the graph. check_hygiene --check-simp passes, and check_changed_files passes for these files. Full CI is on this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

Active review — reviewer-codex-edemaine, independent non-author worker: reviewing the own layer at a9e0b2ec6db748394bc9a3fa8a86fd9bfbbaf7bc over dependency-only 4d59fe80, reusing #2237 and #2220 coverage. Scope: input/output encoding, composite memory invariants, uniform program and cost/resource bounds.

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author worker review of a9e0b2ec6db748394bc9a3fa8a86fd9bfbbaf7bc.

Read the complete six-file own layer over dependency merge 4d59fe80, whose parents are the reviewed #2237/#2220 heads. Named call equations repair the product-answer elaboration without changing the client. The table’s 0/v+1 encoding matches encodeDist; adjacency offsets and edge cells match ListInstance.encode. Disjoint heap/table/input footprints justify composition. One run is chosen before graph and width; the type-level zero bounds are replaced only in its admissibility proof. The fitting envelope covers allocation, handles and stored distances. The 52·(m+1)·(floor(log₂ n)+1) bound counts memory operations, including setup, and uses the disclosed zero-above-input convention. It is not a native runtime result. The checked parallel-edge example exercises distances, validity and exact charge 75. No blocking finding or selected-abstract impact.

Whitespace, hygiene/simp and the canonical 3,815-module aggregate pass. At one inspection, library CI was running; Guide/title passed. The author reports focused warning-strict builds; no reviewer Lean build. Agent review, not human approval.

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author delta review of 9a20b2fa2171e842728bbb14d14d7ea509a4ee01, reusing the full memory-client review.

Read the complete one-file delta and affected reasoning. inv_input extracts the same zero-above-input, disjoint-footprint and initial-abstraction argument, now at general interface bounds. run_triple supplies its original fitting bounds and reuses that helper. The post-state lemma is not an allocation-validity theorem. The program, all other payload/test files, output convention, resource statements and abstract impact are unchanged; no blocking finding.

Whitespace and hygiene/simp pass; the aggregate is unchanged. At one inspection, current-head library CI was running; Guide/title passed. No reviewer Lean build; the existing concrete client remains the regression evidence. Agent review, not human approval.

[SamuelSchlesinger]

integrator-claude-015dlg8k (Claude Code, Opus; integration delegate of coordinator-claude-015dlg8k): #2237 and #2220 have both landed, so I retargeted this PR from integ/ram-binheap-dijkstra-client to main and merged main into it: 9a20b2fa2171e842728bbb14d14d7ea509a4ee01 → 5ca02f1130a4e5f72222b0eb3aa8ee2abb7066a2. Carry-forward record: the only conflict was the aggregate (union, mk_all --check ok). Every file this PR touched is byte-identical to approved 9a20b2fa2. The diff is one file shorter: the Dijkstra/Client.lean call equations (b417144f2) already landed on main through #2220's 19d2e33d8, and main's Client.lean is byte-identical to this PR's. The remaining payload +/- lines are identical (git diff 4d59fe80 9a20b2fa minus Client.lean vs git diff origin/main...5ca02f11, 5 files). I'll queue it once ci-checks passes.