[t-uda]

Closes #733. Part of #661 / #501; ordinary develop work, release version undecided.

Originally finitely presented modules on real coordinate space now have certified minimal rank-projective resolutions whose terms vanish above degree 2n−2, for arbitrary fields and n ≥ 1. The companion theorem proves the same bound for every supplied certified minimal resolution, independently of terminal zero padding.

The proof exposes nonempty factors of the existing presentation grid, applies the proved finite-grid bound, transports actual certified rows and their zero-padded terms through the actual Kan functor, and uses existing termwise uniqueness. The original finite-presentation predicate is the only module hypothesis; no supplied grid, pfd premise, numerical estimate or shortestness assumption is needed. Examples include a nonzero one-coordinate principal upset, a two-coordinate finite presentation with repeated births and nonzero quotient fiber, and the zero module.

Source ↔ Lean

The upper-bound part of BOOS arXiv:2208.00300v3, Theorem 5.18, is obtained from the finite-grid upper bound and Theorem 2.7(2)'s actual Kan reconstruction/minimality mechanism. Existing row-cover and zero-padded uniqueness APIs are reused. This concerns highest nonzero degree, with no raw stored-count bound, equality/lower witness or final signed-stability claim. #501 remains open.

Validation

• Evaluated head 6a3e535bf1ea744f2c969a7be96ebee2e88a73b9; base c359bfed9c7e6be3159c2dedfcbaf8e3fcbe1be3; tree 3c54ea1c88ec52291e07607c43354c533812403f.

• Guarded focused LEAN_NUM_THREADS=2 scripts/lean.sh lake build TDA.Persistence.FinitePresentationGridKan TDA.Persistence.FiniteRankProjectiveResolutionDimension TDA.Persistence.FiniteRankProjectiveResolutionDimensionExamples TDA.Persistence TDA.Persistence.Examples: exit 0, 9276 targets. Subsequent changes are Markdown-only; formal declarations/proofs/imports/pins are unchanged.

• Final git diff --check and referenced Markdown target/anchor checks: exit 0.

• Independent exact-head source/math/API, exposition-flow and deslop-history: PASS; all numbered semantic/API/contract risks and source comparison passed, with no required repairs.

• Exact-head LEAN_NUM_THREADS=2 bash scripts/check.sh: exit 0; build 9532 jobs; live axiom audit 11337 roots within {propext, Classical.choice, Quot.sound}; coverage 9070 public theorems all pinned; private audit 8842 roots (4926 in pinned closures, 3916 additionally checked) passed.

• Hosted evaluated-head CI: run 40557739863 succeeded, including check and its actual full gate. Draft-skipped run 40557699324 is excluded. Independent review: exact-head artifact.

• Post-merge develop push CI: run 40559940906 succeeded, including check and its full gate, at merge commit 7603dcaf07c5775a82131e5d8bfd19f778e70006. Its tree equals reviewed tree 3c54ea1c88ec52291e07607c43354c533812403f; source-to-merge diff is empty. The completed remote/local topic refs were deleted after merged-PR/head/no-extra-commit checks, with separate absence verification; main/develop/work are preserved.

[t-uda]

Reviewed-by: /root/review_733

Exact head 6a3e535bf1ea744f2c969a7be96ebee2e88a73b9, tree 3c54ea1c88ec52291e07607c43354c533812403f, base c359bfed9c7e6be3159c2dedfcbaf8e3fcbe1be3. Independent of implementation worker /root/real_bound_733_impl.

Source/math/API PASS; separate exposition-flow PASS; separate deslop-history PASS. No substantive finding or required repair. Source-based comparison covers BOOS arXiv:2208.00300v3 §2.11–2.12, Theorem 2.7(2), Appendix A's grid/Kan proof and the upper conclusions of Theorem 5.16, Proposition 5.17 and Theorem 5.18. Equality/lower arguments and final signed stability are excluded.

The review checks the original finite-presentation predicate and arbitrary-field/universe hypotheses, internally derived nonempty grid factors including empty presentations, actual quotient-cover/target transport, all-degree Kan termAt comparison including both tails, pinned Functor.map_isZero/IsZero.of_iso reuse, and all-resolution transfer through existing termwise uniqueness. It reads the original nonzero rational/free and genuine repeated-birth presentation consumers, their surviving fiber, zero/degenerate cases, strict degree bounds and padding-insensitive quantifiers. Old public signatures remain unchanged, owning imports/pins are append-only, and no new public local Prop instance is introduced.

Together with #731 this satisfies #661's mathematical upper contract: arbitrary original finitely presented real-coordinate modules have a bounded certified minimal resolution, and every supplied one has zero terms above 2n−2. Empty coordinate factors remain outside the finite-grid theorem's stated hypotheses; empty input presentations are handled by the internally nonempty chosen grid. The result is a highest-nonzero-degree upper bound, not a raw stored-count bound. #501's final signed-stability assembly remains unfinished.

Concrete reuse includes actual repository reconstruction/minimality/termwise uniqueness, pinned Mathlib 0df444a360eaa60ab8c11dca51a86af692955474 zero-preserving-functor APIs, and a bounded comparison with TauCeti 7b0d106bf79dbea38ba8819985bd029989181287 ordinary ModuleCat dimension context, which does not replace this actual Kan bridge. No dependency or generic foundation was added.

No reviewer builds, probes or audits were run; the review relied on supplied focused verification and source inspection. Final exhaustive local and hosted validation is recorded in the PR validation block. There is no unresolved review finding or new approval checkpoint.