[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code, Opus), at Samuel's request: "We want to make sure we aren't introducing bad taste or ugly code into the project just because of some rules, we need to be able to question such rules."

Why. Two rules made code worse during today's work:

• simp only. The rule "non-terminal simp only as simp only" turned short closers like simp [hκ, Key.ofFields]; omega into 6–15-lemma simp only [...] lists (feat(Circuit/Boolean/Tableau): linear-size decoder of the succinct tableau (#1539 M3c) #2088 Decoder/Shape.lean). The checker already accepted simp …; omega on one line but not on two lines, and reviewers read the rule literally.
• Named components (style: avoid positional projection chains (s.1.1.2) in public statements and definitions #1764). The rule produced per-PR exception lists (refactor(Crypto): replace projection chains across protocol modules (#1764) #2005, refactor(Homomorphic): replace projection chains across Homomorphic modules (#1764) #2006, refactor(Crypto): replace projection chains across Signature, Commitment, and Hash modules (#1764) #2007). For automation-keyed certificates, destructuring breaks program_certificate/efficiency-key lookup. In section variables of module files, it elaborates to sorry on the current toolchain (style: avoid positional projection chains (s.1.1.2) in public statements and definitions #1764 comment 6563590976).

Changes

• AGENTS.md, Proof hygiene:
  • A short preamble: the rules serve readability and robustness. When one makes a specific proof or statement worse, deviate, say why, and propose an amendment. Reviewers judge by purpose, not letter.
  • The simp bullet now says why the rule exists: later steps should not depend on a changing simp normal form. A simp closed by omega, linarith, nlinarith, norm_num, ring, grind or tauto counts as terminal. These are tactics that Mathlib's flexible-tactic linter accepts after simp (Mathlib/Tactic/Linter/FlexibleLinter.lean, its flexible set).
• CONTRIBUTING.md:
  • Item 5 is aligned with the new simp bullet.
  • The style: avoid positional projection chains (s.1.1.2) in public statements and definitions #1764 section clarifies that "composed projections" means point-free composition, not respelling p.2.1. It also lists the two standing exceptions: conclusions that automation looks up by head, and section variable hypotheses in module files.
• scripts/check_hygiene.py --check-simp: a bare simp followed only by a finishing tactic that ends its block is no longer flagged. A finishing tactic followed by more tactics, or a rigid follow-up such as rw, is still flagged, and there is a new test for both cases.

This changes repository rules, so Samuel decides. No Lean sources change. Once #2088 lands, a follow-up will restore its short simp …; omega closers.

Existing notions considered: no new definitions.

Validation: python3 -B -m unittest scripts.test_check_hygiene (50 tests) and scripts/check_hygiene.py --check-simp on the whole library pass locally. Hosted CI runs on this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author technical review of fcf5fd88d4c12a1c0cab80a1be09f5d70d14d188, with one nonblocking checker limitation inline.

Read the complete four-file change. The guidance and regression agree on accepting an immediately closing flexible tactic while rejecting later same-block steps. The selected tactic names are in the pinned Mathlib flexible set. The named-component exceptions match the previously reviewed certificate-key behavior and the concrete module/section-variable reproducer in #1764; the latter is a reported toolchain issue, not independently re-elaborated here. No Lean definitions, mathematical/resource statements or abstract claims change. Adoption of the policy wording remains a maintainer decision.

All 50 hygiene tests and the whole-library hygiene/simp scan pass under Cygwin; whitespace checks pass. Native Windows retains the base's diagnostic-separator assertion failures, independently compared against the unchanged formatter. At one inspection, title passed and CI was running. No reviewer Lean build. Agent review, not human approval.

[edemaine]

Nonblocking: this recognizes a tactic-name prefix, so simp at h followed by norm_num at h; exact h on the next line is accepted too. The final exact can still depend on the simplified hypothesis. Consider rejecting rigid tails on that line, or documenting that this remains a line-based heuristic. I do not require a general tactic parser here: the existing same-line simp; ... exemption already has a similar limitation.