pathSumMeasureStatus
plain-language theorem explainer
Status board for the path-sum measure gap on the scoped class of bounded complexes. Six flags are true: count finiteness, quotient finiteness, measure definition, positivity, modulus bounds, and relabel invariance. Continuum limit and substrate-derived nonuniform measure stay false. Downstream status lemmas cite it by rfl; the body is a pure structure literal.
Claim. The path-sum-measure gap status records that count-finiteness, finiteness of the relabeling quotient, definition of the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut}\,K|$, positivity of $\mu$, modulus bounds on the path sum $Z$, and relabeling invariance of $Z$ are all proved, while the continuum limit $B\to\infty$ and a substrate-derived nonuniform measure remain underived.
background
Lane 2 of the Seven Gaps program builds an honest path-sum measure for $Z_{\mathrm{RS}}$ on a scoped configuration class. Configurations are BoundedComplex B: bounded incidence data (vertex/edge/tetrahedron counts and maps) at fixed lattice scale, mirroring Regge triangulation shape without a metric field. The class is a Fintype via an explicit code equivalence, so every subclass is finite.
Relabeling is a proved equivalence relation; the quotient of labeled complexes is finite. Automorphism groups are finite and nonempty, so the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ satisfies $0<\mu(K)\le 1$ and is relabel-invariant. The path sum $Z(B,w)=\sum_K \mu(K),w(K)$ is then a finite sum with modulus bounds $|Z|\le\sum\mu$ and $|Z|\le|\mathrm{BoundedComplex},B|$, and is invariant under equivalence-preserving bijections. Unitary weights $w=e^{iS}$ give the scoped $Z_{\mathrm{RS}}$ statement.
GapStatus is the eight-boolean ledger for what this module closes versus leaves open. All flags are ordinary Bools forced by rfl at use sites; none are : True placeholders.
proof idea
Definitional structure literal, not a proof. Each field of GapStatus is assigned a concrete true or false matching the theorems proved earlier in the module (Fintype instance, finite quotient, $\mu$ positivity and bounds, $Z$ modulus and relabel invariance) and the two items the module doc marks MODEL/OPEN (continuum limit, substrate-derived measure). Downstream status_* lemmas re-export each flag by rfl.
why it matters
This is the honest scoreboard for Seven Gaps Lane 2: a proved path-sum measure for scoped $Z_{\mathrm{RS}}$. It lets parent status theorems (status_count_finite, status_quotient_finite, status_measure_defined, status_measure_positive, status_modulus_bound, status_relabel_invariance, and the two OPEN markers status_continuum_open and the substrate-measure open flag) pin claims without overclaiming.
Module theorems already discharge count-finiteness content that PathSumUVBound.AdmissibleTriangulationFamily.growthBase only postulated, and establish the standard $1/|\mathrm{Aut}|$ CDT-style measure with modulus and relabel control. The two false flags keep the continuum limit $B\to\infty$ and any substrate-derived nonuniform measure explicitly open, matching the module's MODEL tier. Downstream docs point here for that openness (e.g. automorphism positivity notes the uniform convention and defers nonuniform measure to this status).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.