chore(repository): improve documentation and CI

[quangvdao]

Summary

This PR improves repository maintenance and makes PolyFun easier to use.

It:

• removes stale copied version numbers and treats lean-toolchain and lakefile.toml as the version sources of truth;
• adds a compiled polynomial functor example to the README;
• publishes searchable API documentation through GitHub Pages;
• removes the unused automatic PR summary workflow;
• pins every external GitHub Action to a full commit hash;
• reduces validation workflow permissions;
• runs style linting on every pull request so it can safely become a required check;
• moves four source TODOs into issues feat(ipfunctor): add equivalence bridges #117 through refactor(pfunctor): simplify universe annotations #120.

Diff metadata

• Base: 31216a8f561d4259a5845a933e6e8b6c2e3d5e89 (main)
• Head: 00e782dc2818b78c57beb41cd308fd7452658573
• Commits: 3
• Files changed: 16
• Diff: 89 insertions and 108 deletions

Motivation

The repository documentation named three obsolete dependency versions. The automatic PR summary also ran on every pull request only to report that its missing key caused it to skip. Public declarations had no searchable API site, and several action dependencies used mutable version tags.

Change overview

Area	Before	After
Version guidance	Copied version numbers became stale	Toolchain files are the only source of truth
First example	No runnable example in the README	A checked constant polynomial example and command
API documentation	No published declaration index	docgen-action publishes from main
PR summary	A disabled check ran on every PR	The unused workflow is removed
Action dependencies	Several actions used mutable tags	Every external action uses a full commit hash
CI permissions	The build job could write issues and PRs	The build job has read access to contents only
Style check	Path filters could omit the check	The check runs on every PR and push to main
Source TODOs	Design work lived in comments	Issues #117 through #120 record scope and acceptance criteria

API documentation

.github/workflows/docs.yml builds PolyFun and publishes doc-gen4 output after pushes to main. GitHub Pages has been enabled with GitHub Actions as its deployment source. The generated API will be available at https://verified-zkevm.github.io/PolyFun/docs/ after this PR merges and the first deployment succeeds.

Workflow security

All external actions now use immutable commit hashes with readable version comments. The normal build job no longer receives issue or pull request write access. The on-demand /review workflow remains restricted to comments from repository owners, members, or collaborators.

Tracked follow-up work

• feat(ipfunctor): add equivalence bridges #117 adds the missing indexed equivalence bridges.
• refactor(monad): settle morphism hierarchy #118 settles the monad morphism and equivalence hierarchy.
• refactor(pfunctor): derive product distribution #119 reviews the canonical product distribution construction.
• refactor(pfunctor): simplify universe annotations #120 simplifies universe annotations in lifting equivalences.

Validation completed at 00e782d

The following passed:

• lake env lean /tmp/PolyFunReadmeExample.lean
• python3 ./scripts/check-docs-integrity.py
• ./scripts/check-imports.sh
• actionlint
• git diff --check
• full ./scripts/validate.sh --lint --test, including 2,010 library build jobs and 2,056 test build jobs
• repository scan confirming that every external action reference uses a full 40 character commit hash
• all six required pull request checks on the exact head commit

The first GitHub Pages deployment can run only after the documentation workflow reaches main.

Breaking changes

There are no Lean API or dependency changes.

Reviewer map

Suggested review order:

1. .github/workflows/docs.yml
2. .github/workflows/ci.yml and .github/workflows/linting.yml
3. the remaining pinned workflow references and removal of summary.yml
4. README.md, AGENTS.md, and the wiki changes
5. the four removed TODO comments and linked issues