[t-uda]

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

The actual hook-generator Hom cokernel now receives the proved diagonal-quotient projective-dimension bound. Over any field, pfd modules on nonempty-factor coordinate grids with n ≥ 1 have Hom projective dimension at most 2n−2, and every supplied certified minimal rank-projective resolution has zero terms in every higher degree.

The proof constructs the actual algebra/scalar bridges, derives Hom and actual cokernel field-finiteness from the original pfd hypothesis, and reuses the existing quotient bounds and two-injective shift. Examples exercise nonzero rational Hom/scalar behavior, repeated fibers, zero objects and one- and two-coordinate grids. Public documentation states the finite-grid scope; real-coordinate transfer and final signed stability remain under #661 / #501. The result concerns highest nonzero degree, independently of terminal zero padding.

Source ↔ Lean

Source-based independent comparison against BOOS arXiv:2208.00300v3, Lemma 5.11, Theorem 5.16's upper proof and Proposition 5.17's upper consequence. The actual Hom cokernel and quotient action are used, with no target estimate or scalar compatibility as input. This proves the finite-grid upper conclusion, not a lower bound, global-dimension equality, real-coordinate transfer or final stability theorem.

Validation

• Evaluated head: f6372d3dd6adfc80b49f6034c3fedb689f5c4a86; base: a3f9ceefa806c1bd1631162b15bc59fd1f8218a4; tree: 3edfc9f5eb4fcc9ff8e7a5e2d1344bb6a3df3fc6.

• Focused guarded LEAN_NUM_THREADS=2 scripts/lean.sh lake build TDA.Persistence TDA.Persistence.Examples: exit 0, 9274 jobs. Subsequent changes are public prose/docstrings and three axiom-pin additions; declarations/proofs/imports are unchanged. The final canonical gate below validates the corrected exact head.

• Final git diff --check: exit 0.

• Final exact-head independent source/math/API, exposition-flow and deslop-history review: PASS. Two local exposition findings, including the diagonal-pair vertex-idempotent qualifier, are corrected and re-reviewed; no unresolved finding.

• Canonical exact-head LEAN_NUM_THREADS=2 bash scripts/check.sh: exit 0; build 9530 jobs; live axiom audit 11325 roots within {propext, Classical.choice, Quot.sound}; coverage 9060 public theorems all pinned, private audit 8839 roots (4923 in pinned closures, 3916 additionally checked) passed. The initial three-instance pin omission is corrected and re-reviewed.

• Hosted evaluated-head CI: run 40548976169 completed successfully; check and its actual full gate passed. Draft-skipped run 40548942968 is excluded. Independent review: exact-head artifact.

• Post-merge develop push CI: run 40550740596 succeeded, including check and its full gate, at merge commit c359bfed9c7e6be3159c2dedfcbaf8e3fcbe1be3. The merge tree equals reviewed tree 3edfc9f5eb4fcc9ff8e7a5e2d1344bb6a3df3fc6; source-to-merge diff is empty. The completed topic's remote/local refs were deleted after PR/head verification, with separate absence checks; main/develop/work are preserved.

[t-uda]

Reviewed-by: /root/review_703

Exact head f6372d3dd6adfc80b49f6034c3fedb689f5c4a86, tree 3edfc9f5eb4fcc9ff8e7a5e2d1344bb6a3df3fc6, base a3f9ceefa806c1bd1631162b15bc59fd1f8218a4.

Independent from implementation worker /root/quotient_basechange_703_impl. Source/math/API PASS; exposition-flow PASS; deslop-history PASS. Source-based comparison is limited to the contracted BOOS arXiv:2208.00300v3 Lemma 5.11, Theorem 5.16 upper argument and Proposition 5.17 upper consequence.

The review checks actual opposite-algebra orientation and restriction, canonical versus natural Hom scalars and public computation laws, original-pfd derivation of actual cokernel field-finiteness, ambient module dimension transport, discharged grid arithmetic including n=1, and universal certified-minimal termAt vanishing. It also checks concrete pinned API reuse, old interfaces, nonzero/scalar/zero/repeated/grid consumers, imports/pins and the public finite-grid/real-coordinate boundary. No desired numerical estimate, projectivity or compatible-action premise is hidden in the capstones.

Disposition: two non-substantive exposition findings were fixed: the standalone mathematical definitions (including restriction to vertex idempotents at diagonal pair vertices), and placing the equivalence docstring on its public definition. Narrow review of the prose corrections confirms unchanged mathematical declarations/proofs/types/instances/imports/examples. The initial canonical check also identified three public anonymous local Prop-instance roots missing pins; exactly those roots were appended and independently checked on this final head. All findings are resolved; final exhaustive validation is recorded in the PR block.

No reviewer build, probe or audit/coverage run was performed. Mechanical and hosted evidence belongs to the PR validation block. The review does not claim real-coordinate transfer, equality/lower bounds or final signed stability, and adds no gate beyond normal develop review and validation.