Refresh generated project statistics and attribution

[Vilin97]

Regenerates README statistics and NOTICE from the accepted project cards and attribution notes. No proof sources change.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] This metadata-only refresh appears safe to merge.

Summary

Refreshes generated metadata without changing proof sources.

• README statistics now show 300 projects and 11,002,597 lines of Lean.
• NOTICE now lists LiebThirring with its upstream repository.

_{Reviews (1) · Last reviewed commit: "Refresh generated project statistics and..." · Reviewed by Greptile}

[Vilin97]

{
"review": "Permanent reviewer: generated metadata review",
"reviewed_head": "606b340b76e02aa7e48be1823f723691c70c4a16",
"source_verdict": "favorable",
"findings": [],
"summary": "The complete two-file diff adds the accepted LiebThirring project to NOTICE and updates only the delimited README statistics block.",
"coverage": {
"complete_PR_diff": true,
"files": 2,
"Lean_source_changes": 0,
"root": "Reviewed both complete patch hunks, the current stats generator and generated-metadata workflow, and the complete merged PR641 file metadata. No proof/source validation or whole-pool regeneration was repeated.",
"peer": "Independent peer read the complete two-file comparison, whole current stats/NOTICE generators and whole accepted card at main f482. Its Git blob matches the merged card; entry_module, github_repo, Apache-2.0 license and fixed padding yield the exact NOTICE row. Root alone obtained the complete 188-file import metadata. No global recount, build or generation was rerun."
},
"evidence": [
"PR641 at 1a780d4 merged to current base f482bd7. Its complete 188-file metadata contains one added project card and 187 added Lean files, totaling 20,068 added Lean lines.",
"The added card is LeanPool/projects/stability-of-matter.yaml, with entry_module LeanPool.LiebThirring, source.github_repo scottnarmstrong/LiebThirring, and license Apache-2.0. Those fields justify the new NOTICE row in the existing license section.",
"The README arithmetic is exact: 299+1=300 projects and 10,982,529+20,068=11,002,597 Lean lines. The reviewed generator counts registered cards and binary-file lines; this review checks the change against the accepted import rather than independently recomputing the pre-existing totals.",
"No proofs, card declarations, attribution already present, generator implementation, dependency or CI gate are changed."
],
"disposition": {
"state": "MERGED through the protected native queue",
"current_head_CI": {
"run": 38282422520,
"status": "completed",
"conclusion": "success",
"updated_at": "2026-10-12T17:32:27Z"
},
"permanent_reviewer_enqueued": false,
"existing_author_auto_merge_request_consumed": true,
"next_action": "No further action for this unchanged reviewed head. Preserve the accepted source and configured review evidence.",
"configured_review": {
"id": 6129485732,
"head": "606b340b76e02aa7e48be1823f723691c70c4a16",
"verdict": "approve",
"updated_at": "2026-10-12T17:42:56Z",
"body_sha256": "1ddf54958be3c61fee957d0fd4a8103dd8510fdd1e49b3f0601b4a58b056f7cb"
},
"previous_native_queue": {
"id": "MQE_lQDOSY3yXM8AAAABIAxTBs4ABJD4zgM5EUo",
"position": 1,
"state": "AWAITING_CHECKS",
"enqueuedAt": "2026-10-12T17:32:48Z"
},
"merged_at": "2026-10-12T17:50:17Z",
"merge_commit": "f1dde80361e2c9ab3cae58d6be518812d0ac1a4f",
"merge_queue_entry": null,
"merge_group_CI": {
"run": 38284964913,
"head": "f1dde80361e2c9ab3cae58d6be518812d0ac1a4f",
"status": "completed",
"conclusion": "success",
"completed_updated_at": "2026-10-12T17:49:52Z"
}
},
"assessment": {
"scope": "Generated project statistics and attribution refresh",
"introduces_tech_debt": false,
"maintainability": "unchanged",
"brittleness": "unchanged",
"risk": "low",
"assessment_one_sentence": "The exact two-file generated metadata update leaves proof code, generators and build configuration unchanged and adds no maintenance debt."
}
}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 606b340b76e02aa7e48be1823f723691c70c4a16

Verdict: ✅ approve

This PR updates the generated README totals and adds the already registered LiebThirring project to NOTICE. The full diff changes only metadata; Lean sources, generators, and build configuration are untouched, so code maintainability is unchanged.

Aspect	Value
Scope	generated metadata refresh
Introduces tech debt	✅ no
Maintainability	➖ unchanged
Brittleness	➖ unchanged
Risk	✅ low

This metadata refresh introduces no proof brittleness, compile-cost regression, or maintenance debt.

---

Tokens: 199,027 in / 3,643 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $0.4345 (Standard API equivalent; uncached input)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.