[codex] restore decision sufficiency README framing

[Fieldnote-Echo]

What changed

• Restored the decision-sufficiency-not-representation-completeness paragraph near the top of the README.
• Added a no-sorry badge linked to CI.
• Made the build instructions explicitly note that make build runs lake build --wfail.
• Adjusted make audit so Lean sources are checked for proof placeholders while README prose can contain the no-sorry badge text.

Validation

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

[gemini-code-assist]

Code Review

This pull request updates the Makefile to split the audit checks, ensuring that �sorry� is only checked in Lean source files while allowing it in documentation and scripts. It also updates the README.md with a new badge, a conceptual explanation of decision sufficiency, and clarifications on the build process. A review comment points out a potential issue where the use of ! rg in the Makefile could silently succeed if rg is not installed, and suggests explicitly verifying its availability.

[qodo-code-review]

Review Summary by Qodo

Restore decision sufficiency framing and improve build documentation

✨ Enhancement 📝 Documentation

Walkthroughs

Description

• Restored decision-sufficiency framing paragraph to README
• Added "No sorry" CI badge linked to audit workflow
• Clarified build instructions for make build and --wfail flag
• Separated audit checks to exclude README prose from sorry detection

Diagram

flowchart LR
  A["README.md"] -->|"Add decision sufficiency paragraph"| B["Enhanced documentation"]
  A -->|"Add no-sorry badge"| B
  C["Makefile"] -->|"Split audit checks"| D["Lean sources only for sorry"]
  C -->|"Clarify build instructions"| E["Updated build docs"]

Loading

File Changes

1. README.md 📝 Documentation +13/-1

Restore decision sufficiency framing and badges

• Added "No sorry" badge linked to CI workflow
• Restored decision-sufficiency-not-representation-completeness paragraph explaining the theoretical
 scope
• Clarified that make build runs lake build --wfail
• Added explanation of --wfail flag and separate audit checks

README.md

---

2. Makefile ⚙️ Configuration changes +2/-1

Separate audit checks for sources and prose

• Split audit target into two separate checks
• First check searches for sorry and sorryAx only in Lean source files
• Second check searches for sorryAx only in README and documentation files

Makefile

---

[qodo-code-review]

Code Review by Qodo

🐞 Bugs (2) 📘 Rule violations (0)

1. Audit masks rg errors 🐞 Bug ☼ Reliability

Description

The audit target uses shell negation (! rg ...), which treats *any* non-zero ripgrep exit
(including real errors like missing paths or missing rg) as success, so make audit can pass even
when the audit did not actually run. This can produce false-green CI and an incorrect “audited”
signal.

Code

Makefile[R13-14]

Evidence

The Makefile shows audit implemented with ! rg ..., meaning any non-zero rg exit status is
treated as success by the shell, so errors from rg are not surfaced as audit failures.

Makefile[12-14]

Agent prompt

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

### Issue description
`make audit` currently uses `! rg ...`, which inverts ripgrep’s exit code and cannot distinguish “no matches” (exit 1) from “command error” (exit 2/127). This can cause the audit step to succeed even when ripgrep failed to run correctly.

### Issue Context
`rg` exit codes:
- `0`: matches found (audit should fail)
- `1`: no matches (audit should pass)
- `>=2`: error (audit should fail)

### Fix Focus Areas
- Makefile[12-15]

### Suggested change
Replace `! rg ...` with an explicit exit-code check, e.g.:

```make
  a rg -n 'PATTERN' path...; test $$? -eq 1
```

This passes only when `rg` returns 1, and fails on matches (0) or real errors (>=2).

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

---

2. Docs sorry audit weakened 🐞 Bug ⚙ Maintainability

Description

make audit no longer searches docs/ and scripts/ for standalone sorry occurrences (it only
scans those paths for sorryAx), reducing the audit’s ability to catch copied Lean snippets or
other placeholder text outside the compiled Lean sources. This diverges from the previous behavior
where docs/ and scripts/ were also checked for \bsorry\b.

Code

Makefile[14]

Evidence

The audit target’s second rg invocation searches README.md docs scripts for sorryAx only,
meaning \bsorry\b is no longer checked in those paths.

Makefile[12-14]

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 updated audit only checks `README.md docs scripts` for `sorryAx`, not for standalone `sorry`, which reduces audit coverage in non-Lean directories compared to the previous single command.

### Issue Context
If the intent is only to exempt README prose (e.g., the “No sorry” badge text) while keeping docs/scripts guarded, split the checks so:
- Lean sources: `\bsorry\b|sorryAx`
- docs/scripts: `\bsorry\b|sorryAx`
- README: optionally only `sorryAx` (or skip README entirely)

### Fix Focus Areas
- Makefile[12-15]

### Suggested change
Example (also compatible with the exit-code fix in the other finding):

```make
  rg -n '\bsorry\b|sorryAx' OrdvecFormalization OrdvecFormalization.lean; test $$? -eq 1
  rg -n '\bsorry\b|sorryAx' docs scripts; test $$? -eq 1
  rg -n 'sorryAx' README.md; test $$? -eq 1
```

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

---

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 06447f62de

ℹ️ 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".

[chatgpt-codex-connector]

Keep plain sorry audit for docs and scripts

With this narrowed check, plain sorry is no longer audited in docs or scripts; only sorryAx is. In this repo the documentation contains Lean fenced blocks that are not compiled by make check-doc-names beyond extracting theorem names, so a future documented snippet such as by sorry would pass CI while the README now advertises the no-sorry audit. The README badge text needs an exception, but broadening that exception to all docs/scripts weakens the placeholder guard.

Useful? React with 👍 / 👎.