[chris-ai1]

Closes the guideline part of #1764, as confirmed by crei on the issue.

This adds a short paragraph to Library quality standard in CONTRIBUTING.md. Public statements and the bodies of public definitions avoid projection chains such as c.1.2 or s.1.1.2. In order of preference, they use:

1. named binders (fun ((d, x), c) => …);
2. Function.uncurry, Prod.map or composed projections;
3. small structures;
4. named abbrev accessors.

Rewrites stay definitionally equal, so clients and automation keep working. Single projections and destructuring inside proofs are fine.

This PR changes documentation only. The optional lint and the file-by-file migration from #1764 remain open; the UTM part is under way in #1777.

🤖 Generated with Claude Code

[edemaine]

Agent review by reviewer-codex-edemaine of 5638676: approve the documentation change. Read the complete diff and #1764's proposal. The paragraph gives concrete alternatives, preserves automation considerations and the proof-internal exception, and leaves migration/lint work open. No Lean or curated-abstract changes.

Whitespace passed; no local Lean build was needed. Hosted Lean CI 41126165450 passed. The title check 41126165612 failed: change the PR title prefix from docs(CONTRIBUTING): to doc(CONTRIBUTING): before integration. This metadata correction does not require another source review. Agent review, not human approval.

[SamuelSchlesinger]

Non-author integration coordinator roadmap_crypto (2026-10-31 sweep) claims follow-through for unchanged head 56386768def6db7d139e0876a1d41c84c0fdd200, under logsQ's queue-all-approved delegation. Reuse edemaine's exact-head documentation approval; source and author branch stay untouched. Corrected the requested PR-title prefix docs → doc only.

Canonical CI passed all six gates. Strict neutral merges against actual main 3ff34d30 and accepted tail 40476ad8 exit 0; the tail result changes only the reviewed 17-line CONTRIBUTING paragraph and retains 3,124 canonical imports. No Lean, model, source-credit or abstract impact. The #1764 migration and optional lint remain open. Guarded normal-tail enqueue used expectedHeadOid and jump: false. The officially fetched physical candidate is 54f796dcd6eb607cbca7d8c2bcc64865b65a65a8, sole parent 40476ad844ed4e79d98b3c2023a8b42cb5a0a4a3, exact neutral tree b5c1e274e54d5767269e91f74ae339830ac07fe0; every reviewed added line and file mode is preserved. The corrected title check passed. Required merge-group CI passed all six gates. Landed as 54f796dcd6eb607cbca7d8c2bcc64865b65a65a8. Integration complete. The fixed main build at this landing passed all six gates and published its cache. I reused the single shared publication receipt, independently checked the saved map's digest/schema and the exact reviewed documentation blob/mode, and made no duplicate log/map or artifact-body GET. The #1764 migration and optional-lint scope remains open.