Make homepage “Formalized” progress explicit about scope and proof completion #27

Problem

The landing-page hero presents a roadmap statistic as a generic “Formalized N%” headline. It does not identify the denominator as decomposed, declaration-bearing DAG leaves, so readers can reasonably interpret it as progress through the named book or thesis.

The current implementation:

• counts only formalizable leaf nodes;
• treats stated as settled, although that state explicitly means the theorem proof is absent;
• computes the headline with round(100 * done / total).

This creates three separate accuracy problems:

1. Mapped, deferred, undecomposed, and out-of-scope source material disappears from the headline without the scope being shown.
2. A statement-only theorem can count as finished when its dependencies block it (stated), while the same statement does not count once it becomes ready to prove (can_prove).
3. Incomplete work can display as 100%; for example, Python rounds 199/200 to 100%.

Reproduction

Hartshorne (historical deployment)

When this issue was filed on 2026-09-19, the latest successful Pages deployment was run 34066433925, built from commit 3b73cddb…. Its landing page displayed:

100% Formalized
68 of 68 items settled

At that commit, the coverage contract limited scope to Chapter I §§1–3, pages 1–23, while pages 24–420 were untouched.

This is a pinned historical example; later deployments may change the counts without changing the renderer semantics reported here.

Bundled Cabannes example

Autoform own fixture says it develops one representative chapter in detail. Its coverage table has one DECOMPOSED area, five MAPPED areas, and one OUT area.

From the repository root:

cd skills/setup/assets/cabannes-thesis-project
output=$(mktemp -d)
autoform render blueprint --output "$output" --lean-root .
grep -oE '>[0-9]+%<|>[0-9]+ of [0-9]+ items settled<' "$output/README.md"

Output:

>71%<
>5 of 7 items settled<

That is 71% of the seven decomposed targets, not 71% of the thesis.

Expected behavior

The homepage should distinguish source coverage from progress inside the decomposed roadmap. For example:

Decomposed roadmap: 5 of 7 targets complete (71%)
Source coverage: 1 decomposed · 5 mapped · 1 out

Exact wording is flexible, but:

• The denominator is explicitly labeled as scoped/decomposed roadmap targets.
• The scope or coverage summary is visible beside the metric, with a link to the coverage contract.
• A theorem without a proof is not counted as complete regardless of dependency readiness; statement progress may be shown separately.
• Definitions whose Lean bodies compile and verified Mathlib targets still count as complete.
• An incomplete fraction never renders as 100%.
• Tests cover the bundled Cabannes example, a blocked statement-only theorem, and a 199/200 rounding case.

A whole-source percentage is not required; source areas are rarely equal-sized. A clear scoped count plus coverage dispositions is sufficient.

Related groundwork: #8 and #19. The future aggregate progress work in #24 should consume the same clarified semantics.

This issue concerns progress semantics only. Deployment freshness and Markdown-link rewriting are separate concerns.