docs: strengthen formal proof framing

[Fieldnote-Echo]

Summary

• Reframes the bitmap proof story around the checked Lean spine: query-preserving symmetry, quotient sufficiency, finite Bayes-threshold optimality, and idealized hypergeometric calibration.
• Adds the finite in-model caveat across README, docs/RANK_MODES.md, Rust docs, Python package docs/docstrings, and adjacent APIs that are not covered by the top-bucket theorem.
• Adds formalization metadata/linkage plus contributor/changelog guardrails for future proof-backed claims.

Checklist

• cargo fmt --all --check passes
• cargo clippy --all-targets --all-features -- -D warnings is clean
• cargo test --all-features passes
• If a SIMD kernel changed: the AVX-512 path is covered (not applicable; docs/metadata only)
• No new system/numerical dependency (no dependency changes)
• MSRV (1.89) still builds — CI enforces this (not run locally; docs/metadata only)
• CHANGELOG.md updated under Unreleased if user-facing
• cargo deny check passes (not run locally; docs/metadata only)
• If ordvec-python/ changed: cargo clippy -p ordvec-python --all-targets -- -D warnings passes

Notes

Additional local checks run:

• git diff --check
• PYTHONDONTWRITEBYTECODE=1 python3 -m py_compile ordvec-python/python/ordvec/__init__.py
• python3 -c 'import tomllib; tomllib.load(open("ordvec-python/pyproject.toml", "rb"))'
• cargo test --doc --all-features
• cargo doc --no-deps --all-features
• cargo doc --no-deps -p ordvec-python

Skipped maturin develop / Python pytest because this PR changes Python-facing docs and package metadata only; no Python or binding behavior changed.

[qodo-code-review]

Review Summary by Qodo

Strengthen formal proof framing for bitmap-overlap theorem

📝 Documentation

Walkthroughs

Description

• Reframes bitmap-overlap documentation around the checked Lean proof spine
• Adds finite in-model caveats across README, docs, Rust and Python docstrings
• Links to formalization repo with proof-spine, theorem-map, and reviewer-brief
• Strengthens contributor guidelines for theory claims and real-encoder distinctions

Diagram

flowchart LR
  A["Bitmap overlap<br/>documentation"] -->|"reframe around<br/>Lean proof spine"| B["Checked finite model:<br/>symmetry, quotient,<br/>threshold, calibration"]
  B -->|"add in-model<br/>caveats"| C["Real-encoder<br/>empirical contract"]
  D["Formalization repo<br/>links"] -->|"proof-spine,<br/>theorem-map"| B
  E["Contributor<br/>guidelines"] -->|"theory claim<br/>boundaries"| C

Loading

File Changes

1. README.md 📝 Documentation +33/-20

Reframe bitmap null around checked finite model

README.md

---

2. docs/RANK_MODES.md 📝 Documentation +27/-17

Expand proof-chain narrative with formalization links

docs/RANK_MODES.md

---

3. src/bitmap.rs 📝 Documentation +35/-10

Add finite model and theorem framing to module docs

src/bitmap.rs

---

View more (16)

4. src/lib.rs 📝 Documentation +12/-2

Document Bitmap as formalization surface with caveats

src/lib.rs

---

5. src/quant.rs 📝 Documentation +4/-0

Clarify rerank semantics vs bitmap threshold guarantee

src/quant.rs

---

6. src/sign_bitmap.rs 📝 Documentation +4/-0

Distinguish sign-agreement from constant-weight theorem

src/sign_bitmap.rs

---

7. src/multi_bucket.rs 📝 Documentation +5/-1

Clarify bilinear decomposition is not theorem surface

src/multi_bucket.rs

---

8. src/fastscan.rs 📝 Documentation +2/-0

Note fastscan latency path outside theorem scope

src/fastscan.rs

---

9. src/rank_io.rs 📝 Documentation +4/-3

Refine constant-weight hypergeometric null language

src/rank_io.rs

---

10. ordvec-python/src/lib.rs 📝 Documentation +22/-5

Add constant-weight overlap model framing to docstrings

ordvec-python/src/lib.rs

---

11. ordvec-python/python/ordvec/__init__.py 📝 Documentation +8/-0

Document Bitmap theorem assumptions and in-model scope

ordvec-python/python/ordvec/init.py

---

12. ordvec-python/README.md 📝 Documentation +14/-2

Add theory section linking formalization and caveats

ordvec-python/README.md

---

13. ordvec-python/pyproject.toml ⚙️ Configuration changes +1/-0

Add formalization repo URL to project metadata

ordvec-python/pyproject.toml

---

14. ordvec-python/tests/test_bitmap.py 📝 Documentation +3/-3

Update test docstring to reference formalization

ordvec-python/tests/test_bitmap.py

---

15. ordvec-python/tests/test_redteam_fuzz.py 📝 Documentation +2/-1

Clarify constant-weight bitmap-null invariant language

ordvec-python/tests/test_redteam_fuzz.py

---

16. examples/bench_rank.rs 📝 Documentation +5/-0

Add empirical complement note to benchmark docs

examples/bench_rank.rs

---

17. CHANGELOG.md 📝 Documentation +6/-0

Document bitmap-overlap docs reframing in unreleased

CHANGELOG.md

---

18. CONTRIBUTING.md 📝 Documentation +4/-0

Add theory-claim boundary guidelines for contributors

CONTRIBUTING.md

---

19. ROADMAP.md 📝 Documentation +3/-2

Reference formalization repo alongside paper

ROADMAP.md

---

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (1) 📘 Rule violations (0)

1. Invalid rustdoc link paths 🐞 Bug ⚙ Maintainability

Description

ordvec-python/src/lib.rs adds rustdoc intra-doc links using Bitmap.method (with .), which is
not valid Rust path syntax for associated items and will not resolve to links in generated docs. Use
Bitmap::method (or Self::method inside the impl) so the references work and avoid potential
broken-link warnings.

Code

ordvec-python/src/lib.rs[R879-885]

Evidence

The binding uses rustdoc intra-doc link syntax […] but with Bitmap.method (dot), which is not
a Rust path to an associated item. Elsewhere in this repo, the same intra-doc link syntax is written
using :: (e.g. [Self::top_m_candidates]), showing the intended/working style.

ordvec-python/src/lib.rs[879-905]
src/bitmap.rs[239-250]

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 Python binding’s rustdoc comments use intra-doc links like `[`Bitmap.body_overlap_scores_subset`]` and `[`Bitmap.top_m_candidates`]`. Rust associated items are addressed with `::`, so these won’t resolve as clickable rustdoc links (and can produce broken-link warnings under stricter rustdoc settings).

### Issue Context
This is within `impl Bitmap` in the PyO3 binding crate, so the simplest correct forms are `[`Self::body_overlap_scores_subset`]`, `[`Self::top_m_candidates`]`, and `[`Self::top_m_candidates_batched`]` (or `[`Bitmap::…`]`).

### Fix Focus Areas
- ordvec-python/src/lib.rs[879-905]

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

---

[gemini-code-assist]

Code Review

This pull request reframes and clarifies the documentation across multiple files regarding the machine-checked Lean formalization of the constant-weight bitmap overlap model, emphasizing its in-model nature and the need for empirical validation on real-world datasets. The review feedback points out several broken Rust intra-doc links in ordvec-python/src/lib.rs where . was used instead of :: to reference methods.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[Copilot]

Pull request overview

This PR tightens and standardizes the crate’s documentation around the companion Lean formalization, explicitly scoping which APIs are covered by the constant-weight bitmap overlap model (and which are not), and propagating the “finite in-model vs real-corpus” caveat across Rust + Python surfaces.

Changes:

• Reframed Bitmap docs (crate root, module docs, and README/docs) around the checked Lean proof spine: symmetry/quotient sufficiency → Bayes-optimal threshold form → idealized hypergeometric calibration.
• Added explicit boundary statements that top-k / fixed-budget shortlist helpers, SignBitmap, fastscan, and MultiBucketBitmap are not themselves the theorem’s threshold-calibration surface.
• Added formalization linkage/metadata and contributor + changelog guardrails for future proof-backed claims.

Reviewed changes

Copilot reviewed 19 out of 19 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/sign_bitmap.rs	Clarifies SignBitmap is not the constant-weight bitmap/theorem surface.
src/rank_io.rs	Refines invariant commentary to explicitly tie to the idealized constant-weight null model assumptions.
src/quant.rs	Notes subset rerank doesn’t itself provide bitmap threshold-calibration guarantees.
src/multi_bucket.rs	Rewords framing (“algebraic object”) and scopes Lean theorem applicability to top-bucket bitmap overlap.
src/lib.rs	Adds crate-level “strongest formal story” framing and clarifies MultiBucketBitmap is not the theorem surface.
src/fastscan.rs	States fastscan latency path is outside the bitmap overlap calibration theorem.
src/bitmap.rs	Expands module + API docs to distinguish overlap statistic vs threshold admission and reiterates in-model scope.
ROADMAP.md	Adds the Lean formalization repo as part of “framing” references alongside the paper.
README.md	Rewrites the bitmap section to “checked finite model” and adds formalization/proof-spine links and explicit caveats.
ordvec-python/tests/test_redteam_fuzz.py	Updates test commentary to refer to constant-weight/formal overlap model assumptions.
ordvec-python/tests/test_bitmap.py	Updates module docstring framing and points formal theorem to ordvec-formalization.
ordvec-python/src/lib.rs	Updates Rust-docs for Python bindings to scope theorem vs shortlist/rerank behavior and invariants.
ordvec-python/README.md	Adds “Theory and calibration” section and clarifies Bitmap vs SignBitmap theorem scope.
ordvec-python/python/ordvec/init.py	Adds package-level docstring explanation of the finite model and its explicit assumptions.
ordvec-python/pyproject.toml	Adds a Formalization project URL for discoverability.
examples/bench_rank.rs	Notes bitmap metrics as an empirical complement/diagnostic for model assumptions.
docs/RANK_MODES.md	Reframes the “checked finite model” section and adds an explicit “formal boundary” note.
CONTRIBUTING.md	Adds guidance to keep theory claims bounded and to cite theorem names/docs + preserve caveats.
CHANGELOG.md	Adds an Unreleased documentation entry describing the reframing.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.