status_measure_positive
plain-language theorem explainer
Records that the path-sum measure gap status has positivity marked proved. Gap auditors and anyone wiring Seven-Gaps dashboards cite it as the boolean witness that mu is positive on the scoped class. The proof is definitional reflexivity on the status record.
Claim. In the path-sum measure status record, the flag asserting that positivity of the configuration measure has been proved equals $\mathrm{true}$.
background
Lane 2 of the Seven Gaps programme builds an honest path-sum measure for the scoped recognition partition function $Z_{\mathrm{RS}}$. Configurations live in the finite class BoundedComplex B of bounded incidence data at fixed lattice scale (CDT-style equilateral complexes with metric dropped). Relabeling is a genuine equivalence, the quotient of triangulation classes is finite, and each labeled complex $K$ has finite nonempty automorphism group $\mathrm{Aut},K$.
The symmetry-factor measure is $\mu(K)=1/|\mathrm{Aut},K|$. The module proves $0<\mu(K)\le 1$ and relabeling invariance, then forms the finite path sum $Z(B,w)=\sum_K \mu(K),w(K)$ with modulus bounds. The status record aggregates which pieces of that package are closed.
Upstream, pathSumMeasureStatus is the concrete GapStatus value with every relevant boolean set true, including the positivity field.
proof idea
One-line definitional wrapper. The status definition sets measure_positive_proved := true, so the equality is rfl. No lemmas are applied.
why it matters
Closes the positivity checkbox in the Seven Gaps path-sum measure ledger. The underlying mathematics is the pair of theorems that $\mu(K)=1/|\mathrm{Aut},K|$ is strictly positive and at most one on every labeled complex in the scoped class, which licenses the finite weighted sum $Z_{\mathrm{RS}}$ and the unitary instance $w=e^{iS}$. No downstream consumers are wired yet; the flag exists so gap trackers and the module's honest status tier can read a single boolean rather than re-inspect proofs. It does not touch the still-open exponential-growth semantics of growthBase for exact simplicial subclasses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.