run_id: phase3-run-002 · date: 2026-06-11 (UTC) · trial: thread B — merged work reused as an importable dependency.
Machine record: phase3-run-002.json.
The exit metric is: did merged work get reused as an importable dependency — a proof that imports an Unsorry.* module and uses its lemma?
MET. PR #154’s module proves the triangular closed form ∑_{i≤n} i³ = (n(n+1)/2)² like this — in full:
import Unsorry.NicomachusSumCubes
import Mathlib.Algebra.BigOperators.Intervals
theorem sum_range_cube_eq_triangular_sq (n : ℕ) :
∑ i ∈ Finset.range (n + 1), i ^ 3 = (n * (n + 1) / 2) ^ 2 := by
rw [nicomachus_sum_cubes (n + 1), Finset.sum_range_id, Nat.add_sub_cancel,
Nat.mul_comm (n + 1) n]
The first rewrite is nicomachus_sum_cubes — the swarm’s own phase-2 lemma (#133), invoked, not re-derived. “Every merged lemma makes the next one cheaper” was the README’s headline aspiration; this is the first time it happened by mechanism.
| Dimension | Value |
|---|---|
| machinery + seeded dep edge | ADR-014, PR #153 (merged 05:20:25Z) |
| claim → proved | 4 min 57 s, first attempt (fable, pre-ladder static max) |
| proof size | one 4-step rw |
| reuse PR | #154 (merged 05:35:08Z) — seed-to-merged in 15 minutes |
| binding held | yes (gate-a regenerated obligation green) |
| reuse edges, this run | 1 declared (triangular → nicomachus-sum-cubes) |
| reuse edges incl. run-001’s recompositions | 5 (each recomposing parent imported its own proved subs via the same surfacing) |
proved-deps resolves a goal’s declared deps≜⟨…⟩ plus its own decomposition’s subs through the library index (the authoritative proved marker) to their declaring modules; run_proof appends a PROVED DEPENDENCIES section to the prove prompt — import lines with statements — and amends the import-tightness rule to allow exactly these. Advisory only: the prover may ignore it, and the kernel, axiom audit and binding gate judge the result identically either way. Soundness never depends on the hint.
The corroboration matters as much as the headline: run-001’s four recompositions are four more reuse instances of the same mechanism — each recomposing parent (s1-s1, s2, s1, the root) imported its proved subs rather than re-deriving them. Reuse is now how the chain closes, not a special case.