docs: presentation & navigation for newcomers (Phase 4)

[DrMurphyIsIn]

Phase 4 (presentation & navigation) of the public-release-prep effort. Makes the repo legible to a first-time mathematician/reviewer and gives Telperion the onboarding docs it lacked. No code or mathematics changed; all internal links verified to resolve.

README

• CI status badges (proof-lean, proof-verify, telperion-lean-e2e) — the at-a-glance "the kernel check is green" signal a math reviewer looks for first.
• A scannable TL;DR that states what this is, that the conjecture is not claimed proved, and routes the visitor to STATUS.md (proven-vs-open), the verify section, and Telperion getting-started.

New Telperion docs

• telperion/docs/GETTING_STARTED.md — install → generate → and, crucially, verify the emitted Lean locally end-to-end (pinned leanprover/lean4:v4.32.0, lake exe cache get for the Mathlib cache, lake build). The audit flagged this local-verification path as the single biggest doc gap: generating .lean was documented; checking it was not.
• telperion/docs/ARCHITECTURE.md — the untrusted-generator/trusted-kernel model, the certify → validate → emit → freeze pipeline, the emitter catalog, the self-verification layer, and the enforced engine vs. bg/ research-lab boundary (which test_core_boundary.py guards).
• telperion/CONTRIBUTING.md — how to add a certificate shape, including the mandatory emitter-sensitivity stance (the gate that caught the unclassified emitters in Phase 0), the manifest entry, and the CI gates.
• telperion/README.md — a "New to Telperion?" pointer to the three docs above.

Notes

• Several audit-flagged items were already resolved on main and needed no change: the README already says "Fifty-plus shapes" (the stale "64" is gone) and does not misuse "skill" as a subsystem.
• Like the other doc PRs in this series, this is gated on fix(ci): green main — dvp_atoms manifest, RH emitter stances, sympy-1.12 + lake-skip fixes #231 landing (it inherits the pre-dvp_atoms red main until fix(ci): green main — dvp_atoms manifest, RH emitter stances, sympy-1.12 + lake-skip fixes #231 greens it); its own content is docs-only.

🤖 Generated with Claude Code