feat: define and characterize contiguity

[CoolRmal]

This PR adds five filter-based definitions of contiguity and proves their equivalence.

In particular, it:

• proves Contiguous1 → Contiguous2;
• proves Contiguous2 ↔ Contiguous3;
• proves Contiguous3 → Contiguous1;
• streamlines the antitone-basis proof from Contiguous5 to Contiguous1;
• proves that all five definitions are equivalent for sequences indexed by ℕ.

Validation:

• lake env lean Statlib/Contiguity.lean
• lake build
• lean4-skills-sorry-analyzer . --report-only (0 sorries)
• git diff --check

Closes #12.
Closes #13.
Closes #14.
Closes #15.
Closes #24.

Created with the help of Codex.