[codex] Add quotient search formalization, windowed probes, and paper draft

[Fieldnote-Echo]

Summary

• Add QuotientConstraints.lean for generic fiber-invariance and non-identifiability consequences of quotient/factorization contracts.
• Add FiniteQuotientSearch.lean for version-space reduction under quotient contracts: sample consistency, collision falsification, observed-bucket agreement, unobserved-bucket extension, counting facts, refinement, and product targets.
• Add FiniteObservationWindow.lean for generic lossy-probe families and finite prefix windows: joint-code kernels, target invariance, image-quotient factorization, longer-window refinement, finite same-window-code falsifiers, coincidence length, and the finite target-aware separating-window existence theorem.
• Add ProfileStability.lean to package supplied finite score certificates for encoder distortion and quotient geometry, then compose them into margin-based admission equality, image-factorization, and kernel-containment theorems.
• Add a persisted formalization paper under docs/paper/, including the TeX source, rendered PDF, extracted text, README, and local ignore rules for LaTeX intermediates.
• Add a compact manual bibliography with verified foundational references for sufficiency, statistical decision theory, comparison of experiments, monotone likelihood ratio decision procedures, probabilistic classification, Lean 4, and mathlib.
• Wire the quotient/profile/window modules into the root import, public verification checks, theorem map, proof spine, reviewer brief, RAG guide, README, and formalization paper.

Closes #13.

Boundary

The profile layer is certificate-based: it assumes finite score-within and quotient-factorization witnesses and proves what follows from those witnesses. It does not claim a manifest schema, empirical estimation procedure, global real-encoder theorem, or surjectivity onto the full theoretical quotient codomain.

The window layer is generic kernel calculus for finite families of observations. It proves that same-joint-code target disagreement falsifies a window-factorized target, and that a finite target-sufficient window exists exactly when every target-disagreeing pair is eventually separated by some coordinate. It does not claim any concrete production probe family is globally sufficient without the finite target-invariance evidence.

The paper is a narrative extraction of the checked theorem surface and its empirical-search consequences. It preserves the finite, conditional boundary: it does not claim that real encoders satisfy the quotient contract, estimate distortion, or prove contrastive training implies quotient invariance.

Citation Notes

The paper cites verified metadata for Fisher (1922), Halmos--Savage (1949), Wald (1950), Blackwell (1953), Karlin--Rubin (1956), Devroye--Györfi--Lugosi (1996), de Moura--Ullrich (2021), and the mathlib Community (2020). Wald's monograph is cited without a DOI rather than reusing a review DOI.

Validation

Latest validation after the windowed-observation layer:

• make build
• make verify
• make check-doc-names
• make audit
• make lint
• latexmk -pdf -interaction=nonstopmode -halt-on-error ordvec_formalization_paper.tex
• pdftotext ordvec_formalization_paper.pdf ordvec_formalization_paper.txt
• strict LaTeX log scan for warnings, unresolved citations/references, overfull/underfull boxes, and fatal errors
• git diff --check

[gemini-code-assist]

Code Review

This pull request introduces two new Lean modules, FiniteQuotientSearch.lean and QuotientConstraints.lean, which formalize version-space reduction under a quotient contract and the structural consequences of quotient/factorization contracts, respectively. The root module, verification files, and documentation are updated to integrate these new layers. The review feedback focuses on simplifying the formalization, with actionable suggestions to remove unnecessary typeclass constraints, eliminate redundant classical tactics, and streamline proofs using term-style definitions or definitional equalities.

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.

[qodo-code-review]

Review Summary by Qodo

Add quotient-search formalization, windowed probes, and comprehensive paper

✨ Enhancement 📝 Documentation

Walkthroughs

Description

• Add comprehensive quotient-search formalization layer with 11 new Lean modules covering fiber
  invariance, version-space reduction, observation windows, and profile stability
• Introduce QuotientConstraints.lean for generic fiber-invariance and non-identifiability
  consequences of quotient contracts
• Introduce FiniteQuotientSearch.lean for version-space reduction under quotient contracts: sample
  consistency, collision falsification, bucket agreement, and refinement
• Introduce FiniteObservationWindow.lean for generic lossy-probe families and finite prefix
  windows with target-invariance and separating-window existence theorem
• Introduce ProfileStability.lean to package finite score certificates for encoder distortion and
  quotient geometry, composing them into margin-based admission and kernel-containment theorems
• Add supporting modules: FiniteQuotientImage.lean, QuotientKernel.lean,
  FiniteFiberTopology.lean, FinitePairQuotient.lean, QuotientRefinementKernel.lean,
  ScoreMarginQuotient.lean
• Add comprehensive formalization paper under docs/paper/ with TeX source, rendered PDF,
  plain-text extraction, and README documenting finite quotient sufficiency, search constraints, and
  profile stability
• Wire new modules into root imports, verification checks, theorem map, proof spine, reviewer brief,
  RAG guide, and README
• Preserve finite, conditional boundaries: no claims about manifest schemas, real-encoder theorems,
  or global probe-family sufficiency without finite evidence

Diagram

flowchart LR
  QC["QuotientConstraints<br/>fiber-invariance"]
  FQI["FiniteQuotientImage<br/>reachable image"]
  QK["QuotientKernel<br/>kernel containment"]
  FT["FiniteFiberTopology<br/>fiber structure"]
  FQS["FiniteQuotientSearch<br/>version-space reduction"]
  FPQ["FinitePairQuotient<br/>product quotients"]
  QRK["QuotientRefinementKernel<br/>refinement via kernels"]
  FOW["FiniteObservationWindow<br/>target-separating windows"]
  SMQ["ScoreMarginQuotient<br/>threshold margins"]
  PS["ProfileStability<br/>composed certificates"]
  
  QC --> FQI
  QC --> QK
  QC --> FT
  FQI --> FQS
  QK --> FQS
  FT --> FQS
  FQS --> FPQ
  QK --> QRK
  FOW --> SMQ
  SMQ --> PS
  FQS --> PS
  QRK --> PS

Loading

File Changes

1. OrdvecFormalization/FiniteQuotientSearch.lean ✨ Enhancement +383/-0

Finite quotient version-space reduction and sample consistency

• Introduces quotient-compatible targets and sample consistency for finite labeled samples
• Defines quotient-level rules and their relationship to full-space targets
• Proves sample collision falsification: same-bucket label disagreements rule out compatible targets
• Establishes equivalence between sample consistency and existence of fitting quotient rules
• Provides cardinality bounds for search spaces and unobserved bucket assignments
• Formalizes quotient refinement as a preorder and proves product-label consistency

OrdvecFormalization/FiniteQuotientSearch.lean

---

2. OrdvecFormalization/FiniteObservationWindow.lean ✨ Enhancement +366/-0

Generic finite observation windows and target-separating probe families

• Formalizes generic lossy-probe families via joint-code observation maps
• Proves target invariance is equivalent to kernel containment for observation families
• Introduces finite prefix windows of countable observation streams
• Establishes finite existence theorem: target-sufficient window exists iff every target-disagreeing
 pair is eventually separated
• Proves longer windows refine shorter windows and preserve target sufficiency
• Provides sample falsifiers for window-factorized targets

OrdvecFormalization/FiniteObservationWindow.lean

---

3. OrdvecFormalization/QuotientConstraints.lean ✨ Enhancement +155/-0

Generic quotient fiber-invariance and non-identifiability consequences

• Defines fiber invariance: rules constant on quotient fibers
• Proves rules factoring through quotients are fiber-invariant
• Establishes that nontrivial quotient fibers necessarily discard some full-space distinctions
• Shows non-injective quotients fail to preserve some Bool-valued targets
• Proves quotient pullback characterization for Bool rules

OrdvecFormalization/QuotientConstraints.lean

---

View more (17)

4. OrdvecFormalization/FiniteFiberTopology.lean ✨ Enhancement +119/-0

Finite fiber topology and observed bucket structure

• Formalizes finite "clump" structure induced by quotient maps on samples
• Proves observed bucket fibers are pairwise disjoint
• Establishes sample cardinality equals sum of observed fiber sizes
• Characterizes collisions as non-injectivity on samples
• Proves collision existence from cardinality comparison

OrdvecFormalization/FiniteFiberTopology.lean

---

5. OrdvecFormalization/FiniteQuotientImage.lean ✨ Enhancement +77/-0

Reachable image quotients for finite compression maps

• Restricts quotient reasoning to reachable image of finite compression maps
• Defines image quotient as surjective by construction
• Introduces fiber, observed/unobserved buckets, fiber size, and collision definitions
• Proves image quotient surjectivity without assuming full codomain coverage

OrdvecFormalization/FiniteQuotientImage.lean

---

6. OrdvecFormalization/QuotientKernel.lean ✨ Enhancement +84/-0

Quotient kernels and target-safe compression characterization

• Defines kernel relation for compression maps and target kernels
• Proves kernel containment equivalence to fiber invariance
• Establishes image-quotient factorization iff kernel containment
• Provides bidirectional theorems for building/extracting kernel containment

OrdvecFormalization/QuotientKernel.lean

---

7. OrdvecFormalization/QuotientRefinementKernel.lean ✨ Enhancement +78/-0

Quotient refinement via kernel inclusion relations

• Characterizes quotient refinement as kernel inclusion
• Proves refinement builds from kernel subset when fine quotient is surjective
• Establishes equivalence for surjective fine quotients
• Applies results to image quotients

OrdvecFormalization/QuotientRefinementKernel.lean

---

8. OrdvecFormalization/FinitePairQuotient.lean ✨ Enhancement +73/-0

Product quotients for pairwise retrieval decisions

• Defines product quotient for query/document pairs
• Proves pairwise targets factoring through product quotient are invariant on component fibers
• Establishes same-product-quotient label disagreement falsifies pairwise compatible targets

OrdvecFormalization/FinitePairQuotient.lean

---

9. OrdvecFormalization/ScoreMarginQuotient.lean ✨ Enhancement +93/-0

Score margins and threshold admission under approximation

• Defines two-sided uniform score approximation bounds
• Proves threshold margins separate decisions from approximation error
• Shows close approximate scores with sufficient margins give identical threshold decisions
• Proves quotient-factorized scores yield quotient-factorized Boolean thresholds
• Establishes threshold rules factor through image quotients under margin conditions

OrdvecFormalization/ScoreMarginQuotient.lean

---

10. OrdvecFormalization/ProfileStability.lean ✨ Enhancement +126/-0

Profile-stability certificates for encoder distortion and quotient geometry

• Packages encoder-distortion and quotient-geometry profiles as formal finite certificates
• Proves uniform score-error bounds compose additively
• Establishes composed profile error gives source-to-quotient score bound
• Shows threshold admission unchanged by quotient score under composed profile
• Proves threshold rule factors through reachable quotient image under profile assumptions
• Derives kernel containment from distortion and quotient geometry profiles

OrdvecFormalization/ProfileStability.lean

---

11. OrdvecFormalization/Verify.lean ⚙️ Configuration changes +232/-0

Wire new modules into verification and public checks

• Adds imports for all new quotient/window/profile modules
• Extends public verification checks with 140+ new theorem names
• Adds axiom audits for all new theorems

OrdvecFormalization/Verify.lean

---

12. OrdvecFormalization.lean ⚙️ Configuration changes +10/-0

Wire quotient/window/profile layers into root module

• Adds imports for FiniteQuotientSearch, QuotientConstraints, FiniteQuotientImage
• Adds imports for QuotientKernel, FiniteFiberTopology, FinitePairQuotient
• Adds imports for QuotientRefinementKernel, FiniteObservationWindow, ScoreMarginQuotient,
 ProfileStability

OrdvecFormalization.lean

---

13. docs/theorem-map.md 📝 Documentation +281/-5

Document quotient/window/profile theorem surface and dependencies

• Updates main claim description to include quotient-search, window, and profile layers
• Adds comprehensive theorem listings for finite quotient search layer (45+ theorems)
• Adds quotient constraint layer theorems (25+ theorems)
• Adds image/kernel/fiber/pair/refinement/margin/profile theorems (60+ theorems)
• Updates module dependency graph to show new layer structure
• Expands public Lean-name surface with 140+ new names
• Adds compatibility notes clarifying finite/conditional boundaries for new layers

docs/theorem-map.md

---

14. README.md 📝 Documentation +13/-0

Document quotient-search and observation-window empirical scope

• Adds section explaining quotient-search empirical burden and target-separation condition
• Updates main results to include finite quotient-search constraints and observation-window theorems
• Clarifies that concrete probe families are not proved globally sufficient without finite evidence

README.md

---

15. docs/reviewer-brief.md 📝 Documentation +12/-0

Document quotient-search and window layers in reviewer brief

• Adds descriptions of FiniteQuotientSearch.lean, FiniteQuotientImage.lean,
 QuotientKernel.lean
• Adds description of FiniteObservationWindow.lean with target-invariance and refinement
• Extends "What Is Not Claimed" section with probe-family and target-invariance caveats
• Adds audit guidance for same-joint-code label disagreements

docs/reviewer-brief.md

---

16. docs/rag-pipeline-guide.md 📝 Documentation +6/-0

Add multi-probe joint-code audit guidance to RAG pipeline

• Adds guidance on multi-probe systems and joint-code auditing
• Explains same-joint-code relevance disagreements as finite falsifiers
• Clarifies probe-bundle safety conditions before treating as first-stage gate

docs/rag-pipeline-guide.md

---

17. docs/paper/README.md 📝 Documentation +19/-0

Add formalization paper artifact documentation

• New file documenting formalization paper artifacts and rebuild instructions
• Lists tracked artifacts: TeX source, rendered PDF, text extract
• Provides LaTeX build commands

docs/paper/README.md

---

18. docs/paper/ordvec_formalization_paper.tex 📝 Documentation +1291/-0

Add comprehensive formalization paper with theorem narrative

• Added comprehensive 1291-line LaTeX formalization paper documenting finite quotient sufficiency,
 search constraints, profile stability, and bitmap overlap calibration
• Includes abstract, proof roadmap, and detailed sections on finite experiments, quotient contracts,
 search reduction, kernel containment, windowed observations, score margins, ordered evidence, and
 bitmap theorems
• Provides complete bibliography with verified foundational references (Fisher, Halmos–Savage, Wald,
 Blackwell, Karlin–Rubin, Devroye–Györfi–Lugosi, de Moura–Ullrich, mathlib)
• Explicitly documents non-claims and boundary conditions to preserve finite, conditional nature of
 theorems

docs/paper/ordvec_formalization_paper.tex

---

19. docs/paper/ordvec_formalization_paper.txt 📝 Documentation +948/-0

Add plain-text extraction of formalization paper

• Added 948-line plain-text extraction of the LaTeX formalization paper for accessibility and RAG
 indexing
• Preserves all mathematical content, theorem statements, section structure, and bibliography from
 the TeX source
• Removes LaTeX formatting while maintaining semantic structure and reference integrity

docs/paper/ordvec_formalization_paper.txt

---

20. docs/proof-spine.md 📝 Documentation +127/-20

Expand proof-spine with quotient and window layer modules

• Expanded proof-spine roadmap to include 11 new intermediate modules between FiniteExperiment and
 FiniteBayesRisk
• Added detailed descriptions for FiniteQuotientSearch, QuotientConstraints,
 FiniteQuotientImage, QuotientKernel, FiniteFiberTopology, FinitePairQuotient,
 QuotientRefinementKernel, FiniteObservationWindow, ScoreMarginQuotient, and ProfileStability
• Updated dependency graph to reflect new module ordering and relationships
• Renumbered subsequent modules (e.g., FiniteBayesRisk from 2 to 12, OrdinalSufficiency from 3
 to 13)

docs/proof-spine.md

---

[qodo-code-review]

Code Review by Qodo

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

Great, no issues found!

Qodo reviewed your code and found no material issues that require review

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: fdc50b1373

ℹ️ 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 (@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 (@codex) address that feedback".

[Copilot]

Pull request overview

This PR extends the OrdvecFormalization codebase with a new “quotient search / reachable image / kernel / windowed probes / profile stability” layer, and updates the public verification surface and documentation (including a LaTeX paper draft) to reflect the expanded theorem surface.

Changes:

• Add new Lean modules for quotient search constraints, reachable-image/kernel reasoning, finite fiber topology, pair quotients, refinement-by-kernel, observation windows, and score-margin/profile-stability theorems.
• Wire the new modules into the root import and Verify.lean public API/axiom auditing dashboard.
• Update repo docs (README, theorem map, proof spine, reviewer brief, RAG guide) and add a docs/paper/ directory with the paper source + extracted text.

Reviewed changes

Copilot reviewed 21 out of 22 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
README.md	Updates repository claims/boundaries to include quotient-search and windowed-probe layers.
OrdvecFormalization.lean	Imports the newly added quotient/window/profile modules into the root module.
OrdvecFormalization/Verify.lean	Extends the public API verification dashboard with #check/#print axioms for the new layers.
OrdvecFormalization/FiniteQuotientSearch.lean	Adds finite sample consistency, falsifiers, bucket-level rule extension, counting, and refinement/product lemmas.
OrdvecFormalization/QuotientConstraints.lean	Adds generic fiber-invariance and non-identifiability consequences of quotient factorization.
OrdvecFormalization/FiniteQuotientImage.lean	Introduces reachable-image quotients and basic fiber/bucket vocabulary.
OrdvecFormalization/QuotientKernel.lean	Defines kernels/target-kernels and proves kernel containment ↔ image-quotient factorization.
OrdvecFormalization/FiniteFiberTopology.lean	Adds sample fiber “clump” theorems, collision/injectivity characterizations, and counting identities.
OrdvecFormalization/FinitePairQuotient.lean	Adds product quotients for query/document style pair reasoning and sample falsifier.
OrdvecFormalization/QuotientRefinementKernel.lean	Connects quotient refinement to kernel inclusion (with surjectivity/image-quotient specializations).
OrdvecFormalization/FiniteObservationWindow.lean	Adds observation-family/window joint-code API, target-invariance characterizations, refinement monotonicity, and finite separating-window existence results.
OrdvecFormalization/ScoreMarginQuotient.lean	Adds score-approximation + margin-stability theorems for threshold admission and image-quotient factorization.
OrdvecFormalization/ProfileStability.lean	Packages distortion/geometry “certificates” and composes them into threshold equality/factorization/kernel containment.
docs/theorem-map.md	Expands theorem map to include quotient-search/window/profile layers and updates public-name list.
docs/proof-spine.md	Updates proof narrative/dependency spine to incorporate the new layers.
docs/reviewer-brief.md	Updates reviewer guidance to mention the new modules and empirical falsifier checks.
docs/rag-pipeline-guide.md	Adds joint-code (“multi-probe”) guidance and falsifier framing for practical auditing.
docs/paper/README.md	Adds build instructions and artifact list for the formalization paper directory.
docs/paper/ordvec_formalization_paper.tex	Adds the LaTeX paper draft capturing the checked theorem surface and boundaries.
docs/paper/ordvec_formalization_paper.txt	Adds extracted text for review/search of the paper content.
docs/paper/.gitignore	Ignores LaTeX intermediate build artifacts in docs/paper/.

---

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

[Fieldnote-Echo]

Review-response update pushed in 7e198a4.

What changed:

• Corrected unobserved-bucket counting to use reachable image buckets via UnobservedReachableQuotients, so unreachable ambient codomain values no longer inflate induced full-target uncertainty.
• Switched ScoresWithin, ThresholdMargin, and profile error budgets to ℝ≥0.
• Changed the finite window existence theorems from an explicit hfin : Fintype Ω argument to a finite typeclass ([Finite Ω]) to avoid threading instance values while staying warning-clean under --wfail.
• Updated Verify.lean, theorem map, proof spine, and rebuilt the paper PDF/text extract so the paper reflects these latest proof additions.

Validation run locally:

• make build
• make verify
• make check-doc-names
• make audit
• make lint
• latexmk -pdf -interaction=nonstopmode -halt-on-error ordvec_formalization_paper.tex
• pdftotext ordvec_formalization_paper.pdf ordvec_formalization_paper.txt
• strict LaTeX log scan for warnings/errors/unresolved refs/overfull/underfull boxes
• git diff --check