mk_roundtrip
plain-language theorem explainer
Reassembling a Regge convergence registry from its five field projections recovers the original registry definitionally. Anyone treating the registry as a faithful pack of the four external Regge-to-continuum inputs (CMS measure bound, special quadratic, Ricci, Riemann) plus provenance can cite this. The proof is pure reflexivity: structure eta holds by construction.
Claim. For any Regge convergence registry $r$, reconstructing a registry from the five projections of $r$ (CMS curvature-measure bound, special $O(a^2)$ quadratic hypothesis, Ricci-scalar convergence axiom, Riemann/holonomy convergence axiom, and provenance list) yields exactly $r$.
background
The module packages four external Regge-calculus convergence propositions, previously scattered in NonlinearConvergence, into one named structure. Each field is typed by the exact original proposition, so the pack is a faithful repackaging rather than a weakening. The four inputs are external mathematics: Cheeger–Müller–Schrader (1984) Thm 5.1 (curvature-measure bound with $\eta^{1/2}$ bulk plus boundary-tube term), a stronger special-purpose $O(a^2)$ action-convergence hypothesis, a Regge Ricci-scalar convergence axiom, and a Regge holonomy/Riemann convergence axiom. A fifth field records provenance status tags for each.
Sibling projection lemmas already show each field recovers the corresponding original proposition. The present statement is the complementary eta law: the constructor applied to those projections is the identity on registries.
proof idea
Term-mode proof by rfl. After unfolding the registry constructor mk on the five projections of r, both sides are definitionally equal by structure eta (the canonical constructor–projection roundtrip for a structure). No lemmas are invoked; no rewriting or case analysis is needed.
why it matters
Closes the faithfulness story for the registry: projections recover the original external propositions, and the constructor recovers the registry. Downstream consumers can treat a single ReggeConvergenceRegistry value as interchangeable with the four bare axioms plus provenance, without fear of information loss or silent weakening. That matters for gravity-side arguments that need a clean handle on which Regge-to-Einstein–Hilbert continuum limits are assumed (CMS measure bound, special quadratic, Ricci, Riemann) when linking discrete curvature to continuum second-variation and weak-field faces. No used_by edges yet; the theorem is infrastructure for later nonlinear-convergence and continuum-limit citations rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.