Aristotle runs: submissions, ids, and collection state

The proof-agent adapter's durable ledger (lean/proof_adapter.py; contract in docs/26 §4). Every submission is recorded here with its project id so any later session can collect. The rule stands: whatever comes back is input, it counts only after the static refusal scan and a zero-sorry lake build on this repository's toolchain. Aristotle's own verification claims are never copied into this file.

Collect with:

source ~/.zshrc   # ARISTOTLE_API_KEY
.venv-tools/bin/python -c "
import sys; sys.path.insert(0, '.')
from lean.proof_adapter import collect_from_aristotle
print(collect_from_aristotle('<project_id>', destination='/tmp/aristotle'))"
# then, for each returned .lean file:
.venv/bin/python lean/proof_adapter.py check <file.lean> <ModuleName>

Batch 1, Sturm-track calibration (submitted 2026-08-12T00:08-0500)

Four bounded lemmas in Mathlib vocabulary, graded easy → hard, chosen from the Mathlib upstream track (ROADMAP.md, "The upstream track": Sturm is the contribution target). Purpose: calibrate what Aristotle-hours buy at each difficulty grade before spending them on the real chain. Prompts pinned in the table; every prompt required zero sorry/admit/axiom/ native_decide and forbade weakening the statement.

Expected turnaround: hours (the Grasshopper case study measured ~8 for a hard problem; A and C should be far faster). Update the status column at collection: collected, accepted, collected, refused (<reason>), or no output. A refused artifact's reason belongs here verbatim; do not resubmit the same statement without changing something and saying what.

Note: a fifth project (0701719a-…, description "lean", created 2026-08-12T04:55Z) predates this ledger, it is the operator's own dashboard test, not adapter-submitted, and is not tracked here.

Batch 2, the zeta23ext port (submitted 2026-08-12T15:01-0500)

Purpose: make zeta23ext assemble. The package's modules were proved service-side against an older Mathlib and had never been built against the pin they must integrate under. Measured here first, module by module, against the already-compiled Mathlib v4.33.0-rc2 in lean/ (drop the module in as a scratch target, build, delete) rather than buying a round-trip to find out. That measurement is what the prompts carry.

Result of the local survey, which is the reason this batch is three projects and not four:

Prompts pinned at ~/.claude/jobs/8633dae1/tmp/prompts/ for this session; each required zero sorry/admit/axiom/native_decide and forbade weakening or restating any theorem, proof bodies only.

A defect found by the survey, independent of the port. All eight BandCert/ modules as committed carry import RequestProject.X: the proving service's own project-local module namespace, while Zeta23Ext.lean imports Zeta23Ext.BandCert.Main. The package therefore could not have assembled at any pin: the first lake build dies on an unknown module, before any mathematics is reached. Nothing about the proofs is wrong; the artifacts were landed without their import paths rewritten, and no local assembly had ever been attempted to notice. The rewrite is mechanical (RequestProject. → Zeta23Ext.BandCert.) and is folded into port-C's prompt rather than done blind here, so one artifact carries both.

Batch 2 collection (2026-08-12, same day)

All three returned within hours. Two accepted, one refused and repaired locally; the split is the reason the local kernel check exists.

Phi.lean was repaired locally, not submitted. With Leaves ported, the chain's next module failed at 13 sites, all one shape: projection-through- definition ((a.add b).1 vs a.1.add b.1) that the newer simp no longer unfolds. A uniform fix, naming the CIv operation in each simpa set, plus three ofR/AIV sites, cleared all 13. Cheaper to do than to describe in a prompt.

The whole BandCert chain now builds under v4.33.0-rc2: 8 modules, 8704 jobs, Verify alone taking 1513 s. Zero sorryAx anywhere in the log; cap_le_slack and f_nonpos_off_bands report only the three standard axioms.

What this cost, and the lesson. Two of three service artifacts were correct as delivered; the third was confidently wrong in a way its own verification could not have detected, because its environment could not build the target. The refusal scan plus a local kernel check on this machine is what separated them, exactly as proof_adapter.py was built to do. Aristotle's self-report was honest about its limitation and still shipped a non-building artifact, that is the failure mode to keep expecting.

Batch 3: Bridge and the last assembly blocker (submitted 2026-08-12, sprint 3)

bridge-A accepted, and note what its acceptance did NOT rest on. Its summary carried the same caveat that produced a refusal in batch 2, it could only build against v4.28.0, not the target pin. The local check under v4.33.0-rc2 passed this time: all three theorems build, each reporting only [propext, Classical.choice, Quot.sound]. Same caveat, opposite outcome, which is exactly why the caveat is not the decision procedure and the local kernel check is.

One structural change it made and flagged: the definition block is wrapped in a noncomputable section, because Real.sqrt has no executable code and Wmat would otherwise be rejected by the compiler IR check. Definition texts are unchanged; no statement weakened.

What is still owed on Bridge. It is landed as Zeta23Ext/Bridge.lean carrying its own copies of rtrace, frobSq, Wmat, Pmat, xsq, that is what made it provable without the dependency. The point of the module is to sit on upstream's objects, so replacing those local copies with import Zeta23 and re-checking is an outstanding step, not a finished one. BRIDGE-SPEC.md §1 lists each definition against its upstream source line for exactly that swap.

Batch 4: the k=1 retention reduction (submitted 2026-08-12/13)

The 2026-08-12 closure (f39dc49, corrected to k=1 only by 7df6ed8, defect #19) states its reduction is "algebra on two sorry-free theorems already in the tree". This submits exactly that algebra, so the step moves from hardened grade to kernel-checked.

Stated over abstract reals on purpose. Aristotle does not have this package's EForm3 modules, and the reduction needs none of them: both retention_gap and energy_F enter as hypotheses of the submitted lemmas rather than as facts to be reproved. That makes the file self-contained against Mathlib alone, and it makes the artifact reusable, the analysis is already sorry-free in the tree, and only the algebra was ever missing.

Composing the two gives the closure's own formula,

margin = (4/A²)·[ Shq(y)/2 − Σ_j D_j + (1/400)·Σ_{j<k} φ_r(x_j−x_k)² ]

which is the statement that the repulsion term is not optional: the weaker route discards it by using n ≤ E[F] in place of the identity, and that route's hypothesis is arithmetically false from n = 8.

Both statements were checked numerically before submission (2000 random instances each, margin_eq and energy_sub_card both exact), because a wrong statement costs a multi-hour round trip and the ledger already records one submission refuted by the prover for a missing hypothesis.

Batch 4 collection

collected, accepted. Both theorems build here under v4.33.0-rc2, statements byte-identical to the submission, each reporting only [propext, Classical.choice, Quot.sound]. Static scan clean. Landed as Zeta23Ext/RetentionAlgebra.lean.

energy_sub_card rests on one private helper, sum_sq_split, which splits the double sum by trichotomy into strictly-upper, strictly-lower and diagonal parts and identifies the two off-diagonal halves through the symmetry hypothesis; the diagonal then collapses under the normalisation.

Its summary carried the same "built against v4.28.0, not the target pin" caveat that preceded a refusal in batch 2 and a clean pass in batch 3. Third occurrence, and the caveat remains uninformative in both directions, which is the argument for the local kernel check being the gate rather than the service's own report.

What this does and does not move. The k=1 retention reduction's algebra is now kernel-checked. The analysis it composes (retention_gap, energy_F) was already sorry-free in the tree, so the k=1 layer's chain is closed end to end at kernel grade. What is untouched: the multi-pair statement of blocker 2 (k blocks at different depths and centres) is still open, per the correction in 7df6ed8 (defect #19). The lemmas here are stated over abstract reals, so wiring them to EForm3's objects, discharging the two hypotheses from the tree's own theorems, is a remaining step, not a finished one.

Batch 5: the EForm3 port (submitted 2026-08-13)

Found by trying to make batch 4 load-bearing. RetentionWired.lean discharges RetentionAlgebra's four abstract hypotheses from the tree's own retention_gap, energy_F, Qre_zero_even and Qre_zero_zero. It cannot be checked yet, because EForm3 itself does not build at the target pin, the fourth module set in this package landed without ever being built there.

Both prompts carry the two failure classes this package's port has already taught us, convert … using 1 leaving an instance-equality goal first, and projection-through-definition no longer unfolded by simp, since a prompt that names the drift gets a normal-form-independent repair rather than another brittle one.

The pattern is now worth stating as a pattern. Four separate module sets (BandCert/, EForm/, PairEnergy, EForm3/) have been landed into this package without a build at the pin they must integrate under. Each time the proofs were fine and the port was a handful of tactic sites. The cost is not the repair, it is that nothing downstream can be verified until it is done: RetentionWired is written and unverifiable purely because of this. assemble.sh exists to make that check one command; it only helps if it runs before landing rather than after.

Batch 5 collection, and batch 6

Both repairs removed the dependence rather than patching the symptom, which is why each fixed several reported sites at once. Taylor replaced every simpa-built HasDerivAt and every convert … using 1; ring with an explicitly ascribed term corrected by HasDerivAt.congr_deriv, so the side goals are plain real identities. ClosedForm replaced convert h using 1; field_simp; ring with refine h.congr_deriv ?_; rw [div_eq_iff hne]; ring, using the nonvanishing hypothesis explicitly instead of letting field_simp pick a normal form. Batch 6's prompt carries both patterns verbatim, since a prompt that names the drift gets a durable repair rather than another brittle one.

Fixing a layer reveals the next. Taylor and ClosedForm landing exposed Numerics, which the earlier survey could not see because the build stopped above it. That is the expected shape of a port and not a new defect, but it does mean "the survey found N sites" is a lower bound until the chain builds end to end.

Batches 5-7: Pub 1 source-admissible strong closure (submitted 2026-08-16)

Twelve bounded lemmas supporting the Lean formalization of hunts/wide_search/RESULTS-xiprime-admissible-closure.md (PR #45). Every prompt fixed the target toolchain (v4.33.0-rc2, Mathlib 51e6992efd06126df61a496bebf8f49482a4e129), required the statement character-for-character, and forbade sorry/admit/axiom/native_decide. Landed files are lean/ZetaLean/Pub1/Aristotle/<tag>.lean, each wrapped in a namespace Aristotle<tag> so they can coexist.

Every artifact was collected, statically scanned, and built here before use. The service's own verification claim is not recorded and was not relied on.

Measured turnaround. Submit-to-collect, per project. These are upper bounds: collection was polled, not instantaneous, so the true service time is at most the figure shown.

All twelve landed inside about 1h25m of wall clock across three overlapping batches. This is the first entry in this ledger with wall-clock actually observed rather than estimated, and it revises the standing "hours" figure down by roughly an order of magnitude: the Grasshopper case study's ~8 h is not what these bounded lemmas cost.

The recurring port defect, worth naming. Five of the twelve failed here for the same two reasons, both version drift rather than mathematics: norm_num with the interval-integral simp set no longer evaluates a polynomial definite integral (fixed by an explicit antiderivative plus intervalIntegral.integral_eq_sub_of_hasDerivAt), and simpa normalizes a lambda into Pi.mul/Function.comp form that then fails to unify. Prompts for future batches should ask for HasDerivAt.congr_deriv and explicit .mpr applications in preference to simpa/convert.

Prompts are pinned in the private operating repo at fulcrum/records/aristotle-prompts/pub1/ (the prompt corpus is the private side of the boundary; the statements themselves are public, in the .lean files).

Batch 8: Pub 1 analytic obligations (submitted 2026-08-16, later same day)

Seven further bounded lemmas aimed at removing the four analytic assumptions recorded in lean/ZetaLean/Pub1/OBLIGATIONS.md. Same rules as batches 5-7, and the prompts now carry the porting notes distilled from those batches (explicit antiderivatives instead of norm_num on interval integrals; congr_deriv instead of convert; no simpa on lambdas). That guidance paid: all seven ported unchanged, against seven of twelve in the previous round.

What N bought, and why it matters. The informal chain says F₁'' = 2δ₀ + q, and Mathlib has no convenient distributional-derivative API for this kernel. Rather than build one, N differentiates the split integral twice and recovers the delta mass as the sum of two moving-endpoint boundary terms. The coefficient 2 is then a theorem, not a convention: it is 2 f'(0) with f'(0) = 1 proved separately in S. This is the cheaper route by a wide margin and it is the one the operator prompt suggested.

Measured turnaround (submit to collect, upper bounds; collection was polled): N, O ~55 min and ~20 min; R ~35 min; S ~65 min; T ~75 min; U ~85 min. The two series-analysis targets (S) and the product-rule/L¹ target (T) were the slow ones, consistent with batch 5-7 where the series work also ran longest.

Prompts are pinned in the private operating repo at fulcrum/records/aristotle-prompts/pub1/.

Batch 9: Pub 1 analytic closure, second pass (submitted 2026-08-16)

Six lemmas aimed at the two remaining critical paths. Prompts carried the porting notes from batches 5-8.

Why J2 and TU2 exist at all. Batch 8's J, T, U asked for C² on a neighbourhood of the closed interval. That hypothesis is unsatisfiable: w'' jumps by 2w(±1/2) ≥ 2/5 at the endpoints, because the delta mass contributes inside I and not outside. The theorems were true and uninstantiable. Restated over the open interval with bounded derivatives, they instantiate. The lesson for prompt-writing is to ask for the weakest hypothesis the downstream argument actually consumes, not the most convenient one to state.

Turnaround (submit to collect, upper bounds; polled): V ~40 min, W ~40 min, TU2 ~95 min, J2 ~2 h. Four of four accepted; one needed repair.

Batch 10: Pub 1 assembly closure (submitted 2026-08-16)

One project, and it is the one that mattered: batch 8's R form of the same estimate asked for a minimal bound Bz, which would have needed the sup built as an sInf. Restated as "|z| attains its max on the compact interval, and at that point the equation gives the bound directly", it is a short proof and drops straight in. Same lesson as J2/TU2: ask for the form the downstream argument can actually feed.

This batch completed the development. pub1_strong_closure and pub1_strong_closure_reciprocal are now unconditional.

Prompts are pinned in the private operating repo at fulcrum/records/aristotle-prompts/pub1/.

Batch 11 (not opened): S2, the stability rank-trace lemma (2026-08-23)

No project was created and no API call was made. The entry exists because the ledger's job is to let a later session find out what happened, and "nothing was sent" is a thing that happened.

The formal-native probe of hunts/ainta_seven_point/ARISTOTLE-PROBE.md was authorised to send three bounded variants of Ainta's S2 (the scalar lemma alone, the full theorem, the theorem with the scalar lemma as a hypothesis) under the handoff's rule that only what remains goes to the service. After the local pass nothing remained: the full theorem builds with zero sorrys and standard axioms only, in StableRankTrace.lean (then under hunts/frontier_math/zeta23ext/Zeta23Ext/, moved to lean/bridge/Zeta23Ext/ on 2026-08-23 when the theorem was packaged for Palomar), and the scalar lemma turned out to be an existing upstream theorem (Zeta23.ZeroSide.RankTraceMult.sq_sub_ge_gc).

A calibration project the operator may want, and the reason it was not opened here. The interesting unasked question is whether the service searches the ambient library rather than reproving from scratch. Hand it stable_rank_trace_sharp cold, with Zeta23 importable and with no mention of rank_trace_mult, gc or sum_eigenvalues_comm in the prompt, and measure whether it finds the four-line corollary route or reinvents the fifty-line skeleton. Ground truth is now known exactly, which is the only reason the measurement would be worth anything. It is a measurement about the tool, so it is an allocation call and not this pursuit's to make.

Batch 12 (not opened): the Ainta bridge, S6-S9 and S11-S16 (2026-08-23)

No project was created and no API call was made by any of the five agents. Five agents worked the bridge of hunts/ainta_seven_point/TRUST-MAP.md in parallel from the branch bridge/skeleton, each under a cap of 3 submissions, each keeping its own ledger under hunts/ainta_seven_point/bridge/. The five ledgers are merged here; the per-group files stay in place as the provenance record. Total used: 0 of 15. Every obligation closed by direct proof under the pinned toolchain (leanprover/lean4:v4.33.0-rc2, mathlib 51e6992efd06126df61a496bebf8f49482a4e129, Zeta23 at 3635e74826a4c1fcece7d1cd2b6fa75e43a00510) before a residual existed, and the standing rule (ARISTOTLE-PROBE.md section 7, Batch 11 above) is that a closed target is not sent: that buys a comparison about the tool, which is an allocation call for the owner.

Integration (branch bridge/integrate, same day): the five branches merge cleanly (disjoint files by construction), lake build Zeta23Ext.Bridge.Main from deleted Bridge oleans completes in 44 s wall (8854 jobs; since 2026-08-23 the same tree is a package of its own and the command is cd lean/bridge && lake build, 8860 jobs), zero sorry warnings, and every #print axioms line in the tree, seven_point_bound and seven_point_bound_paper included, reports [propext, Classical.choice, Quot.sound]. The record of what was proved and what remains a hypothesis is hunts/ainta_seven_point/BRIDGE.md.

What was not sent, and why it would still be a measurement rather than a result: the same calibration project Batch 11 describes, now with sixteen ground-truth proofs instead of one. The candidates with the most to teach are S9 kernel_limit (808 lines of helper, the proof that the trust map graded LARGE and that turned out to reuse [L23]'s PrimeSide.rho and the sharp window comparison) and S14 pinching_partition (the one library fact the map called MISSING, proved in 321 lines from the row-stochastic mixture of the spectrum of a principal submatrix). Not opened here; the owner's call.