[t-uda]

Closes #721

Minimal elements outside a principal downset in a finite product are now classified by their unique active coordinate. This proves D(G.Point) ≤ n for actual coordinate grids with nonempty factors. The genuinely adjoined top is handled separately, giving D(WithTop S) ≤ max 1 D(S), including singleton S.

For the existing interval-pair subtype, the minimal complement is the disjoint union of the restricted diagonal family (a,a), a≤k, and the bottom-first-coordinate family (⊥,b). Its actual cardinality decomposition gives D(PairPoset G.Point) ≤ 2*n for n≥1 while preserving the existing order and algebra interfaces.

The proved grid count discharges the premise of the existing ordinary-injective Hom theorem: every pointwise finite-dimensional ordinary injective on the grid has actual hook-Hom projective dimension at most n−1, over any field. Every supplied certified minimal rank-projective resolution of that injective therefore has zero terms above n−1.

These are numerical counting and injective-side results toward #661 / #501. Numerical ordinary incidence/Hom-cokernel estimates, the universal 2n−2 bound and final signed stability remain unfinished. Resolution assertions use high-degree term vanishing, not a bound on the stored raw length.

Source context: BOOS arXiv:2208.00300v3, Notation 5.2/5.9, Proposition 5.14 and the counting ingredient of Theorem 5.16. The subtype and adjoined-top cases are proved directly; the full algebra/global-dimension conclusion is not asserted.

Validation (evaluated head df75f50f30cb9aba18775c22affa8928a7944548, base 0d856e9e336b4b2c85b25fcf7acbd33b3f44da62, tree 41755dae01adfe54117633d5888f2d96245d8997):

• Guarded focused module builds passed: core 3,336 jobs, injective consumer 3,337 jobs, examples 3,338 jobs. After the three review fixes, LEAN_NUM_THREADS=2 scripts/lean.sh lake build TDA.Persistence TDA.Persistence.Examples passed, 9,264 jobs. git diff --check: exit 0.

• LEAN_NUM_THREADS=2 bash scripts/check.sh: exit 0 on the final head before push, 9,520 jobs. Live axiom audit: 11,149 declarations within {propext, Classical.choice, Quot.sound}; coverage: 8,933 public theorems, all pinned. The 50 new pin roots include the two generated decode equations.

• Independent final-head mathematics/source/API, exposition-flow and deslop-history: PASS. Three P3 findings are resolved: resolution-target docstring, API prerequisite gloss, and direct reuse of pinned WithTop.untop/coe_untop. The grouped independent review artifact records the inspected surface and resolved findings.

• The normal pre-push hook is enabled. Because this clone lacks its expected origin base refs, the full canonical gate was explicitly executed before push; no full-build result is inferred from the hook's change detection.

• Hosted exact-head check run 40484790208: completed/success, including the full scripts/check.sh step at df75f50f30cb9aba18775c22affa8928a7944548. The earlier draft-only skipped run is not validation. Ordinary develop scope; no release version/publication decision.

• Integration: expected-head squash merged as 7239342466e3904c2bb544eea6a17dc023600ff7. Fetched develop has the reviewed whole tree and identical content in all nine changed files. Direct post-merge push run 40485956755 completed/success, including full gate. Own issue-721-grid-complement-cardinality remote/local topics were deleted (one each) after PR/head/clean-worktree checks; absence verified, persistent and other-owner branches retained.

[t-uda]

Independent final-head review artifact

Reviewed-by: /root/review_703, distinct from sole implementer /root/quotient_basechange_703_impl (requested reviewer Sol high; implementation Luna xhigh). Full source/math/API review at f576c3de0400fab9ae5c9d96e891a974e329c127, then narrow affected-source confirmation at evaluated head df75f50f30cb9aba18775c22affa8928a7944548, tree 41755dae01adfe54117633d5888f2d96245d8997, base 0d856e9e336b4b2c85b25fcf7acbd33b3f44da62.

Final mathematics/source/API PASS; exposition-flow PASS; deslop-history PASS. Findings 1–3 resolved; no open finding. The reviewer read the full frozen Issue contract/comments and complete nine-file implementation, actual consumers, owning imports/pins and public prose. Direct source comparison used BOOS arXiv:2208.00300v3, Notations 5.2/5.9, Proposition 5.14 and Theorem 5.16's counting ingredient.

• Product classification proves both directions for the actual minimal-outside-downset predicate. The chosen active coordinate is genuinely injective, including the empty-index case, so the counts are proved rather than supplied.
• The old/new tops are distinct. Actual minimality excludes the new top below a non-top old point; old top has exactly the new singleton. The max-1 correction is used and covers singleton lattices.
• The existing interval-pair order is preserved by named reducible local lattice/bounded-order constructors. Its exact disjoint decomposition uses diagonal (a,a) with a≤k and the bottom-first family, not an inadmissible ambient-product axis. The cardinality equality retains the restricted first family; dropping its restriction occurs only in a proved upper bound.
• Actual grid bounds treat n=0 and singleton factors correctly; the simplified WithTop/pair bounds explicitly require n≥1. No field assumption enters counting.
• The ordinary-injective pfd consumer derives actual hook-Hom projective dimension ≤n−1 from the new counts and existing theorem, over arbitrary fields. High-term zero holds for every supplied certified minimal rank-projective resolution of M, without a raw-length claim or supplied target bound.
• Concrete pinned Mathlib update/minimality/cardinality/subtype/finite-order APIs and existing Hom dimension comparison are reused. Relevant immutable TauCeti order material was checked for applicability; no dependency or framework port is needed.
• The consumers include zero-coordinate and singleton/square real grids, both tops and actual pair families, and a proved nonzero rational ordinary injective. The reviewer accounted for all 50 appended roots, including two generated decode equations.
• Public exposition introduces the predicate, pair carrier and grid before their bounds, and distinguishes counts/injective-side conclusions from the unfinished ordinary incidence/Hom-cokernel/universal2n−2/signed-stability claims. No execution history is shipped.

Resolved findings: (1) the example docstring now correctly describes a minimal resolution of the original ordinary injective; (2) the API entry adds the prerequisite gloss; (3) the private non-top extraction/spec reuse pinned WithTop.untop and WithTop.coe_untop. The final narrow review reread the changed helper/equivalence consumers and confirmed all public names/types, other proofs, instances and pins unchanged.

The reviewer read the recorded focused build logs, including the corrected 9,264-job owning-aggregator build, and ran no probes/builds/audits or source/GitHub writes. Driver canonical and hosted/integration evidence are recorded separately in the PR validation block.