HasGeometricZRSContinuumLimit
plain-language theorem explainer
Packages the open continuum-limit proposition for the geometric recognition path sum: once a metric refinement family and an explicit real measure on its finite configuration spaces are fixed, the finite-level path sums are required to tend to some complex value as the level tends to infinity. Continuum and gravity workers cite it as the well-typed geometric Z_RS target that remains unproved. The body is pure Prop packaging of a filter limit, not a theorem.
Claim. Given a metric refinement family $F$ and a real-valued measure on each finite configuration space of $F$, the geometric continuum-limit property holds when there exists $L \in \mathbb{C}$ such that the finite-level path sums $Z_n(F,\mathrm{measure})$ tend to $L$ in $\mathbb{C}$ as $n \to \infty$.
background
Module P2.5 isolates a carrier obstruction: the bare triangulation quotient only sees combinatorial type, not metric geometry. Two positive nondegenerate metric decorations of the same one-tetrahedron class have different edge lengths and different Cayley-Menger observables, so no class-only function recovers either observable, and the forgetful map from metric-decorated complexes is non-injective.
To replace a bare complexity cutoff by geometric mesh refinement, the module supplies the minimal carrier interface: a metric refinement family with finite metric-decorated configuration spaces at each level, a genuine mesh tending to zero, coarse projections between adjacent levels, and summable local action-step control. It does not assume path-sum convergence.
The finite-level path sum is then defined by summing measure times $\exp(i,S)$ over those configurations. The measure is an explicit argument because its substrate derivation is the separate P2.2 obligation. The present definition is exactly the continuum-limit proposition for that sequence.
proof idea
Definitional packaging only. The proposition is the standard filter statement that the sequence of finite-level geometric path sums (the sum over configurations of measure times complex exponential of the action) admits some complex limit point as the refinement level tends to infinity. No lemmas are applied and nothing is proved.
why it matters
Closes the honesty boundary of the P2.5 metric-refinement carrier blocker: after the obstruction theorems (non-injective forgetful map, class-only Cayley-Menger failure, causal 4-simplex volume variation) and the proposed carrier API, this is the named OPEN geometric continuum target. Module docs mark construction of such a family from the recognition substrate, derivation of its measure and action, and the geometric continuum theorem as still open. Complexity-cutoff convergence remains a different obligation from metric mesh refinement. No downstream theorems yet consume it; it is the well-typed goalpost for later continuum work in the Seven Gaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.