[codex] add bitmap overlap symmetry theorem

[Fieldnote-Echo]

What changed

• Added BitmapSymmetry.lean, defining the query stabilizer action on bitmap documents.
• Proved overlap is invariant under query-preserving coordinate permutations.
• Proved equal overlap classifies equal-cardinality bitmap documents up to the query-stabilizer orbit.
• Added a maximal-invariant factor-through theorem for invariant statistics on the constant-weight bitmap space.
• Wired the new module into verification and updated the README/reviewer docs/theorem map.

Why

This adds the algebraic justification for the ordinal quotient: in the bitmap setting, overlap is not an ad hoc popcount, but the orbit classifier for the natural query-preserving symmetry group.

Impact

The existing Bayes/MLR spine remains unchanged. The new layer explains why overlap is the canonical invariant feeding that decision-theoretic theorem.

Validation

• make build
• make verify
• make audit
• make lint

[qodo-code-review]

Review Summary by Qodo

Add bitmap overlap symmetry and maximal-invariant theorem

✨ Enhancement

Walkthroughs

Description

• Added BitmapSymmetry.lean module defining query-stabilizer group action on bitmap documents
• Proved query-stabilizer permutations preserve literal overlap and constant weight
• Established that equal-cardinality bitmaps with same overlap lie in same query-stabilizer orbit
• Proved maximal-invariant theorem: query-stabilizer-invariant statistics factor through overlap
• Integrated new module into verification suite and updated documentation

Diagram

flowchart LR
  QS["Query Stabilizer<br/>Permutations"]
  OVL["Bitmap Overlap<br/>Invariant"]
  ORBIT["Query-Stabilizer<br/>Orbits"]
  FACTOR["Maximal-Invariant<br/>Factorization"]
  QS -->|"Preserve"| OVL
  OVL -->|"Classify"| ORBIT
  ORBIT -->|"Enable"| FACTOR

Loading

File Changes

1. OrdvecFormalization/BitmapSymmetry.lean ✨ Enhancement +330/-0

Group-theoretic symmetry layer for bitmap overlap

• Defined BitmapPerm as coordinate permutation group and queryStabilizer as stabilizer subgroup
• Implemented permuteBitmap, bitmapQueryPart, and bitmapQueryComplPart helper functions
• Proved query-stabilizer permutations preserve overlap via bitmapOverlap_queryStabilizer_eq
• Constructed explicit query-stabilizer permutation between equal-cardinality bitmaps with same
 overlap
• Proved maximal-invariant factorization theorem for invariant statistics on constant-weight bitmap
 space

OrdvecFormalization/BitmapSymmetry.lean

---

2. OrdvecFormalization.lean ⚙️ Configuration changes +1/-0

Wire BitmapSymmetry into main module

• Added import for new BitmapSymmetry module

OrdvecFormalization.lean

---

3. OrdvecFormalization/Verify.lean 🧪 Tests +31/-0

Verify BitmapSymmetry module definitions and axioms

• Added 34 new #check directives for BitmapSymmetry definitions and theorems
• Added 4 new #print axioms directives for key symmetry theorems

OrdvecFormalization/Verify.lean

---

View more (3)

4. README.md 📝 Documentation +15/-1

Document bitmap symmetry layer and theorems

• Added "Bitmap symmetry / maximal invariant layer" section with three key theorem names
• Expanded "Scope" section to mention group-theoretic maximal-invariant theorem
• Added BitmapSymmetry.lean description to module overview

README.md

---

5. docs/reviewer-brief.md 📝 Documentation +7/-0

Add symmetry layer to reviewer brief

• Added BitmapSymmetry.lean description explaining query-stabilizer permutations and orbit
 classification
• Added clarification that real encoders are not proved to satisfy query-stabilizer symmetry
 assumption

docs/reviewer-brief.md

---

6. docs/theorem-map.md 📝 Documentation +37/-2

Update theorem map with symmetry layer details

• Updated main claim to include group-theoretic bitmap-overlap invariant theorem
• Added "Bitmap symmetry layer" section with four key theorems
• Updated dependency graph to show BitmapSymmetry depends on BitmapNull and feeds into
 maximal-invariant theorem
• Added detailed section 14 explaining BitmapSymmetry.lean proof structure and results
• Added new public names for symmetry definitions and theorems
• Added clarification about query-stabilizer symmetry assumption limitations

docs/theorem-map.md

---

[qodo-code-review]

Code Review by Qodo

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

1. Overstrong Inhabited constraint ✓ Resolved 🐞 Bug ⚙ Maintainability

Description

invariantOn_constantWeightBitmapSpace_factorsThrough_overlap requires [Inhabited β] only to
define f using default for overlap values that never occur for `d ∈ constantWeightBitmapSpace D
K, unnecessarily restricting callers to types with an Inhabited` instance. This leaks a proof
implementation detail (default in an unreachable branch) into the public API and makes the theorem
harder to reuse.

Code

OrdvecFormalization/BitmapSymmetry.lean[R297-312]

Evidence

The theorem’s statement exports [Inhabited β] and the definition of f uses default in the
else branch. Later in the proof, the constructed witness hwitness shows the existential is true
for x = bitmapOverlap q d whenever d ∈ constantWeightBitmapSpace D K, so the else branch is
not used for the theorem’s required evaluations of f.

OrdvecFormalization/BitmapSymmetry.lean[297-312]
OrdvecFormalization/BitmapSymmetry.lean[313-327]

Agent prompt

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

## Issue description
`invariantOn_constantWeightBitmapSpace_factorsThrough_overlap` currently requires `[Inhabited β]` because it defines `f` with an `else default` branch. In the proof, `f` is only ever evaluated at overlap values coming from some `d ∈ constantWeightBitmapSpace D K`, so the `else` branch is not needed for the theorem’s conclusion; the stronger constraint is an API usability regression.

## Issue Context
The proof constructs `hwitness` from the input `d` (so the existential is always true at the overlap being queried), making the `else` branch unreachable for the values used in the theorem.

## Fix Focus Areas
- OrdvecFormalization/BitmapSymmetry.lean[297-312]

## Suggested fix directions
- Replace `[Inhabited β]` with `[Nonempty β]` and define a fallback value via `Classical.choice` (or locally introduce `letI : Inhabited β := ⟨Classical.choice ‹Nonempty β›⟩` so the rest of the proof stays the same).
- Alternatively, avoid `default` entirely by defining `f x := F d0` for a fixed `d0` when the existential is false; this needs either `Nonempty β` (to build a total function `ℕ → β`) or a `Nonempty` witness for the bitmap space to pick such a `d0`.

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

---

[gemini-code-assist]

Code Review

This pull request introduces a new file BitmapSymmetry.lean which formalizes the group-theoretic symmetry layer for constant-weight bitmap overlap. It defines coordinate permutations, query stabilizers, and proves that query-stabilizer permutations preserve literal overlap. It also shows that query-stabilizer orbits correspond to same-overlap classes, and that any query-stabilizer-invariant statistic factors through literal overlap. The new definitions and theorems are integrated into the verification tests and documentation. The review feedback suggests significant simplifications to the proofs of mem_permuteBitmap_iff and bitmapOverlap_queryStabilizer_eq by leveraging existing algebraic properties and simplification lemmas.

[Copilot]

Pull request overview

Adds a group-theoretic “bitmap symmetry / maximal invariant” layer establishing that (for constant-weight bitmaps) query-overlap is invariant under the query-stabilizer action and classifies equal-cardinality documents up to that orbit, then exposes the main theorems in the public verification surface and documentation.

Changes:

• Introduces BitmapSymmetry.lean defining the query stabilizer subgroup, the induced bitmap permutation action, and key invariance/orbit-classification/maximal-invariant theorems.
• Wires the new module into the root import surface and Verify.lean (#check + #print axioms).
• Updates README and reviewer/theorem-map docs to include the new symmetry layer and exported theorem names.

Reviewed changes

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

Show a summary per file

File	Description
README.md	Documents the new bitmap symmetry/maximal-invariant theorems and updates scope text accordingly.
OrdvecFormalization/Verify.lean	Adds public API #checks and axiom audit #print axioms entries for the new symmetry layer.
OrdvecFormalization/BitmapSymmetry.lean	New module: defines query-stabilizer action on bitmaps; proves overlap invariance, orbit classification (under card constraint), and factor-through result for invariant statistics on constant-weight space.
OrdvecFormalization.lean	Imports OrdvecFormalization.BitmapSymmetry into the top-level module surface.
docs/theorem-map.md	Extends theorem map to include the symmetry layer and its dependency placement.
docs/reviewer-brief.md	Updates reviewer brief to mention the new symmetry layer and its non-claims.

---

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

[Fieldnote-Echo]

Addressed the bot findings in 98d4370.

• Removed the public [Inhabited β] requirement from invariantOn_constantWeightBitmapSpace_factorsThrough_overlap; the off-support branch now uses F ∅, so no extra typeclass leaks into the API.
• Simplified mem_permuteBitmap_iff using the finset action membership form.
• Replaced the manual overlap-cardinality bijection with the algebraic Finset.smul_finset_inter/Finset.card_smul_finset proof.

Validated with make build, make verify, make audit, and make lint.