GapStatus
plain-language theorem explainer
Status record for the path-sum-measure gap: eight boolean flags saying which pieces (count finiteness, quotient finiteness, measure definition and positivity, modulus bounds, relabel invariance, continuum limit, substrate measure) are proved versus still open. Downstream status values fill the flags by rfl. Anyone auditing Lane 2 of the Seven Gaps cites this shape to read the honest closure board without hunting theorems.
Claim. A status record with eight boolean fields recording whether, for the scoped path-sum measure on bounded complexes: (i) the configuration count is finite, (ii) the relabeling quotient is finite, (iii) the measure is defined, (iv) positivity $0 < \mu \le 1$ is proved, (v) modulus bounds on the path sum $Z$ are proved, (vi) relabeling invariance of $Z$ is proved, (vii) a continuum limit is derived, and (viii) a substrate measure is derived.
background
Lane 2 of the Seven Gaps builds an honest path-sum measure for the Recognition Science partition function $Z_{RS}$ on a scoped class of bounded combinatorial complexes. Configurations carry incidence data $(n_V,n_E,n_T)$ with edge and tetrahedron vertex maps, mirroring Regge triangulation shape but dropping the metric; the recognition substrate fixes edge length at the minimum mesh, so the class is CDT-style and equilateral.
The module proves that the labeled class is finite, that relabeling is a genuine equivalence relation with finite quotient, that the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ satisfies $0<\mu(K)\le 1$ and is relabel-invariant, and that the path sum $Z=\sum_K \mu(K),w(K)$ is a finite sum with modulus bounds and equivalence invariance. Unitary weights $w=e^{iS}$ give the scoped $Z_{RS}$ statement.
This structure does not restate those theorems. It is the checklist type against which the module reports what closed and what remains model-level or open (continuum limit, substrate measure, sharper simplicial growth).
proof idea
No proof body: a pure structure declaration. Eight Bool fields, each a status bit. Instantiation is by structure literal (as in the downstream pathSumMeasureStatus), with each field set to true or false by definitional equality; the doc-comment requires that those assignments be rfl-forced rather than : True placeholders.
why it matters
Gives the Seven Gaps board a typed, machine-checkable status object for the path-sum-measure gap instead of prose claims. The sole direct consumer is pathSumMeasureStatus, which fills the first five flags true (count finite, quotient finite, measure defined, positivity, modulus bounds) and leaves the continuum and substrate bits for later work; the module doc already marks continuum limit and substrate measure as outside the proved tier.
In the broader RS gravity program this is the honesty layer for Lane 2: finiteness and the $\mu$-weighted path sum discharge the count-finiteness content that PathSumUVBound.AdmissibleTriangulationFamily had postulated, while refusing to claim a continuum or substrate derivation the file does not contain. It does not itself touch T0–T8 or the RCL; it only certifies how much of the discrete $Z_{RS}$ measure is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.