[t-uda]

The shifted Schanuel construction previously left a degree-dependent shift on every resolution term. This constructs an actual (2n−1)ε interleaving of the unshifted parity sums for arbitrary-field, originally finitely presented real-coordinate modules, any supplied certified minimal resolutions, and an actual ε-interleaving. The high-degree bound is derived internally; arbitrary zero padding is allowed.

The fixed-resolution extended-distance inequality follows without an attainment or finite-distance assumption. Generic finite-family asymmetric comparisons expose their actual maps, both equations and component laws; examples cover nonzero inputs, dimensions one/two, ε=0, empty/zero families and delayed inactive terms.

Closes #735. Part of #501, which remains open for signed-hook multiset identification, matching/dissimilarity and the final (2n−1)^2 stability and boundary obligations. Target: ordinary develop work; release version undecided.

Source ↔ Lean: BOOS arXiv:2208.00300v3, Theorem 6.1 proof, through the unshifted-module comparison. The coefficient here is 2n−1, giving 3 in dimension two; the final signed coefficient 9 is not claimed. No raw stored-length upper bound or optimality claim is added.

Validation (updated in place):

• Evaluated head: c7125aa6021bc7be48fa969795c12550ff821cf6; base: 7603dcaf07c5775a82131e5d8bfd19f778e70006.
• Focused on aeced9f (identical Lean blobs at the evaluated head): LEAN_NUM_THREADS=2 scripts/lean.sh lake build TDA.Persistence.CoordinateInterleavingDelay TDA.Persistence.RankSchanuelUnshifted TDA.Persistence.RankSchanuelUnshiftedExamples TDA.Persistence TDA.Persistence.Examples — exit 0, 9,279 jobs.
• Pin elaboration on aeced9f: LEAN_NUM_THREADS=2 scripts/lean.sh lake env lean scripts/print_axioms/Persistence.lean — exit 0; no unknown constants or sorryAx.
• Corrected generated pins: LEAN_NUM_THREADS=2 scripts/lean.sh lake env lean /tmp/735-f1-pin-elaboration.lean — exit 0 at the evaluated head; both generated theorems use allowed axioms.
• git diff --check — exit 0.
• Independent exact-head source/math/API, exposition-flow and deslop-history review: PASS for all three, with both initial findings repaired on the final head; independent reviewer /root/unshifted_735_review.
• Canonical LEAN_NUM_THREADS=2 bash scripts/check.sh: exit 0, CHECK OK: 9,535 jobs; 11,372 allowed axiom roots; all 9,088 public theorems pinned; private audit 8,866 roots (4,948 in pinned closures, 3,918 additionally checked).
• Hosted evaluated-head check / full gate: run 40573137632 — completed/success at c7125aa6021bc7be48fa969795c12550ff821cf6; check and its actual Full gate step succeeded. Draft-skipped run 40573076117 is excluded.
• Independent review and dispositions: exact-head review artifact.
• Post-merge develop run 40574238551 — completed/success at 6825864551a5be52c9d4abb4764cff85a0c9015c, with successful check and actual Full gate. Its whole tree equals the reviewed 8e0401b21c4a74b8713aaa7a37864fbe136b7a3b; source-to-merge diff is empty.
• Topic cleanup: merged PR/head verified, no extra topic commits, sole clean worktree and completed workers. Removed issue-735-unshifted-schanuel-bound from GitHub and this clone; successful ls-remote returned no topic ref, local show-ref confirmed absence. Persistent main/develop and protected work were retained.

[t-uda]

Reviewed-by: /root/unshifted_735_review

Exact evaluated head: c7125aa6021bc7be48fa969795c12550ff821cf6; tree: 8e0401b21c4a74b8713aaa7a37864fbe136b7a3b; base: 7603dcaf07c5775a82131e5d8bfd19f778e70006.

Independent source/math/API: PASS. Exposition-flow: PASS. Deslop-history: PASS. Reviewer session is distinct from the Luna implementer and root's bounded transport fix; this durable artifact records the reviewer's result rather than a self-review.

Source-based comparison: directly read BOOS arXiv:2208.00300v3, Theorem 6.1 and proof. Checked actual asymmetric maps and both equations, explicit ε+δ transport, original finite-presentation hypotheses over any field and n≥1, any supplied certified minimal resolutions, internally derived high-degree zeros, existing Schanuel reuse, and the ε-independent fixed-target extended-distance proof. No target bound, interleaving certificate, pfd/decomposition of M,N, or infimum attainment is assumed by the capstone. Reviewed meaningful nonzero and zero/empty/dimension/parameter/padding consumers and bounded pinned Mathlib reuse.

Findings and dispositions: the initial head aeced9f lacked two generated public reassoc pins and the standalone note's explicit hypotheses/parity objects/distance statement. Corrected head c7125aa adds both pins and supplies that complete mathematical statement before its proof. A scoped second review verified the exact correction diff and identical Lean blobs; both findings are addressed. No unresolved finding remains. Public docs describe current mathematics without dispatch/review history or an optimality claim.

The result covers only the unshifted-module step with coefficient 2n−1. #501 remains open for actual signed hook multiset/matching/dissimilarity assembly and the squared coefficient and boundary obligations. This review does not claim unrun canonical or hosted checks; actual validation is recorded in the PR body.