[kim-em]

Problem pages omit acceptance-build compute costs and useful submitter production details. Add separate Measured by LeanEval and Production information — self-reported displays, plus sortable per-problem comparisons. Wall times are labeled very noisy, unavailable counters have explicit reasons, and zero remains distinct from missing data. Existing standings and ranking rules are unchanged.

The consumer reads public State v7, prefers an available acceptance measurement (otherwise the latest successful replay), and links owners to the authenticated metadata editor. Current fields retain the date they actually changed; removed and superseded metadata text is not republished. Optional stray, malformed, duplicate or mismatched receipts are skipped with a diagnostic, preserving accepted-result publication. The site keeps its output schema checks without another copy of the producer's hash validator or canonical contract tests. Earlier public projection schemas remain unchanged.

Prerequisites: https://github.com/leanprover/lean-eval-state/pull/51 and leanprover/lean-eval-submissions#2163. Merge/deploy those producers before this consumer. See docs/compute-reporting.md. Historical replay remains separate operator work.

Validation: 89 Python tests, four Node behavior tests, workflow actionlint, and complete real Results/current-State-v7 generation and output validation. Regression tests cover field-level dates and accepted results surviving optional-statistics errors. Pages CI performs the full build; no production deployment is performed by this PR.

[kim-em]

Prerequisites: merge/deploy https://github.com/leanprover/lean-eval-state/pull/51 and leanprover/lean-eval-submissions#2163 before this consumer. The Worker also depends on https://github.com/leanprover/lean-eval-state-staging/pull/25. This PR targets main. Production now requests projection v7 and links to the new owner editor, so deploy the producers first. PR builds continue to use public base Results without private State credentials.