defaultProvenance
plain-language theorem explainer
Default provenance strings for the four external Regge-convergence inputs packaged by the registry: CMS 1984 Thm 5.1 (axiomatized theorem) plus three axiomatized external hypotheses (special quadratic action, Ricci O(a²), holonomy/Riemann). Gravity auditors cite it when checking that the registry only repackages named external math with explicit status tags. The body is a four-element string list literal.
Claim. The default provenance record is the four-element list of status-tagged citations: (1) Cheeger–Müller–Schrader (1984), Theorem 5.1 on curvature-measure convergence, tagged external theorem (axiomatized); (2) the stronger $O(a^2)$ Regge-to-Einstein–Hilbert action-convergence hypothesis, tagged external hypothesis (axiomatized); (3) Regge Ricci-scalar $O(a^2)$ convergence, tagged external hypothesis (axiomatized); (4) Regge holonomy / Riemann convergence, tagged external hypothesis (axiomatized).
background
The module ReggeConvergenceRegistry consolidates four external continuum-limit propositions that previously lived as separate axioms in NonlinearConvergence into one named structure. Module doc: each field is typed by the exact original proposition, so the registry is a faithful repackaging; no convergence content is restated or re-proved.
The four inputs are: CMS Theorem 5.1 (curvature-measure bound with $\eta^{1/2}$ bulk plus boundary-tube term); a special-purpose $O(a^2)$ action-convergence hypothesis used in weak-field or numerical settings; Regge Ricci-scalar $O(a^2)$ convergence; and Regge holonomy/Riemann convergence. Only the first is an external theorem; the other three remain external hypotheses, all axiomatized in Lean.
The structure also carries a provenance field of type List String that documents each input with a status tag. This definition supplies the canonical default value of that field.
proof idea
Pure data definition: a four-element List String literal. Each entry names one registry field, cites the external source (CMS 1984 Thm 5.1, or the corresponding hypothesis), and appends the status tag external theorem, axiomatized or external hypothesis, axiomatized. No tactics, no lemmas, no computation.
why it matters
Keeps the gravity stack honest about what is proved inside Lean versus what is imported from classical Regge calculus. The registry structure packages CMS measure convergence together with the three stronger $O(a^2)$ hypotheses used for Ricci and Riemann recovery; this list is the human-readable audit trail attached to every default registry instance.
Downstream, faithful-projection lemmas (cms_measure_bound_faithful, special_quadratic_faithful, ricci_convergence_faithful, riemann_convergence_faithful) and the mk / mk_provenance constructors rely on this provenance remaining aligned with the four fields. No used-by edges are recorded yet; the value is documentary and constructor-facing rather than a proof dependency.
In the broader RS gravity program this sits upstream of continuum recovery of Einstein–Hilbert from discrete deficit geometry, separate from the discrete Lichnerowicz axis-sector results and from the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.