Measure useful Lean verification yield in ONE job. Maximize distinct whole proof units within normal assigned allowance, not an arbitrary 20-minute cutoff. Proof stages below apply to branches A/B ONLY; final step reconciles evidence without rerunning proofs. This is replication, not new mathematics, final-theorem certification or guaranteed throughput.

Use supplied pinned repo/commit, tree c6111a7d32daf2906275ee1ac265bf6865ebd9a5; leanprover/lean4:v4.35.0-rc2 (Lean source 11acb17ec6b07a8f9e9173e6845197929540936b). Authenticate official toolchain asset and record binary hashes. Preserve mathematics/pins and compare consumed bytes to Git blobs, not just index status. Target only required closures (public import/import all included), no full Solution/Mathlib build. Preserve flags -j1 -DElab.async=false. Cache only locally built, source/toolchain/flags/output-hash-bound objects. Replay input is reference code only: inspect/harden its authentication, audit/parser/exit handling, generalize targets and replace its fixed 1200-second cutoff with safe remaining assigned budget. No new checker-toolchain/framework build.

Finite backlog:85 complete chunks+2 replacements=87 units. N=SpectreFinite.HexSearch.RadiusFive. with trailing dot. Locate actual declarations:

(a) Nroot{r}Node0Step1Chunk{r}_{j}_checked, r in {0,1,4,5,6,7,8}, j=0..5;

(b) Nroot0Node0Step2Chunk{k}_{j}_checked, k in {5,6,7,8}, j=0..5;

(c) Nroot0Node0Step3Chunk5_5_checked and Nroot0Node0Step3Chunk{k}_{j}_checked, k in {6,7,8}, j=0..5;

(d) SpectreFinite.HexSearch.RadiusThree.root2Node0Step4_checked in SpectreFinite.RadiusThreeRoot2Part1; Nroot7Node110Step1_checked in SpectreFinite.RadiusFiveRoot7Part43.

Never invent matching names. Each chunk includes its exact published parent type, referenced slices and row-binding theorem composing checkNarrowing_flatten; validate scope/row order/domains. root0Node0Step2Chunk5_1_checked and root0Node0Step3Chunk5_5_checked alias *_projected_slices_pilot_checked: include the actual intermediate and *_projected_sliceN_checked supports. Totals:381 slices,85 row bindings,2 intermediates,555 unique unit/support roots. Supports/dependencies are not extra units. Each replacement is one unit.

Canonical order:Root8 step1 chunks8_2,8_0,8_1,8_3,8_4,8_5; small replacement; stress replacement. First three parents use SpectreFinite.RadiusFiveRoot8Part0Segment03, next three Segment04. Thereafter minimize (additional module count,additional source bytes,source-path ASCII,line,full declaration ASCII) relative to the union of earlier SCHEDULED closures. Filter by branch ownership; keep order despite failures, logging blocked entries and continuing viable successors. Branches may finish in any order.

First obtain actual compile/exact-type/transitive-axiom results for one assigned COMPLETE unit, before optional tooling. Audit all its roots with autoImplicit=false and reject kernel bypasses. Save results, then extend warm same-module cohorts while safe budget remains. Do not stop at an easy seed if further work fits. Export small cohorts, interleaving breadth/depth; give the first completed unit each available checker tier. Do not chase missing tools, one stuck checker or a giant final export.

Checker reference:PalomarRegistry/PalomarSubmission@d4e41c1d5b0d114c4859e6e5831dc6d3ad1d0d44 scripts/verify_submission.py and docs/comparator-declaration-closure.md; matching Lean src/lake/Lake/CLI/Check.lean. Use authenticated bundled leanexport MODULE -- ROOTS... (stdout export); leanchecker --silent --from-export EXPORT; nanoda_bin CONFIG; con-ron --jobs=2 EXPORT. Include complete unit roots, permitted axioms, Quot builtins and primitiveTargets parsed from matching source excluding comments, with all transitive declarations. Use the matching NanoDa config; its unpermitted_axiom_hard_error:false never waives strict axiom checking. No guessed tools/versions or comparator/registry run.

Only propext,Quot.sound,Classical.choice permitted: reject sorryAx/added/native-reduction axioms. PASS needs successful exit AND exact expected-type/axiom evidence for EVERY unit root. Retain isolated false-type/disallowed-axiom controls and an incomplete-export/dependency control when replay runs. Never invent control outcomes. Record separate compile/type/axioms/export/lean_replay/nanoda/con_ron statuses:PASS,FAIL(actual rejection),INCONCLUSIVE(interrupted),BLOCKED(missing prerequisite),NOT_RUN. Loader failures are not disproofs. Bind replay to actual binary/config/command, accessible export bytes/hash/roots, raw logs, exits and phase wall times. Lean replay is same-kernel; structural acceptance is not proof validation. Count distinct complete units per tier, not sums across tiers.

Respect supplied time/turn/lease/resource/tool limits. Reserve enough time for checks, packaging and normal upload; finish BEFORE exhaustion: local checkpoints are not delivered and timeout can discard them. No extra requester deadline. Stop on queue exhaustion, insufficient safe budget or blocker; record reason, attempted results and exact remaining IDs. Honest partial coverage is acceptable; all87/allkernels are NOT mandatory. No proof executed means no verification. No detached work, limit bypass, extra paid job, signing, host/config/credential/environment inventory, global installation, Actions, deployment or publication. Task-local authenticated tool acquisition within normal policy only. Let normal worker submission upload; no device credentials/direct uploads.

Only declared artifacts may change. Preserve original sources and accepted branch outputs. Branch receipt schema imd-lean-capacity/v1:source/toolchain/branch, unit IDs/types/root sets/stage results, commands/exits/timings/controls, cache provenance, stop reason, remaining IDs and tier totals. Archive regenerated source-bound manifest, receipts/logs/configs and deduplicated exports, not toolchain/cache binaries. Limits:64MiB/file,128MiB uploads/lease,8MiB source changes; archive<=60MiB. Retain earliest deliverable exports if space runs out; flag missing delivery, never truncate proofs or count missing bytes as portable evidence.