[codex] polish docs and guard theorem names

[Fieldnote-Echo]

What changed

• Reworked README.md into a concise front door focused on why the theorem matters.
• Moved the module-by-module proof narrative into docs/proof-spine.md.
• Kept docs/theorem-map.md as the stable checked-name surface and clarified the conceptual dependency stack.
• Tightened reviewer-facing wording around symmetry, MLR/Bayes optimality, and bitmap-null calibration.
• Added make check-doc-names, which extracts documented OrdvecFormalization.* names and theorem-map public names, then checks they resolve in Lean.
• Wired the documented-name guard into CI.

Issue coverage

Closes #5 by pinning the public-name surface and adding a docs-to-source name guard. The direct headline axiom audit is already present in Verify.lean.

Validation

• make build
• make verify
• make check-doc-names
• make audit
• make lint

[gemini-code-assist]

Code Review

This pull request refactors and simplifies the documentation (specifically README.md and docs/theorem-map.md) by moving the detailed proof descriptions into a new docs/proof-spine.md file. It also introduces a Python verification script (scripts/check_doc_names.py) and a corresponding Makefile target to ensure that all documented Lean theorem names resolve correctly. The review feedback focuses on improving the robustness of the Python script, specifically by dynamically parsing markdown sections instead of relying on hardcoded headers, and utilizing a temporary directory context manager to prevent potential file leaks.

[qodo-code-review]

Review Summary by Qodo

Polish docs and add theorem-name verification guard

📝 Documentation ✨ Enhancement

Walkthroughs

Description

• Restructured README into concise front door with "Why This Matters" section
• Moved detailed proof narrative to new docs/proof-spine.md module guide
• Added make check-doc-names Python script to guard documented theorem names
• Integrated documentation-name verification into CI pipeline
• Clarified three-part proof structure: symmetry, decision theory, null calibration

Diagram

flowchart LR
  README["README.md<br/>Concise front door"]
  ProofSpine["docs/proof-spine.md<br/>Module narrative"]
  TheoremMap["docs/theorem-map.md<br/>Public names surface"]
  CheckScript["scripts/check_doc_names.py<br/>Name verification"]
  CI["CI Pipeline<br/>check-doc-names step"]
  
  README --> ProofSpine
  README --> TheoremMap
  CheckScript --> CI
  TheoremMap --> CheckScript

Loading

File Changes

1. README.md 📝 Documentation +45/-256

Streamline README to concise front door

• Condensed from 280 to 67 lines with focused "Why This Matters" section
• Removed verbose proof spine details (moved to docs/proof-spine.md)
• Simplified theorem listings and scope clarifications
• Added cross-references to docs/theorem-map.md, docs/proof-spine.md, and
 docs/reviewer-brief.md
• Clarified task-relative decision sufficiency vs representation completeness

README.md

---

2. docs/proof-spine.md 📝 Documentation +142/-0

New module-by-module proof narrative guide

• New file: 142 lines of module-by-module proof narrative
• Explains conceptual stack from observations through quotient to threshold to calibration
• Documents dependency shape and import order distinctions
• Provides detailed descriptions of all 15 modules in the formalization
• Includes reviewer check commands and expected axiom baseline

docs/proof-spine.md

---

3. docs/theorem-map.md 📝 Documentation +15/-142

Refactor theorem-map to focus on public names

• Removed 130+ lines of detailed proof spine (now in docs/proof-spine.md)
• Simplified dependency shape diagram with cross-reference to proof-spine
• Added "Public Names" section header with stability note
• Updated reviewer check commands to include make check-doc-names
• Clarified that make verify checks public theorem dashboard

docs/theorem-map.md

---

View more (4)

4. docs/reviewer-brief.md 📝 Documentation +11/-5

Clarify proof structure and update checks

• Clarified three-part proof separation: symmetry, decision theory, null calibration
• Refined engineering consequence wording from "approximately true" to "empirically validated"
• Changed "full-score computation" to "arbitrary accept/reject rule"
• Added make check-doc-names to reviewer check commands

docs/reviewer-brief.md

---

5. scripts/check_doc_names.py ✨ Enhancement +91/-0

New Python script to guard documented names

• New Python script: 91 lines for verifying documented theorem names
• Extracts OrdvecFormalization.* names from markdown files via regex
• Extracts public surface names from docs/theorem-map.md "Public Names" section
• Generates temporary Lean file with #check statements for all names
• Runs lake env lean to verify names resolve; reports failures with diagnostics

scripts/check_doc_names.py

---

6. Makefile ⚙️ Configuration changes +5/-2

Add check-doc-names target to build system

• Added check-doc-names to .PHONY targets
• New check-doc-names target runs python3 scripts/check_doc_names.py
• Updated audit target to include scripts directory in sorry/sorryAx search

Makefile

---

7. .github/workflows/lean_action_ci.yml ⚙️ Configuration changes +3/-0

Integrate documentation-name check into CI

• Added new CI step "Check documented theorem names" after verify step
• Runs make check-doc-names to guard theorem-name surface in CI
• Positioned before audit step in workflow sequence

.github/workflows/lean_action_ci.yml

---

[qodo-code-review]

Code Review by Qodo

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

1. Dotted names mis-parsed ✓ Resolved 🐞 Bug ≡ Correctness

Description

scripts/check_doc_names.py only captures the first identifier after OrdvecFormalization.; a
documented name like OrdvecFormalization.Foo.bar would be reduced to Foo, causing the guard to
check the wrong thing (or fail) and undermining the docs↔source drift protection.

Code

scripts/check_doc_names.py[R22-23]

Evidence

QUALIFIED_RE stops at the first identifier segment, so any additional .segment is not captured;
the script then emits #check @{name} for whatever was captured, meaning it will check Foo rather
than Foo.bar for a doc reference OrdvecFormalization.Foo.bar. The codebase also contains dotted
OrdvecFormalization.<Module> references in doc-like commentary, making this limitation likely to
matter over time.

scripts/check_doc_names.py[22-31]
scripts/check_doc_names.py[44-53]
OrdvecFormalization/OverlapNull.lean[13-20]

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 documented-name extractor only matches a single identifier segment after `OrdvecFormalization.` and cannot handle namespaced declarations (e.g. `OrdvecFormalization.BitmapNull.someLemma`). This can lead to checking the wrong name (only the first segment) and missing/incorrectly reporting docs↔source drift.

### Issue Context
The repo already uses dotted `OrdvecFormalization.<Module>` references in doc-like text (e.g. module mentions), and it’s plausible markdown may eventually cite namespaced declarations.

### Fix Focus Areas
- Update the regex to capture dotted names (multiple `.<ident>` segments) safely.
- Consider also allowing dots in the backtick extraction regex for future-proofing.
- Keep the Lean `#check` generation compatible with dotted names.

### Fix Focus Areas (code references)
- scripts/check_doc_names.py[22-23]
- scripts/check_doc_names.py[44-53]

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

---

2. Brittle section delimiter ✓ Resolved 🐞 Bug ☼ Reliability

Description

public_surface_names() hard-codes ## What Is Not Claimed as the end of the Public Names block; a
harmless docs heading rename/reorder will break CI even if the listed theorem names are still
correct.

Code

scripts/check_doc_names.py[R34-41]

Evidence

The script explicitly searches for ## Public Names and then for the literal string `## What Is Not
Claimed` to bound the slice; the theorem-map file currently contains those headings, but this
coupling means a documentation-only restructure will break the check and block merges.

scripts/check_doc_names.py[34-41]
docs/theorem-map.md[119-208]

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 theorem-map parsing depends on an exact heading string (`## What Is Not Claimed`) to terminate extraction of public names. Changing that heading text or moving sections will raise and fail CI unnecessarily.

### Issue Context
`docs/theorem-map.md` is explicitly being edited as part of this PR, so future doc refactors are plausible.

### Fix Focus Areas
- Extract the `## Public Names` section by finding the next markdown H2 heading (`^## `) after it, instead of requiring a specific end heading.
- Optionally validate that the extracted block contains at least N bullet items to catch structural mistakes without pinning to a specific heading title.

### Fix Focus Areas (code references)
- scripts/check_doc_names.py[34-41]
- docs/theorem-map.md[119-208]

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

---

[Copilot]

Pull request overview

This PR polishes user-facing documentation and adds a CI guard that the public theorem names cited in the markdown actually resolve in Lean, addressing issue #5's request to pin the public-name surface and prevent docs↔source drift.

Changes:

• Slimmed README.md to a concise front door and moved the module-by-module narrative to a new docs/proof-spine.md; clarified the conceptual dependency stack in docs/theorem-map.md and tightened reviewer wording in docs/reviewer-brief.md.
• Added scripts/check_doc_names.py which extracts OrdvecFormalization.<name> references from the docs plus backticked names in the theorem-map "Public Names" section and #checks them via lake env lean.
• Wired the new check into the Makefile (make check-doc-names), extended make audit to also scan scripts/, and added a CI step that runs the guard.

Reviewed changes

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

Show a summary per file

File	Description
README.md	Rewritten as a short overview that links out to the theorem-map, proof-spine, and reviewer brief.
docs/theorem-map.md	Tightened dependency diagram, removed inline proof-spine prose (now in docs/proof-spine.md), marked Public Names as a stable surface, and documented the new check.
docs/proof-spine.md	New file holding the module-by-module proof narrative previously in the README.
docs/reviewer-brief.md	Reframed claims into symmetry / decision theory / null calibration; sharpened the engineering takeaway; added make check-doc-names to the reviewer checks.
scripts/check_doc_names.py	New script that gathers documented names and #checks them in a temporary Lean file under lake env lean.
Makefile	Adds check-doc-names target and includes scripts/ in the audit sorry grep.
.github/workflows/lean_action_ci.yml	Runs make check-doc-names after make verify.

---

💡 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: cc4b07a342

ℹ️ 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]

Addressed the name-guard bot findings in 3527f2d.

• scripts/check_doc_names.py now captures dotted Lean names after OrdvecFormalization. and in the theorem-map public-name block.
• The Public Names extraction now ends at the next markdown H2 heading instead of depending on the literal ## What Is Not Claimed section title.
• Generated Lean checks now use fully qualified names, e.g. #check @OrdvecFormalization.<name>, from the root namespace.
• The temporary check file now lives in a TemporaryDirectory context so cleanup is exception-safe.

Validated with make build, make verify, make check-doc-names, make audit, and make lint.