[codex] Add calibrated evidence layer#9
Conversation
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request refactors the formalization by modularizing several components. It introduces FiniteBayesRisk.lean to house Bayes-risk wrappers, CalibratedEvidence.lean to package ordered-tail calibration with Bayes-optimal cutoffs, and BitmapIncidence.lean to isolate constant-weight bitmap definitions and bridges. BitmapCalibration.lean is refactored to utilize these new modules, and corresponding updates are made to the verification checks and documentation. There are no review comments to address, and the changes appear clean and well-structured.
Review Summary by QodoAdd calibrated evidence layer with modular bitmap incidence and Bayes-risk separation
WalkthroughsDescription• Add graph-neutral CalibratedEvidence layer pairing Bayes-optimal cutoff with supplied calibration equality • Split finite Bayes-risk wrappers into dedicated FiniteBayesRisk module while preserving backward compatibility • Extract bitmap incidence definitions into narrower BitmapIncidence module for better separation of concerns • Refactor BitmapCalibration proofs to use supplied calibration layer without changing public theorem statements • Update documentation, proof spine, reviewer brief, and theorem map for new module boundaries Diagramflowchart LR
FE["FiniteExperiment"]
FBR["FiniteBayesRisk"]
OS["OrdinalSufficiency"]
CE["CalibratedEvidence"]
BI["BitmapIncidence"]
BC["BitmapCalibration"]
OBO["OverlapBayesOptimal"]
FE --> FBR
FE --> OS
FBR --> CE
OS --> CE
BI --> BC
CE --> BC
OBO --> BC
FE -.->|backward compat| OBO
File Changes1. OrdvecFormalization.lean
|
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 |
There was a problem hiding this comment.
Pull request overview
This PR introduces a graph-neutral “calibrated evidence” layer that lets downstream results pair an ordered Bayes-optimal cutoff with an explicitly supplied ordered-tail calibration equality, while also refactoring bitmap incidence and Bayes-risk wrappers into narrower modules and keeping legacy import paths working.
Changes:
- Added
CalibratedEvidence(OrderedTailCalibration+ existence theorems returning a Bayes-optimal cut together with the supplied equality at that cut). - Split out
FiniteBayesRiskwrappers and constant-weight bitmap incidence infrastructure into dedicated modules, updating imports/verification while preserving legacy aggregate imports. - Refactored bitmap calibration proofs to route through the new calibrated-evidence layer without changing the public bitmap theorem statements.
Reviewed changes
Copilot reviewed 12 out of 12 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| README.md | Documents the new “supplied calibration packaged with cutoff” concept and why it matters. |
| OrdvecFormalization/VerifyMovedImports.lean | Adds compatibility #checks ensuring moved names remain available via legacy aggregate imports. |
| OrdvecFormalization/Verify.lean | Extends public API verification to include new modules and new calibrated-evidence names/axiom prints. |
| OrdvecFormalization/OverlapBayesOptimal.lean | Removes in-file Bayes-risk wrappers and imports FiniteBayesRisk instead. |
| OrdvecFormalization/FiniteBayesRisk.lean | New module containing finiteBayesRisk / finiteCostedBayesRisk wrappers. |
| OrdvecFormalization/CalibratedEvidence.lean | New module defining OrderedTailCalibration and calibrated-cut existence theorems. |
| OrdvecFormalization/BitmapIncidence.lean | New module containing constant-weight bitmap subtype, uniform law, overlap evidence, and event-bridge lemmas. |
| OrdvecFormalization/BitmapCalibration.lean | Refactors calibration proofs to use CalibratedEvidence + BitmapIncidence, keeping theorem statements stable. |
| OrdvecFormalization.lean | Updates root module imports to include new modules. |
| docs/theorem-map.md | Updates theorem surface map and dependency shape to include calibrated-evidence and incidence layers. |
| docs/reviewer-brief.md | Updates reviewer narrative to distinguish calibrated-evidence from null calibration. |
| docs/proof-spine.md | Updates proof spine/dependency narrative to reflect new module boundaries and calibrated-evidence step. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Summary
CalibratedEvidencelayer that pairs an ordered Bayes-optimal cutoff with a supplied calibration equality.Validation
make buildmake verifymake check-doc-namesmake auditmake lint