docs(interval): record final centered reconciliation

Author: Kim Morrison

progress/20260814T214921Z.md

@@ -0,0 +1,30 @@
+# PR #9228 final reconciliation
+
+## Accomplished
+
+- Replayed only the prepared centered arbitrary-function feature onto exact
+  current `main` `b6fbf1369c32cdc7a83c854ef5d4d31be7fc4533`.
+- Resolved the Lake registration overlap by preserving the finalized dyadic
+  semantics, PNT+ Table 12 targets, and the centered experiment/conformance.
+- Preserved the prepared package theorem, live one-rule quote, generic replay,
+  ordinary theorem, and mutated-premise rejection without source changes.
+- Refreshed the centered proof-only Lake exemption for exact resolved blob
+  `93b5d48c2868027cb186ba84dea21de832485f4e`.
+- Built the centered, dyadic, nested-branch, ReLU, and PNT targets successfully
+  in a 2,252-job focused build.
+- Passed copyright, file-line, DAG, trust-surface, Phase 4, factor-freshness,
+  PNT-inventory, diff, and banned-mechanism checks.
+
+## Current frontier
+
+- The exact local candidate is ready to push to PR #9228 and retarget to
+  upstream `main` before fresh exact-head review and CI.
+
+## Next step
+
+- Push with force-with-lease, verify literal base/head metadata, then run a
+  fresh isolated Opus review and monitor exact-head CI.
+
+## Blockers
+
+- None.

scripts/bench/proof_only_runtime_exemptions.json

@@ -200,7 +200,7 @@
   {
     "path": "lakefile.lean",
     "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
-    "current_blob": "69b01838e58037470269a8036ece5cd865b0a7f0",
+    "current_blob": "93b5d48c2868027cb186ba84dea21de832485f4e",
     "reason": "Additionally registers the proof-only centered-function real-semantics companion and its conformance module; the factorization service target and executable dependency graph are unchanged."
   },
   {