Link Arithmon/K3; rewrite global-k3-bound as the certified-metric problem

- LEDGER: declare the K3 concept DOI 10.5281/zenodo.22047469 in known_dois
  before any surface cites it.
- problems/global-k3-bound: status active. The certified atlas (Arithmon/K3)
  is the first public layer; work toward a certified evaluation of the metric
  with a global error bound is in progress, no result is claimed. The K7
  erratum correction is kept.
- INDEX: title and status updated.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Author: gift-framework

INDEX.md

@@ -6,7 +6,7 @@
 ## Geometry (3)
 
 - [From explicit near-solution to exact G2 metric](problems/exact-g2-metric.md) · **active** · updated 2026-06-11
-- [Global residual bound on all of K3](problems/global-k3-bound.md) · **open** · updated 2026-06-11
+- [From a certified atlas to a certified metric on K3](problems/global-k3-bound.md) · **active** · updated 2026-09-23
 - [Closed-form spectral data for the K7 metric](problems/closed-form-spectral-data.md) · **dormant** · updated 2026-06-11
 
 ## Selection (1)

LEDGER.json

@@ -40,6 +40,7 @@
     "10.5281/zenodo.20666879": "Sieve, frozen inputs, pre-registration",
     "10.5281/zenodo.20666878": "Sieve, companion deposit",
     "10.5281/zenodo.16891489": "K7 Framework, concept DOI",
+    "10.5281/zenodo.22047469": "K3, certified analytic geometry on an explicit K3 surface (Arithmon/K3), concept DOI",
     "10.5281/zenodo.18860358": "de La Fourniere 2026, Explicit G2 Holonomy Metric on a Compact TCS 7-Manifold K7 (cited in k7-lean sources + blueprint)",
     "10.5281/zenodo.18920368": "de La Fourniere 2026, Spectral Geometry of a TCS G2 Manifold (cited in k7-lean sources)"
   },

problems/global-k3-bound.md

@@ -1,32 +1,33 @@
 ---
-title: Global residual bound on all of K3
+title: From a certified atlas to a certified metric on K3
 axis: geometry
-status: open
+status: active
 opened: 2026-06-11
 updated: 2026-09-23
 ---
 
-**Statement.** Extend the certified bound on the Calabi-Yau volume-form
-residual from a box-local statement (4000 open boxes, Krawczyk-verified, with
-the variance aggregation re-computed inside Lean) to a global bound on all of
-K3.
+**Statement.** Produce a certified evaluation of the Ricci-flat (Calabi-Yau)
+metric on one explicit K3 surface: an algorithm that evaluates the metric
+with a global, machine-checked error bound, rather than a closed formula.
 
-**Why it matters.** The box-local certificate is the framework's rigor
-anchor; a global bound would remove the locality caveat entirely.
+**Why it matters.** The geometry this program rests on is only known
+numerically. A certified evaluator would turn "a good approximation" into a
+statement with a proved error, everywhere on the surface.
 
-**Correction (K7 erratum, 2026-08-22).** The box-local certificate does not
-bound what this statement says: it bounds an auxiliary quantity, not the
-Calabi-Yau volume-form residual. Measured on the same 4000 points in the
-correct pullback convention, the residual variance is 5.3e-1 (ratio 3677 to
-the certified value) and 522 points carry no positive-definite form. What
-stands is the surface-level certification (each box contains an exact point
-of K3) and the method. The premise of this problem is therefore withdrawn as
-stated; see `K7/publications/ERRATUM_v3.5.md`.
+**Where it stands.** The first layer is public:
+[Arithmon/K3](https://github.com/Arithmon/K3) (concept DOI
+[10.5281/zenodo.22047469](https://doi.org/10.5281/zenodo.22047469)) certifies
+the analytic geometry of an explicit K3 surface, a finite holomorphic atlas
+whose chart domains, transitions and branch continuations are machine-checked.
+No Ricci-flat metric is claimed there. Work toward the certified evaluation of
+the metric is in progress; no result is claimed.
 
-**Known constraints.** The certificate formerly quoted here (variance
-envelope 1321/10^7, 7.57x margin) applies to the auxiliary quantity only. Scoping concluded that a genuinely global bound is research-level
-and that the only identified route is a Positivstellensatz / sum-of-squares
-certificate over the orbifold chart.
+**Correction (K7 erratum, 2026-08-22).** An earlier formulation of this problem
+started from a box-local "certified bound on the Calabi-Yau residual". That
+bound certifies an auxiliary quantity, not the Calabi-Yau residual: in the
+correct pullback convention the residual variance of that ansatz is 5.3e-1 and
+522 of its 4000 points carry no positive-definite form. See
+`K7/publications/ERRATUM_v3.5.md`.
 
-**Next step.** SOS feasibility study on a reduced chart; no commitment until
-the central lock (exact metric) settles priorities.
+**Next step.** Complete the certified evaluator and publish it the way the
+atlas was published: with the certificates and a one-command verification.