Vernier CRT seam-density theorem (sorry-free)

[toadkicker]

Verified, sorry-free. Adds the within-axis vernier CRT seam-density
theorem to the OrdvecFormalization corpus. All proofs discharged against
Lean 4.28.0 + the pinned Mathlib.

Theorem

For pairwise-coprime grid periods m : Fin L → ℕ, the positions in
ZMod (∏ m i) within band t of a seam on every grid number exactly
∏ (2t+1) (capped form ∏ min(2t+1, m i) once a band saturates its grid).
In particular (t = 0) there is exactly one all-grids coincidence per period.

Proof structure

• crtEquiv — the indexed CRT bijection ZMod (∏ m i) ≃ Π i, ZMod (m i), taken
  as .toEquiv of Mathlib's existing ZMod.prodEquivPi (no bespoke Fin L
  fold of the two-modulus CRT was needed — the Pi-CRT is already in Mathlib).
  Carries [∀ i, NeZero (m i)] and [NeZero (∏ i, m i)] (the latter is not
  synthesizable from the former — ∏ is a general Finset.prod). Sole consumer
  of coprimality.
• card_admissible — Finset.card_image_of_injOn + ZMod natCast window
  injectivity (2t+1 ≤ m ⇒ no wraparound).
• blindspot_card_product — Fintype.card_piFinset. The easy half; carries
  no coprimality hypothesis, which is the honest statement of what it proves.
• blindspot_card_positions — the real theorem; transports the product count
  across crtEquiv via Finset.card_equiv.
• unique_coincidence_per_period — the t = 0 corollary.

Verification (all green locally)

• lake build ✔
• #print axioms on all 5 public names → [propext, Classical.choice, Quot.sound],
  no sorryAx
• make audit ✔ (no sorry in tree) · make verify ✔ · lake lint ✔
  (Linting passed) · check-doc-names ✔ (277 names)

Files

• OrdvecFormalization/VernierSeamDensity.lean (new, in the audited tree)
• OrdvecFormalization.lean — registered in the root aggregator
• docs/theorem-map.md — 5 new public names

Provenance

Cross-checked exhaustively by finite enumeration over ℤ/M in the companion
ordvec research repo's Rust oracle; this is the verified Lean proof.

CI note

The upstream Lean workflow currently shows action_required — this is a fork
PR, so GitHub holds the run pending a maintainer "Approve and run workflows"
click (first-time fork-contributor gate). It has not failed; it has not been
allowed to start. Approving the run populates the required build check and
clears BLOCKED. Given the local results above, I expect it green.

🤖 Generated with Claude Code

[gemini-code-assist]

Code Review

This pull request adds a proof sketch for the within-axis vernier CRT seam-density theorem in drafts/VernierSeamDensity.lean, along with a descriptive drafts/README.md. The review feedback correctly identifies that Lean's typeclass resolution cannot automatically synthesize NeZero (∏ i, m i) from [∀ i, NeZero (m i)]. To prevent elaboration failures and ensure Finset.univ can resolve its Fintype instance, you should explicitly add [NeZero (∏ i, m i)] as an instance argument to crtEquiv, blindspot_card_positions, and unique_coincidence_per_period.

Important

The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.

[toadkicker]

Promoted from draft → verified, sorry-free. All proof debt discharged against Lean 4.28 + Mathlib on a local toolchain.

The crux turned out NOT to need a bespoke Fin L CRT induction — Mathlib already ships the indexed Pi-CRT as ZMod.prodEquivPi (Mathlib/Data/ZMod/QuotientRing.lean), so crtEquiv is just .toEquiv of it. card_admissible is card_image_of_injOn + a ZMod natCast window-injectivity argument; blindspot_card_positions transports the product count across crtEquiv via Finset.card_equiv.

Moved into the audited OrdvecFormalization/ tree and registered in the root aggregator. Local gate results:

• lake build ✔
• #print axioms → [propext, Classical.choice, Quot.sound] only, no sorryAx (all 5 public names)
• make audit ✔ (no sorry) · make verify ✔ · lake lint ✔ · check-doc-names ✔ (277 names; added the 5 new ones to docs/theorem-map.md)

Theorem: for pairwise-coprime grid periods m : Fin L → ℕ, positions in ZMod (∏ m i) within band t of a seam on every grid number exactly ∏ (2t+1) (capped form ∏ min(2t+1, m i) under saturation), with exactly one all-grids coincidence per period. Provenance: exhaustively cross-checked by the companion research repo's ℤ/M enumeration oracle.

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (1) 📘 Rule violations (0)

1. Long-line linter violation 🐞 Bug ☼ Reliability

Description

OrdvecFormalization/VernierSeamDensity.lean introduces very long theorem-signature lines (notably
blindspot_card_product) while weak.linter.style.longLine is enabled and builds run with
--wfail, so this can surface as a warning that fails CI builds.

Code

OrdvecFormalization/VernierSeamDensity.lean[R63-65]

+theorem blindspot_card_product
+    {L : ℕ} (m : Fin L → ℕ) [∀ i, NeZero (m i)] (t : ℕ) (hband : ∀ i, 2 * t + 1 ≤ m i) :
+    (Finset.univ.filter

Evidence

The project enables weak.linter.style.longLine and uses lake build --wfail, so style warnings
can fail builds. The new file contains at least one very long theorem signature line (the
blindspot_card_product binder line).

lakefile.toml[7-18]
Makefile[1-6]
OrdvecFormalization/VernierSeamDensity.lean[63-67]

Agent prompt

The issue below was found during a code review. Follow the provided context and guidance below and implement a solution

## Issue description
The repo enables the long-line style linter (`weak.linter.style.longLine = true`) and runs builds with `lake build --wfail`, which treats warnings as failures. The new theorem signatures in `VernierSeamDensity.lean` include very long single lines, which violates the style constraint and can break CI.

## Issue Context
This project’s CI pipeline is configured to fail on warnings, and style linters are enabled via Lean options.

## Fix Focus Areas
- OrdvecFormalization/VernierSeamDensity.lean[63-67]
- OrdvecFormalization/VernierSeamDensity.lean[90-97]
- lakefile.toml[7-18]
- Makefile[1-6]

## Suggested fix
Reformat the long declarations by splitting parameters and hypotheses across multiple lines (matching the style used elsewhere in the repo), e.g. put each implicit/explicit argument group on its own line, and consider breaking long `filter` predicates onto multiple lines where needed.

ⓘ Copy this prompt and use it to remediate the issue with your preferred AI generation tools

---

[qodo-code-review]

PR Summary by Qodo

Formalize vernier CRT seam-density theorem in OrdvecFormalization
✨ Enhancement 📝 Documentation 🕐 20-40 Minutes

Walkthroughs

Description

• Add Lean formalization of within-axis vernier seam-density counting over coprime grids.
• Register the new theorem module in the OrdvecFormalization root import aggregator.
• Extend theorem-map documentation to list the new vernier seam-density results.

Diagram

graph TD
  agg["OrdvecFormalization.lean"] --> vernier["VernierSeamDensity.lean"] --> mathlib["Mathlib (ZMod/Finset)"]
  docs["docs/theorem-map.md"] --> vernier

Loading

High-Level Assessment

The following are alternative approaches to this PR:

1. Expose `crtEquiv` as a `RingEquiv` (or use `ZMod.prodEquivPi` directly in statements)

• ➕ Keeps algebraic structure available for downstream lemmas (homomorphism properties, simp lemmas).
• ➕ May reduce the need to coerce between RingEquiv/Equiv later.
• ➖ Slightly heavier statements and typeclass obligations for purely cardinality-focused results.
• ➖ May increase simp/search complexity for reviewers unfamiliar with the RingEquiv API.

2. Factor the position-space count via `Fintype.card_congr` on subtype sets

• ➕ Often yields a more declarative proof: define the admissible subset and transport it across the equivalence.
• ➕ Can make the Finset.univ.filter proofs shorter and more reusable.
• ➖ Requires more setup (subtype predicates, coercions between Finset and Set).
• ➖ May be more verbose than the current Finset.card_equiv approach.

Recommendation: Current approach is solid: prove a per-modulus admissible cardinality lemma, count in product space via Fintype.card_piFinset, then transport to ZMod (∏ m i) via ZMod.prodEquivPi (wrapped as an Equiv). Consider switching crtEquiv to a RingEquiv only if upcoming work needs algebraic properties beyond bijectivity.

File Changes

Enhancement (2)

OrdvecFormalization.lean Import the new VernierSeamDensity module +1/-0

Import the new VernierSeamDensity module

• Adds 'import OrdvecFormalization.VernierSeamDensity' to the root aggregator so the new theorems become part of the library build/import surface.

OrdvecFormalization.lean

---

VernierSeamDensity.lean Add vernier CRT seam-density counting lemmas over ZMod +115/-0

Add vernier CRT seam-density counting lemmas over ZMod

• Introduces 'admissible' residues within a centered band and proves 'card_admissible' when the band fits. Proves the product-space cardinality ('blindspot_card_product'), defines the CRT equivalence ('crtEquiv' via 'ZMod.prodEquivPi'), transports the count to position space ('blindspot_card_positions'), and derives the 't=0' corollary ('unique_coincidence_per_period').

OrdvecFormalization/VernierSeamDensity.lean

---

Documentation (1)

theorem-map.md Document vernier seam-density theorems in the theorem map +8/-0

Document vernier seam-density theorems in the theorem map

• Adds a new section listing the Vernier seam-density definitions/lemmas so readers can discover them from the theorem index.

docs/theorem-map.md

---

[toadkicker]

CI note: the Lean workflow shows action_required — it's a fork PR, so GitHub is holding the run pending a maintainer's "Approve and run workflows" click (first-time fork-contributor gate). It hasn't failed; it hasn't been allowed to start. A maintainer approving the run is all that's needed to populate the required build check and clear the BLOCKED state.

For reference, the full gate sequence was run locally against Lean 4.28.0 + the pinned Mathlib and all passed:

• lake build ✔
• #print axioms for all 5 public names → [propext, Classical.choice, Quot.sound], no sorryAx
• make audit ✔ (no sorry in tree) · make verify ✔ · lake lint ✔ (Linting passed) · check-doc-names ✔ (277 names)

So I expect the upstream run to go green once approved.