Lean formalisation attribution + SearchResults #[must_use] (external-review quick fixes)

[Fieldnote-Echo]

What

The "fix now" slice of triaging an external technical review of v0.2.0. The remaining 13 recommendations are filed as #80–#88 (+ comments on #32/#33). Two changes here:

1. docs: correct the Lean formalisation claims (README + docs/RANK_MODES.md)

The README claimed the rank-transform monotone-reparametrisation invariance was "machine-checked in Lean" with no link, and docs/RANK_MODES.md still said the Bayes-optimality theorem was "not claimed here". Both are now public, sorry-free Lean 4 proofs — but in two repos, proving two different theorems:

• ordinal/rank invariance under strictly monotone reparametrisation → Project-Navi/takens-formalization (isOrdinalPatternOf_comp_strictMono)
• in-model Bayes-threshold optimality of the popcount overlap cutoff + the exact hypergeometric null → Fieldnote-Echo/ordvec-formalization (exists_uniformBitmapOverlapTail_finiteBayesRisk_le_and_hypergeomTail)

Now attributes the right theorem to the right repo, with the in-model conditional kept explicit — optimal under the modelled MLR/FNCH assumptions, not a claim that any corpus obeys the model (whether real neighbours clear the bar stays empirical, per §6/§7).

2. feat: #[must_use] on SearchResults + top_m_candidates*

Discarding a search result is a silent no-op footgun — index.search_asymmetric(&queries, 10); does the work and drops it. Annotates SearchResults (covers every search* method returning it) and the pure top_m_candidates* query methods on Bitmap/SignBitmap. Compile-only metadata; no runtime change.

Test plan

• cargo fmt --all --check
• cargo clippy --all-targets --all-features -- -D warnings — compiles all tests, so would catch any in-tree discarded #[must_use] value; clean
• cargo test — 131 passed
• bot review (copilot / gemini / qodo) + Codex stop-gate

Follow-ups (not in this PR)

Filed from the same review, with corrections baked in: #80 (remove ordered-float — via f32::total_cmp, not the review's sort_unstable which would break the documented stable tie-break), #81 (Debug), #82 (serde), #83 (iterator add), #84 (fastscan feature-gate), #85 (parallel feature — scoped; no_std is a bigger lift than the review implied, since write/load are std-only), #86 (try_*/Result), #87 (C-ABI), #88 (tombstone). Dropped: real-corpus harness (lives in ordvec-harness) and Criterion (cuts against the self-contained bench_rank).

🤖 Generated with Claude Code

[qodo-code-review]

Review Summary by Qodo

Add #[must_use] to SearchResults and correct Lean formalization attribution

✨ Enhancement 📝 Documentation

Walkthroughs

Description

• Add #[must_use] attribute to SearchResults and candidate-generation methods
  - Prevents silent no-op footgun of discarding search results
  - Covers all search* methods and top_m_candidates* on Bitmap/SignBitmap
• Correct and expand Lean formalization attribution in documentation
  - Link ordinal invariance proof to takens-formalization repo
  - Link Bayes-optimality theorem to ordvec-formalization repo
  - Clarify in-model scoping of optimality result (not corpus-level claim)

Diagram

flowchart LR
  A["SearchResults & top_m_candidates methods"] -->|"Add #[must_use] attribute"| B["Compiler warns on unused results"]
  C["README & RANK_MODES.md"] -->|"Link to Lean repos"| D["takens-formalization<br/>ordvec-formalization"]
  D -->|"Clarify in-model scope"| E["Explicit assumptions documented"]

Loading

File Changes

1. src/bitmap.rs ✨ Enhancement +3/-0

Mark candidate generation methods with #[must_use]

• Add #[must_use] attribute to top_m_candidates method
• Add #[must_use] attribute to top_m_candidates_batched method
• Add #[must_use] attribute to top_m_candidates_batched_chunked method

src/bitmap.rs

---

2. src/lib.rs ✨ Enhancement +1/-0

Mark SearchResults struct with #[must_use]

• Add #[must_use] attribute with explanatory message to SearchResults struct
• Message clarifies that dropping search results is a silent no-op

src/lib.rs

---

3. src/sign_bitmap.rs ✨ Enhancement +2/-0

Mark SignBitmap candidate methods with #[must_use]

• Add #[must_use] attribute to top_m_candidates method
• Add #[must_use] attribute to top_m_candidates_batched method

src/sign_bitmap.rs

---

View more (2)

4. README.md 📝 Documentation +19/-5

Attribute Lean formalizations to their repositories

• Expand Lean formalization section with explicit repo links and theorem names
• Add link to takens-formalization repo for ordinal invariance proof
• Add link to ordvec-formalization repo for Bayes-optimality theorem
• Clarify in-model scoping: optimality under stated assumptions, not corpus-level claim

README.md

---

5. docs/RANK_MODES.md 📝 Documentation +17/-9

Document machine-checked Bayes-optimality theorem and assumptions

• Update "research program" section to reflect now-checked Bayes-optimality result
• Add link to ordvec-formalization repo with specific theorem name
• Clarify in-model nature of the result and empirical verification scope
• Emphasize distinction between theoretical optimality and corpus-level claims

docs/RANK_MODES.md

---

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (0) 📘 Rule violations (0) 📎 Requirement gaps (0)

1. Misleading must_use message ✓ Resolved 🐞 Bug ⚙ Maintainability

Description

SearchResults is annotated with #[must_use], but its warning text says dropping the value “does
no work” even though the search computation already occurred and dropping still runs destructors
(deallocating the backing Vecs). This can confuse users reading the compiler warning about what
actually happened and why the call was wasteful.

Code

src/lib.rs[112]

Evidence

The #[must_use] message claims dropping does “no work”, but Bitmap::search performs the scan and
fills the output buffers before returning SearchResults by value; dropping that value still drops
Vec<f32>/Vec<i64> and deallocates them.

src/lib.rs[101-118]
src/bitmap.rs[122-171]

Agent prompt

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

## Issue description
`SearchResults` uses a `#[must_use = "…"]` message that is misleading: dropping the returned value does not mean “no work” happened. The search already ran, and dropping still deallocates the result buffers.

## Issue Context
This message appears in compiler warnings when a caller ignores a search return value. The intent is good (prevent silent no-op usage), but the wording should accurately describe the situation (results were computed and then ignored/wasted).

## Fix Focus Areas
- src/lib.rs[101-118]

Suggested replacement text (pick one):
- `#[must_use = "search returns results by value; unused results waste work"]`
- `#[must_use = "unused search results; use them or explicitly ignore with let _ = …"]`

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

---

[gemini-code-assist]

Code Review

This pull request updates the documentation in README.md and docs/RANK_MODES.md to reference the Lean 4 formalizations of ordinal invariance and the bitmap candidate filter. It also adds #[must_use] attributes to several candidate generation functions in src/bitmap.rs and src/sign_bitmap.rs, as well as the SearchResults struct in src/lib.rs. The review comments suggest minor grammatical improvements to the documentation and recommend adding descriptive warning messages to the #[must_use] attributes to ensure consistent and informative compiler warnings.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[Fieldnote-Echo]

@codex review

[Copilot]

Pull request overview

This PR applies a small set of “fix now” items from an external review: it corrects/clarifies Lean formalisation attribution in the docs, and adds #[must_use] to search/candidate-result-returning APIs to prevent silent result dropping.

Changes:

• Update README + docs/RANK_MODES.md to attribute two distinct Lean 4 proofs to the correct external repositories and to clarify the “in-model” nature of the optimality claim.
• Add #[must_use] to SearchResults to warn on ignored search results.
• Add #[must_use] to Bitmap/SignBitmap top_m_candidates* methods to warn on ignored candidate sets.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/sign_bitmap.rs	Adds #[must_use] to candidate-generation APIs to prevent silently ignored results.
src/lib.rs	Marks SearchResults as #[must_use] to warn when search outputs are dropped.
src/bitmap.rs	Adds #[must_use] to candidate-generation helpers (single, batched, chunked).
README.md	Corrects Lean formalisation attribution and clarifies theorem scope (“in-model”).
docs/RANK_MODES.md	Updates the research-program section to reflect the now-checked formal link and reiterates scope limits.

---

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 82801039a5

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[Fieldnote-Echo]

Review triage (pushed in 1d81187)

Finding	Reviewer	Disposition
SearchResults #[must_use] message says "no work" — misleading	Copilot	Fixed — reworded: the scan already ran, so a dropped result discards work
Add descriptive messages to the top_m_candidates* #[must_use] (×5)	gemini	Fixed — added consistent messages
README: "on which the rank transform rests" grammar	gemini	Fixed
RANK_MODES: "rather than claiming that"	gemini	Declined — kept not a claim that parallel with the README's matching caveat
README headline theorem "not defined" in ordvec-formalization	Codex	False alarm — the theorem is real at HEAD (BitmapCalibration.lean:305); the review read a pre-sweep snapshot (the name it cites, overlapNull_threshold_isBayesOptimal, was renamed away by b4205e2). Filed a name-stability guard upstream: Fieldnote-Echo/ordvec-formalization#5

Gate re-run green: fmt / clippy --all-targets --all-features -D warnings / cargo test (all suites pass).