[t-uda]

Closes #737. Part of #501; ordinary develop work, release version undecided.

Originally finitely presented modules over an arbitrary field now yield actual occurrence matchings of their signed hook barcodes at radius (2*n-1)^2 * ε. The extended-distance bound holds for every certified minimal resolution, and for the module barcode obtained from proved minimal-resolution existence, without attainment or finite-distance assumptions.

The construction presents the unshifted Schanuel biproducts as finite hook sums and identifies each tag multiplicity with the two cross-sign multisets. It reuses the existing interleaving, hook matching and choice-independence results. A consumed ULift index conversion preserves the original finite-presentation universe and existing barcode API. Focused consumers cover dimensions one and two, zero radius, finite and infinite deaths, empty families, and repeated cross-sign occurrences.

Source ↔ Lean: BOOS arXiv:2208.00300v3 §§2.7–2.9, Proposition 4.3 (finite-family case), and the final assembly of Theorem 6.1. The signed comparison preserves positive/negative occurrences without cancellation. No countable matching extension, optimality, ordinary one-dimensional barcode identification, triangle law, or full #501 completion is claimed.

Validation (evaluated head 3165f41cbbbec40166161d50a620de5b49a24035, base 6825864551a5be52c9d4abb4764cff85a0c9015c, tree 057494b7f72bc4aa5f1278a54266e8f332d1879e):

• Focused guarded Lean targets: LEAN_NUM_THREADS=2 scripts/lean.sh lake build TDA.Persistence.RankSignedStabilityExamples TDA.Persistence — exit 0, 9127 jobs.

• LEAN_NUM_THREADS=2 bash scripts/check.sh: exit 0; 9539 build jobs; live audit 11406 declarations within {propext, Classical.choice, Quot.sound}; 9111 public theorems all pinned; 8891 private roots audited (4971 in pinned closures, 3920 additionally checked).

• Independent source/math/API and separate exposition-flow/deslop-history review: PASS at the evaluated head.

• Evaluated-head hosted check / full gate: run 40586707227 completed successfully, including check and Full gate (scripts/check.sh); draft-skipped run 40586666928 is not acceptance evidence.

• Post-merge develop b79987fc4a1e8b94064f95f7aec5b61dc6eb16fb: run 40587940808 completed successfully, including check and full gate. Its tree equals the reviewed tree; source-to-merge diff is empty. Own remote/local topic branch deleted and absence verified; long-lived branches and protected WIP retained.

[t-uda]

Reviewed-by: /root/signed_stability_plan_review

Independent final-head source/math/API review: PASS. Separate exposition-flow: PASS; deslop-history: PASS.

Reviewed head 3165f41cbbbec40166161d50a620de5b49a24035, tree 057494b7f72bc4aa5f1278a54266e8f332d1879e, base 6825864551a5be52c9d4abb4764cff85a0c9015c. Reviewer is distinct from implementation worker /root/signed_737_impl. Comparison mode: source-based, directly reading BOOS arXiv:2208.00300v3 §§2.7–2.9, Proposition 4.3 and Theorem 6.1, the full amended #737/#501 contracts, complete diff, actual inherited definitions and relevant pinned APIs.

The review verifies the original FinitelyPresented.{u,0,0} assumptions over arbitrary fields, the proved ULift presentation-index conversion with actual free/cokernel isomorphisms, actual parity hook presentations and tag-by-tag multiplicity equalities, reuse of the existing interleaving and hook matching to construct radius (2*n-1)^2*ε witnesses, fixed-target double-infimum distance proof without attainment/finiteness assumptions, and module barcode comparison through existing choice independence. Meaningful finite-death, principal, empty, repeated cross-sign and original-FP consumers were inspected. Existing public HookBetti interfaces remain unchanged; no matching/decomposition/numerical certificate is an added caller premise. No countable extension, optimality, triangle instance or full #501 completion is claimed.

No substantive findings. One nonblocking documentation naming suggestion would explicitly identify the exported names behind the already defined dHook/dSigned shorthand; the definitions and intended meanings are recoverable, so it is deferred without a source change or extra review round. The reviewer inspected the supplied focused build/scoped axiom logs and did not rerun builds. The canonical gate and hosted checks are recorded separately in the PR validation block; they were not claimed as performed by this review.